Em lógica matemática, uma teoria (também chamada de teoria formal) é um conjunto de sentenças em uma linguagem formal. Normalmente um sistema dedutivo é entendido do contexto. Um elemento de uma teoria é chamado de axioma da teoria, e cada sentença que segue do axioma () é chamado de teorema da teoria. Todo axioma também é um teorema. Uma teoria de primeira ordem é um conjunto de sentenças de primeira ordem.
Quando se definem teorias, deve-se tomar cuidado adicional e uma linguagem normal de teoria dos conjuntos pode não ser apropriada.
A construção da teoria começa especificando uma classe conceitual não-vazia, com seus elementos sendo chamados de afirmações. Essas afirmações iniciais são comumente chamadas de elementos primitivos ou afirmações elementares da teoria, para distingui-las de outras afirmações que possam ser derivadas delas.
Uma teoria é uma classe conceitual que consiste de algumas dessas afirmações elementares. As afirmações elementares que pertencem à são chamadas de teoremas elementares de e ditos verdadeiros. Desse modo, uma teoria é uma forma de designar um subconjunto que consiste inteiramente de afirmações verdadeiras.
Essa forma geral de designar uma teoria estipula que a verdade de qualquer um de seus elementos não é sabida sem uma referência à . Portanto a mesma afirmação pode ser verdade em relação à uma teoria, e falsa em relação à outra. Isso em linguagem ordinária, em que afirmações do tipo "Ele é uma pessoa terrível" não podem ser julgadas falsas ou verdadeiras sem uma referência a alguma interpretação de quem é "Ele" e o que é "pessoa terrível" nessa teoria.[1]
Uma teoria S é uma subteoria de uma teoria T se S é um subconjunto de T. Se T é um subconjunto de S então S é uma extensão ou superteoria de T.
Uma teoria é dita ser uma teoria dedutiva se é uma classe indutiva. Isto é, que seu conteúdo é baseado em algum sistema de dedução formal e que alguma de suas afirmações elementares são tomadas como axiomas. Em uma teoria dedutiva, qualquer sentença que é uma consequência lógica de um ou mais de um axioma também é uma sentença dessa teoria.[1]
Uma teoria sintaticamente consistente é uma teoria na qual nem toda sentença na linguagem subjacente pode ser provada (com respeito a algum sistema dedutivo que geralmente está claro no contexto). Em um sistema dedutivo (como a lógica de primeira ordem) que satisfaça o princípio de explosão, isso é equivalente a requerer que não exista sentença φ tal que φ e sua negação possam ser provadas a partir dessa teoria.
Uma teoria satisfatível é uma teoria que tem um modelo. Isso significa que existe uma estrutura M que satisfaz toda sentença na teoria. Qualquer teoria satisfatível é sintaticamente consistente, pois, para cada sentença φ,a estrutura que satisfaz a teoria satisfará exatamente φ ou a negação de φ.
Uma teoria consistente é por vezes definida como uma teoria sintaticamente consistente, e por vezes definida como uma teoria satisfatível. Para a lógica de primeira ordem, o caso mais importante, a partir do teorema da completude, segue que os dois sentidos coincidem. Em outras lógicas, tal qual a lógica de segunda ordem, existem teorias sintaticamente consistentes que não são satisfatíveis, como teorias ω-inconsistentes.
Uma teoria completa é uma teoria consistente T tal que para cada sentença φ em sua linguagem, ou φ é provável em T ou T {φ} é inconsistente. Para teorias fechadas sob a consequência lógica, isso significa que para cada sentença φ, φ ou a negação de φ estão contidas na teoria. Uma teoria incompleta é uma teoria consistente que não é completa.
Cada estrutura tem várias teorias associadas. A teoria completa de uma estrutura A é o conjunto de todas as sentenças de primeira ordem na assinatura de A que são satisfatíveis em A, denotadas por Th(A). De uma forma mais geral, a teoria de K, uma classe de σ-estruturas, é o conjunto de todas as σ-sentenças de primeira ordem que são satisfatíveis por todas as estruturas em K, denotado por Th(K). Claramente Th(A) = Th({A}). Essas noções também podem ser definidas com relação a outros tipos de lógica que não a de primeira ordem.
O diagrama de A consiste de todas as sentenças atômicas ou negação de sentenças atômicas que são satisfeitas por A e é denotado por diagA. O diagrama positivo de A é o conjunto de todas as σ'-sentenças atômicas que são satisfeitas por A e é denotado por diag+A. O diagrama elementar de A é o conjunto eldiagA de todas as σ'-sentenças de primeira ordem que são satisfeitas por A ou, equivalentemente,