Metalogic

Un lenguaje formal es un conjunto organizado de símbolos , los cuales lo definen con precisión mediante su forma y posición. Por lo tanto, dicho lenguaje puede definirse sin referencia al significado de sus expresiones; puede existir antes de que se le asigne cualquier interpretación , es decir, antes de que tenga significado alguno. La lógica de primer orden se expresa en algún lenguaje formal. Una gramática formal determina qué símbolos y conjuntos de símbolos constituyen fórmulas en un lenguaje formal.

Un lenguaje formal puede definirse formalmente como un conjunto A de cadenas (secuencias finitas) sobre un alfabeto fijo α. Algunos autores, incluido Rudolf Carnap , definen el lenguaje como el par ordenado <α, A >. ^{[ 3 ]} Carnap también exige que cada elemento de α aparezca en al menos una cadena de A.

Las reglas de formación (también llamadas gramática formal ) son una descripción precisa de las fórmulas bien formadas de un lenguaje formal. Son sinónimo del conjunto de cadenas sobre el alfabeto del lenguaje formal que constituyen fórmulas bien formadas. Sin embargo, no describen su semántica (es decir, su significado).

Un sistema formal (también llamado cálculo lógico o sistema lógico ) consta de un lenguaje formal junto con un aparato deductivo (también llamado sistema deductivo ). El aparato deductivo puede consistir en un conjunto de reglas de transformación (también llamadas reglas de inferencia ) o un conjunto de axiomas , o bien ambos. Un sistema formal se utiliza para derivar una expresión a partir de una o más expresiones.

Un sistema formal puede definirse formalmente como una tripleta ordenada <α,${\displaystyle {\mathcal {I}}}$,${\displaystyle {\mathcal {D}}}$d>, donde${\displaystyle {\mathcal {D}}}$d es la relación de derivabilidad directa. Esta relación se entiende en un sentido amplio , de modo que las oraciones primitivas del sistema formal se toman como directamente derivables del conjunto vacío de oraciones. La derivabilidad directa es una relación entre una oración y un conjunto finito, posiblemente vacío, de oraciones. Los axiomas se eligen de tal manera que cada miembro de primer lugar de${\displaystyle {\mathcal {D}}}$d es miembro de${\displaystyle {\mathcal {I}}}$y cada miembro que ocupa el segundo lugar es un subconjunto finito de${\displaystyle {\mathcal {I}}}$.

Un sistema formal también puede definirse con solo la relación${\displaystyle {\mathcal {D}}}$d. Por lo tanto, puede omitirse${\displaystyle {\mathcal {I}}}$ y α en las definiciones de lenguaje formal interpretado y sistema formal interpretado . Sin embargo, este método puede ser más difícil de entender y usar. ^{[ 3 ]}

Una demostración formal es una secuencia de fórmulas bien formadas de un lenguaje formal, la última de las cuales es un teorema de un sistema formal. El teorema es una consecuencia sintáctica de todas las fórmulas bien formadas que lo preceden en el sistema de demostración. Para que una fórmula bien formada se considere parte de una demostración, debe resultar de la aplicación de una regla del aparato deductivo de algún sistema formal a las fórmulas bien formadas anteriores en la secuencia de demostración.

La interpretación de un sistema formal consiste en asignar significados a los símbolos y valores de verdad a las oraciones de dicho sistema. El estudio de las interpretaciones se denomina semántica formal . Dar una interpretación es sinónimo de construir un modelo .

En metalógica, los lenguajes formales a veces se denominan lenguajes objeto . El lenguaje utilizado para formular enunciados sobre un lenguaje objeto se llama metalenguaje . Esta distinción es una diferencia clave entre lógica y metalógica. Mientras que la lógica se ocupa de demostraciones en un sistema formal , expresadas en algún lenguaje formal, la metalógica se ocupa de demostraciones sobre un sistema formal , expresadas en un metalenguaje sobre algún lenguaje objeto.

En metalógica, la «sintaxis» se refiere a lenguajes formales o sistemas formales sin considerar su interpretación, mientras que la «semántica» se refiere a las interpretaciones de lenguajes formales. El término «sintáctico» tiene un alcance ligeramente más amplio que «teórico de la demostración», ya que puede aplicarse tanto a propiedades de lenguajes formales sin sistemas deductivos como a sistemas formales. «Semántico» es sinónimo de «teórico de modelos».

En metalógica, las palabras «usar» y «mencionar» , tanto en su forma sustantiva como verbal, adquieren un sentido técnico para identificar una distinción importante. ^{[ 2 ]} La distinción entre uso y mención (a veces denominada distinción entre palabras como palabras ) es la diferencia entre usar una palabra (o frase) y mencionarla . Generalmente, se indica que una expresión se menciona en lugar de usarse encerrándola entre comillas, escribiéndola en cursiva o colocándola en una línea aparte. El hecho de encerrar una expresión entre comillas nos da el nombre de la misma, por ejemplo:

"Metalogic" es el nombre de este artículo. Este artículo trata sobre la metalogic.

La distinción entre tipo y token es una distinción en metalógica que separa un concepto abstracto de los objetos que son instancias particulares de ese concepto. Por ejemplo, la bicicleta en tu garaje es un token del tipo de cosa conocida como "La bicicleta". Sin embargo, la bicicleta en tu garaje está en un lugar y momento específicos, lo cual no se aplica a "la bicicleta" en el sentido de la oración: " La bicicleta se ha vuelto más popular recientemente". Esta distinción se utiliza para clarificar el significado de los símbolos en los lenguajes formales .