El número de variables distintas que aparecen en una fórmula o teoría, donde 'distintas' se refiere a símbolos de variable sintácticamente diferentes; se usa como una métrica simple de complejidad sintáctica y demanda de recursos.

Principio

La cuenta de variables mide cuántos marcadores de posición separados están disponibles o son necesarios en una expresión; interactúa con la estructura de cuantificadores, el ámbito y el renombrado, y puede ser un parámetro crucial en fragmentos lógicos (por ejemplo, el fragmento de una o dos variables).

Demostración

La fórmula ∀x ∃y (P(x) ∧ Q(y,z)) contiene las variables distintas x, y, z, por lo que su cuenta de variables es 3; renombrar y a y' conserva el recuento aunque cambien los nombres.

Aplicación incorrecta

Contar las apariciones totales de variables en lugar de los símbolos de variable distintos, o confluir la cuenta de variables con el número de variables ligadas frente a libres sin aclaración, es una mala aplicación que da estimaciones de complejidad engañosas.

Consecuencia

Limitar el número de variables distintas en un lenguaje o fragmento puede producir resultados fuertes sobre decidibilidad o complejidad: muchos fragmentos lógicos se vuelven decidibles o más fáciles de analizar cuando la cuenta de variables está limitada, y los procedimientos algorítmicos a menudo explotan tales cotas.

Inversión

La situación inversa considera un suministro ilimitado o infinito de símbolos de variables; aunque flexible para representar muchos marcadores distintos, las variables no acotadas pueden oscurecer la complejidad y dificultar obtener cotas algorítmicas uniformes.

Límite

La cuenta de variables se refiere a los símbolos de variable sintácticamente declarados presentes en fórmulas o en una teoría y no mide directamente cómo se usan las variables (ligadas vs libres) salvo que el contexto especifique esa distinción; excluye metadariables y parámetros introducidos solo a nivel meta.

Tensión semántica

La cuenta de variables compite con medidas relacionadas como el rango de cuantificadores y la longitud de la fórmula: una pequeña cuenta de variables puede permitir aun así gran alternancia de cuantificadores o fórmulas largas mediante la reutilización de variables, generando tensión sobre qué medida captura mejor la complejidad.

Síntesis

La cuenta de variables es el número de símbolos de variable sintácticamente distintos que aparecen en una fórmula o teoría; como parámetro simple y manejable, restringe el ámbito y la expresividad y se usa con frecuencia para clasificar y analizar fragmentos lógicos.