El conjunto de símbolos no lógicos (predicados, funciones y constantes) junto con las categorías o tipos especificados que define la firma de un lenguaje formal.

Principio

Un vocabulario (firma) fija los símbolos primitivos y sus aridades y tipos; determina qué fórmulas y términos están bien formados y restringe la clase de interpretaciones al especificar qué símbolos deben recibir significado.

Demostración

Una firma Σ puede consistir en un predicado binario R, una función unaria f y constantes c,d; el lenguaje construido a partir de Σ permite formar términos como f(f(c)) y fórmulas como ∃x R(f(x),d) según las aridades y tipos de Σ.

Aplicación incorrecta

Usar símbolos que no están en el vocabulario declarado o cambiar la aridad de un símbolo durante una prueba —por ejemplo tratar R como binario en un paso y ternario en el siguiente— viola las reglas de formación e invalida las derivaciones.

Consecuencia

Un vocabulario claramente especificado brinda un marco estable para la sintaxis, la semántica y la teoría de la prueba: asegura la bien-formación, la interpretación uniforme entre modelos y enunciados precisos sobre expresividad y definibilidad.

Inversión

Si el vocabulario pudiera variar arbitrariamente dentro de una teoría, la coherencia sintáctica y las comparaciones semánticas entre modelos colapsarían; las teorías carecerían de un conjunto fijo de símbolos primitivos.

Límite

No incluye símbolos lógicos (conectivos, cuantificadores) que suelen ser fijos, ni la notación metalingüística; según el formalismo puede o no incluir igualdad o declaraciones de tipos/sorts.

Tensión semántica

Existe tensión entre usar un vocabulario mínimo para favorecer la generalidad y expandirlo para nombrar conceptos convenientes; añadir símbolos aumenta la comodidad expresiva pero puede ocultar relaciones de definibilidad e interpretabilidad relativa.

Síntesis

Un vocabulario es la firma del lenguaje: la colección finita o infinita de símbolos de predicado, función y constante (y tipos) cuyas aridades e identidades declaradas determinan cómo se forman términos y fórmulas y cómo los modelos deben interpretarlos.