Q0 (数学的論理)

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

定理証明システムTPSとETPSはQ0に基づいています_。 2009年8月、TPSは高階定理証明システムの最初のコンテストで優勝しました。^[1]

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

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

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

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

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

${\displaystyle (5)}$  ℩${\displaystyle _{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 では、x はAのBにおいて自由でなければなりません。つまり、置換によってAの自由変数の出現が置換の結果に束縛されることはありません。

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

Andrews 2002 では、公理 4 は、置換のプロセスを細分化した 5 つのサブパートに分かれて展開されています。ここで示されている公理は代替案として説明され、サブパートから証明されています。

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

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

は定理です（番号5309）。つまり、すべての型には明確な記述演算子があります。これは保守的な拡張であるため、コアが一貫している場合、拡張されたシステムは一貫しています。

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

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

Q _{0 には}推論規則が 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. ∃x Px
2. Px ⊃ Qx

A ⊃ B ≡ (A ≡ A ∧ B)という事実から、量指定子を削除せずに先に進むことができます。

3. Px ≡ (Px ∧ Qx) を   A と B に対してインスタンス化します
。4. ∃x (Px ∧ Qx)   規則 R を 3 行目を使用して 1 行目に代入します。

• アンドリュース、ピーター B. (2002)。『数理論理学と型理論入門：証明を通して真実へ（第 2 版）』。オランダ、ドルドレヒト：Kluwer Academic Publishers。ISBN 1-4020-0763-9。 [1]も参照
• Church, Alonzo (1940). 「単純な型理論の定式化」(PDF) . Journal of Symbolic Logic . 5 (2): 56–58. doi :10.2307/2266170. JSTOR  2266170. S2CID  15889861. 2019-01-12 にオリジナル(PDF)からアーカイブ。

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