5.3: Términos y Fórmulas

Template:MathJaxZach

Una vez que\(\Lang L\) se da un lenguaje de primer orden, podemos definir expresiones construidas a partir del vocabulario básico de\(\Lang L\). Estos incluyen en términos y fórmulas particulares.

Definición\(\PageIndex{1}\): Terms

El conjunto de términos\(\Trm[L]\) de\(\Lang L\) se define inductivamente por:

1. Cada variable es un término.
2. Cada símbolo constante de\(\Lang L\) es un término.
3. Si\(f\) es un símbolo de función\(n\) -place y\(t_1\),...,\(t_n\) son términos, entonces\(\Atom{f}{t_1, \ldots, t_n}\) es un término.
4. Nada más es un término.

Un término que no contiene variables es un término cerrado.

Los símbolos constantes aparecen en nuestra especificación del lenguaje y los términos como una categoría separada de símbolos, pero en su lugar podrían haber sido incluidos como símbolos de función de lugar cero. Entonces podríamos prescindir de la segunda cláusula en la definición de términos. Sólo tenemos que entender\(\Atom{f}{t_1, \ldots, t_n}\) como solo\(f\) por sí mismo si\(n = 0\).

Definición\(\PageIndex{2}\): Formula

El conjunto de fórmulas\(\Frm[L]\) del lenguaje\(\Lang L\) se define inductivamente de la siguiente manera:

1. \(\lfalse\) is an atomic formula.
2. Si\(R\) es un símbolo de predicado\(n\) -place de\(\Lang L\) y\(t_1\),...,\(t_n\) son términos de\(\Lang L\), entonces\(\Atom{R}{t_1,\ldots, t_n}\) es una fórmula atómica.
3. Si\(t_1\) y\(t_2\) son términos de\(\Lang L\), entonces\(\Atom{\eq[][]}{t_1, t_2}\) es una fórmula atómica.
4. Si\(A\) is a formula, then \(\lnot A\) is formula.
5. Si\(A\) and \(B\) are formulas, then \((A \land B)\) is a formula.
6. Si\(A\) and \(B\) are formulas, then \((A \lor B)\) is a formula.
7. Si\(A\) and \(B\) are formulas, then \((A \lif B)\) is a formula.
8. Si\(A\) is a formula and \(x\) is a variable, then \(\lforall{x}{A}\) is a formula.
9. Si\(A\) is a formula and \(x\) is a variable, then \(\lexists{x}{A}\) is a formula.
10. Nada más es una fórmula.

Las definiciones del conjunto de términos y la de fórmulas son definiciones inductivas. Esencialmente, construimos el conjunto de fórmulas en infinitamente muchas etapas. En la etapa inicial, pronunciamos todas las fórmulas atómicas como fórmulas; esto corresponde a los primeros casos de la definición, es decir, los casos para\(\lfalse\), \(\Atom{R}{t_1,\dots,t_n}\) y\(\Atom{\eq[][]}{t_1,t_2}\). “Fórmula atómica” significa así cualquier fórmula de esta forma.

Los otros casos de la definición dan reglas para construir nuevas fórmulas a partir de fórmulas ya construidas. En la segunda etapa, podemos utilizarlos para construir fórmulas a partir de fórmulas atómicas. En la tercera etapa, construimos nuevas fórmulas a partir de las fórmulas atómicas y las obtenidas en la segunda etapa, y así sucesivamente. Una fórmula es cualquier cosa que finalmente se construya en tal etapa, y nada más.

Por convención, escribimos\(\eq[][]\) entre sus argumentos y dejamos fuera los paréntesis:\(\eq[t_1][t_2]\) es una abreviatura de\(\Atom{\eq[][]}{t_1,t_2}\). Además,\(\lnot \Atom{\eq[][]}{t_1,t_2}\) se abrevia como\(\eqN[t_1][t_2]\). Al escribir una fórmula\((B \ast C)\) construida a partir de\(B\),\(C\) usando un conectivo de dos lugares\(\ast\), a menudo omitiremos el par de paréntesis más externo y escribiremos simplemente\(B \ast C\).

Algunos textos lógicos requieren que la variable\(x\) se produzca\(A\) en orden para\(\lexists{x}{A}\) y\(\lforall{x}{A}\) para contar como fórmulas. No pasa nada malo si no lo requieres, y facilita las cosas.

Definición\(\PageIndex{3}\)

Las fórmulas construidas usando los operadores definidos deben entenderse de la siguiente manera:

1. \(\ltrue\) abbreviates \(\lnot\lfalse\).
2. \(A \liff B\) abbreviates \((A \lif B) \land (B \lif A)\).

Si trabajamos en un lenguaje para una aplicación específica, a menudo escribiremos símbolos predicados de dos lugares y símbolos de función entre los términos respectivos, por ejemplo,\(t_1 < t_2\) y\((t_1 + t_2)\) en el lenguaje de la aritmética y\(t_1 \in t_2\) en el lenguaje de la teoría de conjuntos. La función sucesora en el lenguaje de la aritmética incluso se escribe convencionalmente después de su argumento:\(t'\). Oficialmente, sin embargo, estas son solo abreviaturas convencionales para\(\Atom{\Obj A^2_0}{t_1, t_2}\)\(\Obj f^2_0(t_1, t_2)\),,\(\Atom{\Obj A^2_0}{t_1, t_2}\) y\(f^1_0(t)\), respectivamente.

Definición\(\PageIndex{4}\): Syntactic identity

El símbolo\(\ident\) expresa identidad sintáctica entre cadenas de símbolos, es decir,\(A \ident B\) iff\(A\) y\(B\) son cadenas de símbolos de la misma longitud y que contienen el mismo símbolo en cada lugar.

El\(\ident\) símbolo puede estar flanqueado por cadenas obtenidas por concatenación, por ejemplo,\(A \ident (B \lor C)\) significa: la cadena de símbolos\(A\) es la misma cadena que la obtenida al concatenar un paréntesis de apertura, la cadena\(B\), la \(\lor\)símbolo, la cadena\(C\) y un paréntesis de cierre, en este orden. Si este es el caso, entonces sabemos que el primer símbolo de\(A\) es un paréntesis de apertura,\(A\) contiene\(B\) como una subcadena (comenzando en el segundo símbolo), esa subcadena es seguida por\(\lor\), etc.