Q0（数理論理学）

Q ₀はピーター・アンドリュースによる単純型付きラムダ計算の定式化であり、一階述語論理と集合論を組み合わせた数学の基礎を提供する。これは高階論理の一種であり、 HOL定理証明器ファミリーの論理と密接に関連している。

定理証明システムTPSとETPS（Wayback Machineに2011年4月11日にアーカイブ）はQ ₀ に基づいています。2009年8月、TPSは高階定理証明システム間の初のコンペティションで優勝しました。^[¹^]

_{Q 0}の公理

このシステムには、次のように述べることができる 5 つの公理があります。

$(1)$ $g_{oo}T\land g_{oo}F=\forall x_{o}[g_{oo}x_{o}]$

$(2^{\alpha })$ $[x_{\alpha }=y_{\alpha }]\supset [h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }]$

$(3^{\alpha \beta })$ $f_{\alpha \beta }=g_{\alpha \beta }=\forall x_{\beta }[f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\beta }]$

$(4)$ $[\lambda \mathbf {x_{\alpha }} \mathbf {B} _{\beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }}^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta }$

$(5)$ ℩ $_{i(oi)}[{\text{Q}}_{oii}y_{i}]=y_{i}\,$

(公理 2、3、4 は公理スキーマ、つまり類似の公理のファミリーです。公理 2 と公理 3 のインスタンスは変数と定数の型のみが異なりますが、公理 4 のインスタンスではAとBを置き換える任意の式を持つことができます。)

添え字付きの「o」はブール値の型記号であり、添え字付きの「i」は個々の（ブール値ではない）値の型記号です。これらの並びは関数の型を表し、異なる関数の型を区別するために括弧を含めることができます。添え字付きのギリシャ文字（α、βなど）は型記号の構文変数です。太字の大文字（ $A$ 、 $B$ 、 $C$ など）はWFFの構文変数であり、太字の小文字 $（x$ 、 $y$ など）は変数の構文変数です。S $は、$ すべての自由出現における構文置換を示します。

プリミティブ定数は $Q ((oα)α)$ （各型αの要素の等価性を表す）と $℩ (i(oi))$ （個体の記述演算子、つまり個体を1つだけ含む集合の唯一の要素を表す）のみである。記号 λ と括弧 (“"[” と “]”) は言語の構文である。その他の記号は、これらを含む用語の略語であり、量指定子 ∀ と ∃ も含まれる。

公理 4 では、 $B$ 内の $Aに対して$ $x は$ 自由でなければなりません。つまり、置換によって、 $A$ の自由変数の出現が置換の結果に束縛されることはありません。

公理について

$公理 1 は、 T$ と $F が$ 唯一のブール値であるという考えを表現します。
公理スキーマ 2 ^αと 3 ^{αβ は} 関数の基本的な特性を表現します。
公理スキーマ 4 は、λ 表記法の性質を定義します。
公理5によれば、選択演算子は個体に対する等式関数の逆である。（1つの引数が与えられると、_Q $は$ その個体をその個体を含む集合/述語にマッピングする。Q0において、 $x = yは$ $Qxy$ の略語であり、Qxyは $(Qx)y$ の略語である。）この演算子は、確定記述演算子とも呼ばれる。

Andrews 2002では、公理4は置換過程を細分化した5つのサブパートに分けられています。ここで示されている公理は代替案として議論され、サブパートから証明されています。

論理コアの拡張

アンドリュースはこの論理を、あらゆる型のコレクションに対する選択演算子の定義に拡張し、

$(5a)$ ℩ $_{\alpha (o\alpha )}[{\text{Q}}_{o\alpha \alpha }y_{i}]=y_{i}\,$

は定理（番号5309）です。言い換えれば、すべての型は明確な記述演算子を持ちます。これは保存的な拡張であり、コアが整合していれば拡張されたシステムは整合します。

彼はまた、個体は無限に存在すると述べる追加の公理 6と、それと同等の無限公理を提示しています。

型理論と型理論に基づく証明支援の他の多くの定式化とは異なり、 Q _{0 は}oとi以外の基本型を提供しないため、たとえば有限基数は、単純な型理論の意味での型ではなく、通常のペアノの公理に従う個体の集合として構築されます。

_{Q 0}の推論

Q ₀には推論規則が 1 つあります。

規則 R. $C$ および $A α = B α$ から、 $C$ 内の $A α$ $の 1 つの出現をB$ $α$ の出現に置き換えた結果を推論します。ただし、 $C$ 内の $A$ $α$ の出現の直前に $λ$ (変数の出現) がない場合は除きます。

導出された推論規則R′は、仮説集合Hからの推論を可能にする。

規則 R′. $H ⊦ A α = B α$ 、 $H ⊦ C$ 、 $Dが$ $Cから$ $A α$ の1つの出現を $B α$ の1つの出現に置き換えることによって得られる場合、 $H ⊦ D$ が成り立ちます。ただし、次の条件を満たします。

$C$ における $A α$ の出現は、 $λ$ の直前の変数の出現ではなく、
$A α = B α$ には自由な変数がなく、 $A$ $α$ が置換された時点で $H$ のメンバーが $C$ にバインドされます。

注: C でA $α を$ $B α$ に置き換えるという制約により、仮説と $A$ $α$ $=$ $B$ $α$ $の$ 両方で自由な変数は、置き換えが完了した後も両方で同じ値を持つように制約され続けます。

Q _0の演繹定理は、規則 R′ を使用した仮説からの証明は、仮説なしで規則 R を使用した証明に変換できることを示しています。

いくつかの類似システムとは異なり、Q ₀の推論では、WFF 内の任意の深さの部分式を、等しい式に置き換えます。例えば、以下の公理が与えられたとします。

1. $\existsx Px$ 2. $Px \supset Qx$

$そして、 A \supset B \equiv (A \equiv A \land B)$ という事実から、量指定子を削除せずに続行できます。

3. $Px \equiv (Px \land Qx) を$ A と B に対してインスタンス化します。4. $\existsx (Px \land Qx)$ 規則 R を 3 行目を使用して 1 行目に代入します。

注記

^ 「CADE-22 ATPシステムコンペティション（CASC-22）」。2011年1月20日時点のオリジナルよりアーカイブ。2011年2月7日閲覧。

参考文献

アンドリュース、ピーター・B. (2002). 『数理論理学と型理論入門：証明を通して真理へ』（第2版）. ドルドレヒト、オランダ:クルーワー・アカデミック・パブリッシャーズ. ISBN 1-4020-0763-9。[1] も参照
チャーチ、アロンゾ(1940). 「単純な型理論の定式化」(PDF) . Journal of Symbolic Logic . 5 (2): 56– 58. doi : 10.2307/2266170 . JSTOR 2266170. S2CID 15889861. 2019年1月12 日時点のオリジナル(PDF)からのアーカイブ。

さらに読む

Q ₀のより詳しい説明。スタンフォード哲学百科事典のチャーチの型理論に関する記事の一部。
数理論理学の概要（Q ₀のさまざまな後継を含む）：数学の基礎。系譜と概要 doi:10.4444/100.111。

[1] 「CADE-22 ATPシステムコンペティション（CASC-22）」。2011年1月20日時点のオリジナルよりアーカイブ。2011年2月7日閲覧。

[