Metalógica

Metalógica é o estudo da metateoria da Lógica. Enquanto a Lógica estuda como sistemas lógicos podem ser usados para construir argumentos válidos e corretos, a Metalógica estuda as propriedades dos sistemas lógicos ^[1]. Lógica concerne as verdades que podem ser verificadas usando sistemas lógicos; Metalógica fornece afirmações que podem ser verificadas a partir de linguagens e sistemas que são usados para expressar tais afirmações ^[2]

Os objetos básicos do estudo da metalógica são as linguagens formais, sistemas formais, e suas interpretações. O estudo da interpretação de sistemas formais está no ramo da Lógica Matemática que é conhecida como teoria dos modelos, e os estudos de sistemas dedutivos faz parte do área de conhecimento da Teoria da Prova.

Visão Geral

Linguagem Formal

Ver artigo principal: Linguagens Formais

Uma linguagem formal é uma organização de conjunto de símbolos dos quais define-se precisamente sua forma e conteúdo. Cada linguagem, portanto, pode ser definida sem referência ao significado das expressões; ela pode existir antes que qualquer interpretação possa ser dada para ela - isto é, antes que tenha algum significado. Lógica de primeira ordem é expressa em algumas linguagens formais. A gramática formal determina quais símbolos e conjuntos de símbolos são fórmulas em uma linguagem formal. Uma linguagem formal pode ser formalmente definida como sendo um conjunto A de palavras(sequências finitas) sobre um alfabeto fixo α. Alguns autores, incluindo Carnap, definem a linguagem tal como o par ordenado <α, A>^[3]. Carnap assim explica que para cada elemento de α deve ocorrer pelo menos uma palavra A.

Regras de Formação

Regras de Formação (também chamadas de gramática formal) são uma descrição precisa das fórmulas bem formadas (FBF) de uma linguagem formal. Elas são a base de formação do conjunto de palavras sobre o alfabeto da linguagem formal que constituem fórmulas bem formadas. Entretanto, sem descrever seu significado (isto é, o que elas significam).

Sistemas Formais

Ver artigo principal: Sistema formal

Um sistema formal (também chamado de cálculo lógico, ou sistema lógico) consiste de uma linguagem formal junta com um aparato dedutivo(também chamado sistema dedutivo). O sistema dedutivo pode consistir de um conjunto de regras de transformação (também chamadas de regras de inferência) ou um conjunto de axiomas, ou conter ambos. Um sistema formal é usado para derivar uma expressão de uma ou mais outras expressões. Um sistema formal pode ser formalmente definido como uma tripla ordenada <α,${\displaystyle {\mathcal {I}}}$, ${\displaystyle {\mathcal {D}}}$d>, onde ${\displaystyle {\mathcal {D}}}$ é a relação de derivabilidade direta. Esta relação é entendida em um sentido abrangente de tal modo que sentenças primitivas dos sistemas formais são tomadas como deriváveis diretamente do conjunto vazio de sentenças. Diretamente derivável é a relação entre uma sentença e um conjunto finito, possivelmente vazio de sentenças. Axiomas são então escolhidos de modo que cada membro de primeira colocação de ${\displaystyle {\mathcal {D}}}$d é um membro de ${\displaystyle {\mathcal {I}}}$ e cada membro de segunda colocação é um subconjunto de ${\displaystyle {\mathcal {I}}}$.

Um sistema formal pode também ser definido como somente a relação ${\displaystyle {\mathcal {D}}}$d. Assim, pode-se omitir ${\displaystyle {\mathcal {I}}}$ e α nas definições de linguagem formal interpretada, e sistemas formais interpretados. Contudo, este método pode ser mais difícil de entender e usar.

Provas formais

Ver artigo principal: Prova Formal

Uma prova formal é uma sequência de fórmulas bem formadas de uma linguagem formal, a última da qual é um teorema de sistemas formais. O teorema é uma consequência sintática de todas as fórmulas bem formadas da qual a prova precede. Fórmula bem formada se qualificar como parte da prova, ela deve resultar da aplicação de uma regra de sistema dedutivo de algum sistema formal para as fórmulas bem formadas anteriores na sequência de provas.

Interpretações

Ver artigo principal: Interpretação (lógica)

Ver artigo principal: Semântica formal (lógica)

Uma interpretação de um sistema formal é a assinatura dos significados dos símbolos e o valor-verdade para as sentenças dos sistemas formais. O estudo de interpretações é chamado Semântica Formal. Dada uma interpretação tem-se uma equivalência na construção de um modelo.

Distinções importante em metalógica

Linguagem Objeto-Metalinguagem

Ver artigo principal: Metalinguagem

Ver artigo principal: Linguagem objeto

Em Metalógica, linguagens formais são às vezes chamadas linguagens objeto. A linguagem usada para fazer afirmações sobre um linguagem objeto é chamada uma metalinguagem. A distinção é a diferença chave entre Lógica e Metalógica. Enquanto Lógica lida com provas em um sistema formal, expressada em alguma linguagem formal, Metalógica lida com provas sobre um sistema formal que são expressas em uma metalinguagem sobre alguma linguagem objeto.

Sintaxe e Semântica

Ver artigo principal: Sintaxe (lógica)

Ver artigo principal: Semântica formal (lógica)

Na metalógica 'sintaxe' tem a ver com linguagens formais ou sistemas formais sem fazer referência a qualquer interpretação delas; por outro lado, 'semântica' tem a ver com as interpretações de linguagens formais. O termo sintaxe tem um escopo um pouco mais largo que "prova teórica", desde que ele possa ser aplicado a propriedades de linguagens formais sem quaisquer sistemas dedutivos, nem tampouco sistemas formais. 'Semântica' é sinônimo de 'modelo teórico'.

História

Questões metalógicas tem sido perguntadas desde o tempo de Aristóteles. Contudo, foi só com o surgimento de linguagens formais no final do século XIX e início do século XXque investigações nas fundações de lógica começaram a florescer. Em 1904, David Hilbert investigando fundamentos matemáticos descobriu que noções lógicas são pressupostos, e portanto um acordo simultâneo de princípios matemáticos e metalógicos foi adquirido. Hoje, Metalógica e Metamatemática são largamente afins uma com a outra, e ambas tem sido substancialmente inserida pela Matemática e Lógica na academia. Uma possível alternativa, de um modelo menos matemático pode ser encontrado em Charles Sanders Peirce e outros semióticos. Embora Semióticos possam ser interpretados pela linguística, outra interpretação é a que trata de símbolos universais, de acordo com Carl Jung.

Referências em Metalógica

Referências em Metalógica consiste de cada assunto com provas formais, demonstrando a consistência, completude e decidibilidade de sistemas formais particulares.

Maiores resultados em metalógica incluem:

• Prova da não-enumerabilidade dos conjuntos de todos os subconjuntos do conjunto dos números naturais (Teorema de Cantor 1891)
• Teorema de Löwenheim-Skolem (Leopold Löwenheim 1915 and Thoralf Skolem 1919)
• Prova da consistência da lógica proposicional vero-funcional (Emil Post 1920)
• Prova da decidibilidade da lógica proposicional vero-funcional (Emil Post 1920)
• Prova da completude semântica da lógica proposicional vero-funcional (Paul Bernays 1918)^[4] ,(Emil Post 1920)^[2]
• Prova da completude sintática da lógica proposicional vero-funcional (Emil Post 1920)
• Prova da consistência da lógica de predicados monádica de primeira ordem (Leopold Löwenheim 1915)
• Prova da consistência da lógica de predicados de primeira ordem (David Hilbert and Wilhelm Ackermann 1928)
• Prova da completude semântica da lógica de predicados de primeira ordem (teorema da completude de Gödel 1930)
• Prova da indecidibilidade da lógica de predicados de primeira ordem (teorema de Church 1936)
• Primeiro Teorema da Incompletude de Gödel 1931
• Segundo Teorema da Incompletude de Gödel 1931
• Teorema da indefinibilidade de Tarski (Gödel e Tarski nos anos 1930s)

Referências