Lógica infinitária

Uma lógica infinitária é uma lógica que permite declarações infinitamente longas e/ou provas infinitamente longas. Algumas lógicas infinitárias podem ter propriedades diferentes da lógica de primeira ordem comum. Em particular, lógicas infinitárias podem falhar em serem compactas ou completas. Noções de compacto ou completo que são equivalentes na lógica finitária, nem sempre o são na lógica infinitária. Portanto para lógicas infinitárias as noções de compacidade forte e completude forte são definidas. Esse artigo trata das logicas infinitárias do tipo Hilbert, pois essas foram extensivamente estudadas e constituem a extensão mais direta da lógica finitária. Porém, essas não as únicas lógicas infinitárias que foram formuladas ou estudadas.

Considerar se uma determinada lógica infinitária nomeada Ω-logic está completa promete ajudar a entender a hipótese do continuum.

Sobre notação e o axioma de escolha

Quando uma linguagem com formulas infinitamente longas é apresentada, não é possível escrever expressões da maneira que elas deveriam ser escritas. Para contornar esse problema, várias “conveniências notacionais”, que, estritamente falando, não fazem parte da linguagem formal, são usadas. $\cdots$ é usado para pontuar uma expressão que é infinitamente longa. Onde não ficar claro, o tamanho da sequência é colocado em notação depois. Onde essa notação se tornar ambígua ou confusa, sufixos como $\lor _{\gamma <\delta }{A_{\gamma }}$ são usados para indicar uma “disjunção infinita” sobre um conjunto de fórmulas de cardinalidade $\delta$. A mesma notação pode ser aplicada a quantificadores, por exemplo $\forall _{\gamma <\delta }{V_{\gamma }:}$. O significado disso é representar uma sequência infinita de quantificadores para cada $V_{\gamma }$ onde $\gamma <\delta$. Todo uso de sufixos e $\cdots$ não fazem parte das linguagens infinitárias formais. O “Axioma da escolha” é presumido (como frequentemente acontece quando se discute lógica infinitária) já que isso é necessário para ter leis distributivas sensatas.

Definição de lógicas infinitárias do tipo Hilbert

Uma lógica infinitária de primeira ordem L_α,β, α regular β = 0 ou ω ≤ β ≤ α, usa o mesmo grupo de símbolos que uma lógica finitária e pode usar todas as regras para a formação de formulas da lógica finitária, junto com mais algumas:

• Dado um grupo de variáveis $V=\{V_{\gamma }|\gamma <\delta <\beta \}$ e a fórmula $A_{0}$ então $\forall V_{0}:\forall V_{1}\cdots (A_{0})$ e $\exists V_{0}:\exists V_{1}\cdots (A_{0})$ são fórmulas (Em cada caso a sequência tem comprimento $\delta$).
• Dado um grupo de fórmulas $A=\{A_{\gamma }|\gamma <\delta <\alpha \}$ então $(A_{0}\lor A_{1}\lor \cdots )$ e $(A_{0}\land A_{1}\land \cdots )$ são fórmulas (em cada caso a sequência tem comprimento $\delta$).

Os conceitos de variáveis ligadas, se aplica da mesma maneira em infinitas sentenças. Note que o número de chaves nessas fórmulas é sempre finito. Assim como na lógica finitária, uma fórmula em que todas as variáveis estão ligadas é conhecida como sentença.

Uma teoria T em lógica infinitária $L_{\alpha ,\beta }$ é um grupo de declarações nessa lógica. Uma prova em lógica infinitária de uma teoria T é uma sequencia de declarações de comprimento $\gamma$ que obedece as seguintes condições: cada declaração pode ser um “axioma lógico”, um elemento de T, ou é deduzido de declarações prévias usando uma regra de interferência. Como antes, todas as regras de interferência da lógica finitária podem ser usadas, junto com mais uma:

• Dado um grupo de declarações $A=\{A_{\gamma }|\gamma <\delta <\alpha \}$ que tenham ocorrido previamente na prova, então a declaração $\land _{\gamma <\delta }{A_{\gamma }}$ pode ser inferida.

Os esquemas de “axiomas lógicos” especificos para lógica infinitária estão representados abaixo. Esquema global de variáveis: $\delta$ e $\gamma$ tais que $0<\delta <\alpha$.

• $((\land _{\epsilon <\delta }{(A_{\delta }\implies A_{\epsilon })})\implies (A_{\delta }\implies \land _{\epsilon <\delta }{A_{\epsilon }}))$
• Para cada $\gamma <\delta$, $((\land _{\epsilon <\delta }{A_{\epsilon }})\implies A_{\gamma })$
• Leis distributivas de Chang (para cada $\gamma$): $(\lor _{\mu <\gamma }{(\land _{\delta <\gamma }{A_{\mu ,\delta }})})$, onde $\forall \mu \forall \delta \exists \epsilon <\gamma :A_{\mu ,\delta }=A_{\epsilon }$ ou $A_{\mu ,\delta }=\neg A_{\epsilon }$, e $\forall g\in \gamma ^{\gamma }\exists \epsilon <\gamma :\{A_{\epsilon },\neg A_{\epsilon }\}\subseteq \{A_{\mu ,g(\mu )}:\mu <\gamma \}$
• Para $\gamma <\alpha$, $((\land _{\mu <\gamma }{(\lor _{\delta <\gamma }{A_{\mu ,\delta }})})\implies (\lor _{\epsilon <\gamma ^{\gamma }}{(\land _{\mu <\gamma }{A_{\mu ,\gamma _{\epsilon }(\mu )})}}))$, onde $\{\gamma _{\epsilon }:\epsilon <\gamma ^{\gamma }\}$ é uma boa ordenação de $\gamma ^{\gamma }$

Os últimos dois esquemas de axioma requerem o axioma de escolha porque certos grupos devem ser bem ordenada. O ultimo esquema de axioma é desnecessário, estritamente falando, pois as leis distributivas de Chang o implica isso, no entanto é incluído como uma maneira natural de permitir enfraquecimentos naturais na lógica.

Completude, compacidade e completude forte

Uma teoria é qualquer grupo de declarações. A verdade de declarações em modelos é definida por recursividade e irá concordar com a definição da lógica finitária onde ambos são definidos. Dada uma teoria T uma declaração é dita válida para essa teoria se for verdadeira em todos os modelos de T.

Uma lógica $L_{\alpha ,\beta }$ é completa se para cada sentença S válida em cada modelo dela existir uma prova de S. É fortemente completa se para qualquer teoria T para cada sentença S válida em T existir uma prova de S vindo de T. Uma lógica infinitária pode ser completa sem ser fortemente completa.

Um cardinal $\kappa \neq \omega$ é um cardinal fracamente compacto quando para cada teoria T em $L_{\kappa ,\kappa }$ contendo no máximo $\kappa$ fórmulas, se cada S $\subseteq$ T de cardinalidade menor que $\kappa$ tem um modelo, então T tem um modelo. Um cardinal $\kappa \neq \omega$ é um cardinal fortemente compacto quando para cada teoria T em $L_{\kappa ,\kappa }$, sem restrição de tamanho, se cada S $\subseteq$ T de cardinalidade menor que $\kappa$ tem um modelo, então T tem um modelo.

Conceitos expressivos na lógica infinitária

Na linguagem de teoria de grupo a seguinte declaração expressa regularidade:

$\forall _{\gamma <\omega }{V_{\gamma }:}\neg \land _{\gamma <\omega }{V_{\gamma +}\in V_{\gamma }}.\,$

Diferente do axioma da regularidade, essa declaração não admite interpretações não-padrão. O conceito de bem fundado pode ser expresso apenas numa lógica que permita infinitos quantificadores numa declaração individual. Como consequência muitas teorias, incluindo Aritmética de Peano, que não podem ser propriamente transformadas em axiomas na lógica finitária podem o ser na lógica infinitária. Outros exemplos incluem as teorias de Propriedade arquimediana e torção. Essas três teorias podem ser definidas sem o uso de quantificação infinita; apenas junções infinitas são necessárias.

Lógicas infinitárias completas

Duas lógicas infinitárias se destacam por sua completude. Elas são $L_{\omega ,\omega }$ e $L_{\omega _{1},\omega }$. A primeira é lógica finitária padrão e a segunda é uma lógica infinitária que só permite declarações de tamanho contável.

$L_{\omega ,\omega }$ também é fortemente completa, compacta e fortemente compacta.

$L_{\omega _{1},\omega }$ falha em ser compacta, mas é completa (sob os axiomas dados acima). Alem disso, satisfaz uma variante da propriedade interpolação de Craig.

$L_{\alpha ,\alpha }$ é completa (sob os axiomas dados acima) sempre que $\alpha$ é inacessível. Só será fortemente completo se $\alpha$ for fortemente compacto (pois provas nessas lógicas não podem usar $\alpha$ ou mais dos axiomas dados).