teoria consistente ω - ω-consistent theory
Na lógica matemática , uma teoria ω-consistente (ou ômega-consistente , também chamada numericamente segregativa ) é uma teoria (coleção de sentenças ) que não é apenas (sintaticamente) consistente (ou seja, não prova uma contradição ), mas também evita provando certas combinações infinitas de sentenças que são intuitivamente contraditórias. O nome é devido a Kurt Gödel , que introduziu o conceito no decorrer da prova do teorema da incompletude .
Definição
Diz-se que uma teoria T interpreta a linguagem da aritmética se houver uma tradução das fórmulas da aritmética para a linguagem de T de modo que T seja capaz de provar os axiomas básicos dos números naturais sob essa tradução.
Um T que interpreta a aritmética é ω-inconsistente se, para alguma propriedade P de números naturais (definida por uma fórmula na linguagem de T ), T prova P (0), P (1), P (2), e assim por diante (isto é, para cada número natural padrão n , T prova que P ( n ) é válido), mas T também prova que existe algum número natural n (necessariamente não padrão) tal que P ( n ) falha . Isto pode não gerar uma contradição dentro T porque T pode não ser capaz de provar para qualquer determinado valor de n que P ( n ) falhar, mas apenas que não é tal n .
T é ω-consistente se for não ω-inconsistente.
Existe uma propriedade mais fraca, mas intimamente relacionada, da sonoridade Σ 1 . Uma teoria T é Σ 1 -som (ou 1-consistente , em outra terminologia) se cada Σ 0 1 -sentência provável em T é verdadeira no modelo padrão da aritmética N (ou seja, a estrutura dos números naturais usuais com adição e multiplicação). Se T for forte o suficiente para formalizar um modelo razoável de computação , Σ 1 -sondagem é equivalente a exigir que sempre que T provar que uma máquina de Turing C para , então C realmente para. Toda teoria consistente com ω é som Σ 1 , mas não vice-versa.
De maneira mais geral, podemos definir um conceito análogo para níveis superiores da hierarquia aritmética . Se Γ é um conjunto de sentenças aritméticas (tipicamente Σ 0 n para algum n ), uma teoria T é Γ-sólida se todas as sentence sentenças prováveis em T forem verdadeiras no modelo padrão. Quando Γ é o conjunto de todas as fórmulas aritméticas, a integridade Γ é chamada de integridade (aritmética) justa. Se a linguagem de T consiste apenas na linguagem da aritmética (em oposição, por exemplo, à teoria dos conjuntos ), então um sistema de som é aquele cujo modelo pode ser pensado como o conjunto ω, o conjunto usual de números naturais matemáticos. O caso de T geral é diferente, consulte a lógica ω abaixo.
A sonoridade n tem a seguinte interpretação computacional: se a teoria prova que um programa C usando um oráculo Σ n −1 - para , então C realmente para.
Exemplos
Teorias consistentes e inconsistentes em ω
Escreva PA para a teoria aritmética de Peano e Con (PA) para a declaração da aritmética que formaliza a afirmação "PA é consistente". Con (PA) poderia ter a forma "Para todo número natural n , n não é o número de Gödel de uma prova de PA de que 0 = 1". (Esta formulação usa 0 = 1 em vez de uma contradição direta; isso dá o mesmo resultado, porque PA certamente prova ¬0 = 1, então se fosse 0 = 1 também teríamos uma contradição, e por outro lado, se PA prova uma contradição, então prova qualquer coisa , incluindo 0 = 1.)
Agora, assumindo que PA é realmente consistente, segue-se que PA + ¬Con (PA) também é consistente, pois se não fosse, então PA provaria Con (PA) ( reductio ), contradizendo o segundo teorema da incompletude de Gödel . No entanto, PA + ¬Con (PA) não é consistente com ω. Isso ocorre porque, para qualquer número natural particular n , PA + ¬Con (PA) prova que n não é o número de Gödel de uma prova de que 0 = 1 (o próprio PA prova esse fato; a suposição extra ¬Con (PA) não é necessário). No entanto, PA + ¬Con (PA) prova que, para algum número natural n , n é o número de Gödel de tal prova (esta é apenas uma reformulação direta da afirmação ¬Con (PA)).
Neste exemplo, o axioma ¬Con (PA) é Σ 1 , portanto, o sistema PA + ¬Con (PA) é de fato Σ 1 -unsound, não apenas ω-inconsistente.
Teorias aritmeticamente sólidas e inconsistentes com ω
Seja T PA junto com os axiomas c ≠ n para cada número natural n , onde c é uma nova constante adicionada à linguagem. Então T é aritmeticamente correto (como qualquer modelo não padrão de PA pode ser expandido para um modelo de T ), mas ω-inconsistente (como prova , e c ≠ n para cada número n ).
Σ 1 -Sound teorias ω-inconsistentes usando apenas a linguagem da aritmética pode ser construído como segue. Seja I Σ n a subteoria de PA com o esquema de indução restrito a Σ n- fórmulas, para qualquer n > 0. A teoria I Σ n + 1 é finitamente axiomatizável, seja A , portanto, seu único axioma, e considere a teoria T = I Σ n + ¬ Uma . Podemos supor que A é uma instância do esquema de indução, que tem a forma
Se denotarmos a fórmula
por P ( n ), então para cada número natural n , a teoria T (na verdade, mesmo o cálculo de predicado puro) prova P ( n ). Por outro lado, t prova a fórmula , porque é logicamente equivalente ao axioma ¬ Uma . Portanto, T é ω-inconsistente.
É possível mostrar que T é Π n + 3 -som. Na verdade, é Π n + 3 - conservador sobre a (obviamente sólida) teoria I Σ n . O argumento é mais complicado (ele se baseia na comprovação do princípio de Σ n + 2 -reflecção para I Σ n em I Σ n + 1 ).
Teorias aritmeticamente incorretas e consistentes com ω
Seja ω-Con (PA) a sentença aritmética formalizando a afirmação "PA é consistente com ω". Então, a teoria PA + ¬ω-Con (PA) é incorreta (Σ 3 -inferior, para ser preciso), mas consistente em ω. O argumento é semelhante ao primeiro exemplo: uma versão adequada das condições de derivabilidade de Hilbert-Bernays-Löb vale para o "predicado de provabilidade" ω-Prov ( A ) = ¬ω-Con (PA + ¬ A ), portanto, satisfaz um análogo do segundo teorema da incompletude de Gödel.
ω-lógica
O conceito de teorias da aritmética cujos inteiros são os verdadeiros inteiros matemáticos é capturado pela lógica ω . Seja T uma teoria em uma linguagem contável que inclui um símbolo predicado unário N destinado a conter apenas os números naturais, bem como nomes especificados 0, 1, 2, ..., um para cada número natural (padrão) (que podem ser constantes separadas ou termos constantes, como 0, 1, 1 + 1, 1 + 1 + 1, ..., etc.). Observe que o próprio T pode estar se referindo a objetos mais gerais, como números reais ou conjuntos; assim, em um modelo de T, os objetos que satisfazem N ( x ) são aqueles que T interpreta como números naturais, e nem todos precisam ser nomeados por um dos nomes especificados.
O sistema da lógica ω inclui todos os axiomas e regras da lógica usual de predicados de primeira ordem, juntamente com, para cada fórmula T P ( x ) com uma variável livre especificada x , uma regra ω infinitária da forma:
- De inferir .
Ou seja, se a teoria afirma (ou seja, prova) P ( n ) separadamente para cada número natural n dado por seu nome especificado, então ela também afirma P coletivamente para todos os números naturais de uma vez por meio da contraparte evidente finita universalmente quantificada do infinito antecedentes da regra. Para uma teoria da aritmética, significando uma com o domínio pretendido dos números naturais, como a aritmética de Peano , o predicado N é redundante e pode ser omitido da linguagem, com o consequente da regra para cada P simplificando para .
Um modelo ω de T é um modelo de T cujo domínio inclui os números naturais e cujos nomes especificados e o símbolo N são interpretados de forma padronizada, respectivamente como esses números e o predicado tendo apenas esses números como seu domínio (de onde não há números não padronizados) . Se N estiver ausente da linguagem, então o que seria o domínio de N deve ser o do modelo, ou seja, o modelo contém apenas os números naturais. (Outros modelos de T podem interpretar esses símbolos de forma não padronizada; o domínio de N nem precisa ser contável, por exemplo.) Esses requisitos fazem a regra ω soar em cada modelo ω. Como corolário do teorema da omissão de tipos , o inverso também é válido: a teoria T tem um modelo ω se e somente se for consistente na lógica ω.
Há uma conexão estreita entre a lógica ω e a consistência ω. Uma teoria consistente na lógica ω também é consistente ω (e aritmeticamente correta). O inverso é falso, pois a consistência na lógica ω é uma noção muito mais forte do que a consistência ω. No entanto, a seguinte caracterização é válida: uma teoria é consistente com ω se e somente se seu fechamento sob aplicações não aninhadas da regra ω for consistente.
Relação com outros princípios de consistência
Se a teoria T é axiomatizável recursivamente , a consistência ω tem a seguinte caracterização, devido a Craig Smoryński :
- T é consistente com ω se e somente se for consistente.
Aqui, é o conjunto de todas as Π 0 2 -sentências válido no modelo padrão da aritmética, e é o princípio de reflexão uniforme para T , que consiste nos axiomas
para cada fórmula com uma variável livre. Em particular, uma teoria finitamente axiomatizável T na linguagem da aritmética é consistente com ω se e somente se T + PA é -som.
Notas
- ^ WVO Quine (1971), Set Theory and Its Logic .
- ^ Smorynski, "The incompleteness teoreems", Handbook of Mathematical Logic , 1977, p. 851.
- ^ A definição deste simbolismo pode ser encontrada na hierarquia aritmética .
- ^ J. Barwise (ed.), Handbook of Mathematical Logic , Norte-Holland, Amsterdã, 1977.
- ^ Smoryński, Craig (1985). Auto-referência e lógica modal . Berlim: Springer. ISBN 978-0-387-96209-2 . Revisado em Boolos, G .; Smorynski, C. (1988). “Auto-referência e lógica modal”. The Journal of Symbolic Logic . 53 : 306. doi : 10.2307 / 2274450 . JSTOR 2274450 .
Bibliografia
- Kurt Gödel (1931). «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I». Em Monatshefte für Mathematik . Traduzido para o inglês como On Formally Undecidable Propositions of Principia Mathematica and Related Systems .