Lógica de Primeira Ordem e Completude

A lógica de primeira ordem é a linguagem formal de declarações quantificadas sobre objetos e relações, e o teorema da completude de Goedel mostra que seu sistema de prova captura exatamente as sentenças verdadeiras em todas as interpretações.

Definition

A lógica de primeira ordem estende a lógica proposicional com quantificadores que abrangem um domínio de objetos, juntamente com símbolos de relação, função e constante; o teorema da completude afirma que uma sentença é derivável em seu sistema de prova precisamente quando é uma consequência lógica dos axiomas assumidos.

Scope

Este tópico abrange a sintaxe das linguagens de primeira ordem, termos, fórmulas e sentenças, a semântica de estruturas e satisfação, as noções de validade e consequência lógica, um sistema dedutivo para a lógica de primeira ordem, e os teoremas de correção e completude que relacionam a provabilidade à verdade.

Core questions

• Qual é a sintaxe e a semântica precisas da lógica de primeira ordem?
• O que significa para uma sentença ser uma consequência lógica de uma teoria?
• Por que toda sentença válida é formalmente provável?
• Como a completude conecta o sistema de prova à classe de todos os modelos?

Key theories

Teorema da correção

Toda sentença derivável no sistema de prova é verdadeira em todo modelo das premissas, de modo que o sistema dedutivo nunca prova consequências falsas.

Teorema da completude de Goedel

Inversamente, toda sentença que se mantém em todos os modelos de uma teoria é derivável dela, de modo que a provabilidade e a consequência lógica coincidem para a lógica de primeira ordem.

Construção de Henkin

A completude é provada construindo um modelo diretamente a partir de um conjunto consistente maximal de sentenças com testemunhas para declarações existenciais, fornecendo uma receita sintática para a construção de modelos.

Clinical relevance

A lógica de primeira ordem é o arcabouço padrão para formalizar teorias matemáticas, e a completude garante que qualquer verdade semântica comum a todos os modelos pode, em princípio, ser provada, sustentando a prova automatizada de teoremas e a adequação fundamental dos sistemas axiomáticos.

History

A lógica de primeira ordem emergiu da Begriffsschrift de Frege e foi isolada como um sistema distinto por Hilbert e Ackermann. Goedel provou a completude em sua dissertação de doutorado de 1929, e a construção de Henkin de 1949 forneceu a prova simplificada usando conjuntos consistentes maximais que é padrão hoje.

Key figures

• Gottlob Frege
• Kurt Goedel
• Leon Henkin
• Alfred Tarski

Seminal works

• enderton2001
• marker2002
• shoenfield1967

Frequently asked questions

Como a completude difere dos teoremas da incompletude de Goedel?

A completude trata da consequência lógica: toda sentença verdadeira em todos os modelos de uma teoria é provável. A incompletude trata de uma teoria específica: uma teoria consistente suficientemente forte possui sentenças verdadeiras em seu modelo pretendido que ela não pode provar. Os dois conceitos abordam noções diferentes e não estão em conflito.

Por que a lógica de primeira ordem é a escolha padrão?

É expressiva o suficiente para formalizar a maior parte da matemática, mas desfruta de completude e compacidade, que falham para lógicas mais fortes, como a lógica de segunda ordem. Esse equilíbrio entre expressividade e boas propriedades metateóricas a torna o arcabouço lógico padrão.