無限論理
数理論理学または順序数の概念に詳しくない者はまずそちらの記事を参考にすることが推奨される。
無限論理 (むげんろんり、infinitary logic) は、無限に長い言明および/または無限に長い証明を許す論理である。
いくつかの無限論理は標準的な一階述語論理とは異なる性質を持つ。特に、無限論理はコンパクト性や完全性を満たさないことが多い。コンパクト性や完全性の概念は、有限論理においては等価であることもあるが、無限論理においてはそうではない。無限論理においては強いコンパクト性や強い完全性の概念が定義される。この記事では、ヒルベルト型無限論理について主に述べる。この型はかなり研究されてきており、有限論理の最も直接的な拡張を構成している。しかしながら、これらは形式化されているまたは研究対象となっている唯一の無限論理ではない。
Ω論理という無限論理が完全かどうかを考察することは連続体仮説の解明につながる。
無限に長い式・句を伴う言語が存在すると、全ての式を書き下すことは不可能である。この問題を避けるには、多くの都合の良い表記法が使われる。これらの表記法自体は厳密に言うと形式言語の一部ではない。\cdotsは無限に長い式を表すために用いられる。それが明確ではないところでは、式の列の長さが後で記される。この表記法は曖昧で紛らわしいので、濃度\deltaの式の集合の無限の論理和を示すために、\lor_{\gamma < \delta}{A_{\gamma}のような添字が用いられる。同じ表記法が、例えば\forall_{\gamma < \delta}{V_{\gamma}:}のような量化子に応用されることもある。これは各V_{\gamma}に対する量化子の無限列を表すことを意味する。ここで\gamma < \deltaである。
添字および\cdotsの使用法は全て形式無限言語の一部ではない。選択公理は(無限論理が議論されたときによくなされるのだが)実用的な分配性法則を持つために必須であるとして仮定される。
一階無限論理Lα,β、ここでαは正則、β = 0 または ω ≤ β ≤ α、は有限論理と同じ記号の集合を持っており、有限論理の式の形成についての全ての規則といくつかの追加規則を用いる:
変数V=\{V_\gamma | \gamma< \delta < \beta \}および式A_0の集合について、\forall V_0 :\forall V_1 \cdots (A_0)および\exists V_0 :\exists V_1 \cdots (A_0)は式である(それぞれの場合に量化子の列は長さ\deltaを持つ)。
式A=\{A_\gamma | \gamma < \delta <\alpha \}の集合について、(A_0 \lor A_1 \lor \cdots)および(A_0 \land A_1 \land \cdots)は式である(それぞれの場合に列は長さ\deltaを持つ)。
束縛変数の概念は、同様の方法で無限文にも適用される。これらの式における括弧の数は常に有限であることに注意。有限論理と同じように、全ての変数が束縛されている式は文と呼ばれる。
無限論理L_{\alpha , \beta}における理論Tは、その論理における言明の集合である。理論Tからの無限論理における証明は以下の条件に従う長さ\gammaの文の列である:各文は論理的な公理Tの要素であるか、または推論規則を用いて過去の言明から推論(演繹)される。前述のものと同様に、無限論理における全ての推論規則と追加規則を用いることができる:
その証明において以前に生じている言明A=\{A_\gamma | \gamma < \delta <\alpha \}の集合を持つとき、その言明\land_{\gamma < \delta}{A_{\gamma}は推論可能である。
無限論理に特徴的な論理的公理型を以下に与える。0 < \delta < \alpha のような各\deltaおよび\gammaについて、以下の論理的公理を持つ:
((\land_{\epsilon < \delta}{(A_{\delta} \implies A_{\epsilon})}) \implies (A_{\delta} \implies \land_{\epsilon < \delta}{A_{\epsilon}))。
各\gamma < \deltaについて、((\land_{\epsilon < \delta}{A_{\epsilon}) \implies A_{\gamma})である。
Changの分配性法則(各\gammaについて):(\lor_{\mu < \gamma}{(\land_{\delta < \gamma}{A_{\mu , \delta})})。ここで、\forall \mu : \forall \delta : \exists \epsilon < \gamma:A_{\mu , \delta} = A_{\epsilon} and \forall g \in \gamma^{\gamma} : \exists \epsilon < \gamma: \{A_{\epsilon} , \neg A_{\epsilon}\} \subseteq \{A_{\mu , g(\mu)} : \mu < \gamma\}。
\gamma < \alphaについて、((\land_{\mu < \gamma}{(\lor_{\delta < \gamma}{A_{\mu , \delta})}) \implies (\lor_{\epsilon < \gamma^{\gamma}{(\land_{\mu < \gamma}{A_{\mu ,\gamma_{\epsilon})}))。ここで、\gamma_{\epsilon}は\gamma^{\gamma}の整列である。
特定の集合は整列可能でなくてはならないので、最後の二つの公理型は選択公理を必要とする。 Changの分配性法則が暗示するように最後の公理型は厳密に言うと不要である。しかしながら、それは自然な論理の弱化を許す自然な方法として含まれる。
ある理論は言明のあらゆる集合である。モデルにおける言明の真理は再帰によって定義され、両方が定義されるところの有限論理に対する定義と一致する。理論Tが仮定されると、ある言明はTの全てのモデルにおいて真ならば理論Tに対して妥当(恒真)であると言われる。
論理L_{\alpha , \beta}は、全てのモデルにおいて妥当な全ての文SについてSの証明が存在するならば完全である。Tにおいて妥当な全ての文Sに関するどんな理論Tについても、TからのSの証明が存在するならば、それは強く完全である。無限論理は強く完全でなくても完全であり得る。
濃度\alphaの全ての理論Tについて、Tの全ての部分集合Sがモデルを持つならばTはモデルを持つとき、論理はコンパクトである。全ての理論Tについて、Tの全ての部分集合Sがモデルを持つならばTはモデルを持つとき、論理は強くコンパクトである。 ここで、Sは濃度< \alphaを持つ。もし論理が強くコンパクトかつ完全であるなら、強く完全である。
L_{\kappa , \kappa}がコンパクトであるなら、濃度 \kappa \neq \omega は弱くコンパクトである。また、L_{\kappa , \kappa}が強くコンパクトなら、\kappaは強くコンパクトである。
集合論の言語において、以下の言明は正則性公理(基礎の公理)を表現する:
\forall_{\gamma < \omega}{V_{\gamma}:} \neg \land_{\gamma < \omega}{V_{\gamma +} \in V_{\gamma}.\,
基礎の公理と違って、この言明は非標準の解釈を認めない。整礎性の概念は、個別の言明に無限に多くの量化子を許す論理においてのみ表現できる。その結果、有限論理においては適切に公理化できないペアノ算術を含む多くの理論は適切な無限論理において存在することができる。他の例は非アルキメデス体および捻れのない群の理論を含む。これら三つの群は無限の量化子なしで定義することができる。ここではただ無限の連結が必要となる。
二つの無限論理は特に完全性が際立っている。それらは、L_{\omega , \omega}とL_{\omega_1 , \omega}である。前者は標準的な有限一階論理で、後者は可算サイズの言明だけを許す無限論理である。
L_{\omega , \omega}もまた強く完全、コンパクト、そして強くコンパクトである。