型理論の演繹定理

過去記事「矢印記号の使用法と読み方 2024」において、様々な矢印記号の意味・運用について述べました。構文論で使う矢印記号に関して、別な読み方・名前を追加して一覧表を再掲します。

矢印記号	読み方	別な読み方・名前
$`\Rightarrow`$	含意〈implies〉	関数型〈function type〉
$`\vdash`$	伴意〈entails〉	判断ストローク〈judgement stroke〉
$`\rightrightarrows`$	推論〈infers〉	(特になし)
$`\Vdash`$	正当〈correct〉	整形式性〈well-formedness〉
$`\Vvdash`$	導出可能〈derivable〉	証明可能〈provable〉

論理の通常の記法では、'$`\vdash`$' が導出可能〈証明可能〉を意味するメタ記号です。が、型理論で常用される '$`\vdash`$' は伴意／判断ストロークなので、ここでは、導出可能〈証明可能〉の記号に '$`\Vvdash`$' を使います。

「矢印記号の使用法と読み方 2024」では、導出システム〈演繹システム | 証明システム〉$`S`$ により判断〈シーケント〉が導出可能なことを $`S \Vvdash \Gamma \vdash A`$ のように書いてましたが、ここでは次の記法にします。

$`\quad \Vvdash_S \Gamma \vdash A`$

'$`\Vvdash`$' の左側を別な用途に使いたいので。

自然演繹の演繹定理

自然演繹の導出システムを $`N`$ とします。自然演繹の導出システムは、判断〈シーケント〉を導出するのではなくて、論理式を導出します。$`A`$ を論理式として、$`N`$ により $`A`$ が導出可能なことは次のように書けます。

$`\quad \Vvdash_N A`$

導出可能の記号 '$`\Vvdash`$' の左側には、前提〈仮定〉を置くことにします。論理式 $`X`$ を前提して、$`N`$ により $`A`$ が導出可能なことを次のように書きます。

$`\quad X \Vvdash_N A`$

自然演繹に関する演繹定理は、次の2つのメタ命題が、メタに同値であることを主張します。

1. $`X \Vvdash_N A`$
2. $`\Vvdash_N X\Rightarrow A`$

$`X`$ を前提〈仮定〉して $`A`$ が証明できることは、何の前提もなしに含意命題 $`X\Rightarrow A`$ が証明できることと同じことだ、という内容です。

型理論の演繹定理

自然演繹の演繹定理と類似の定理を型理論（あるいはシーケント計算）で考えてみます。

ここで、もうひとつ記号を導入します。コンテキスト（$`\vdash`$ の左辺）を幾つか並べるときの区切り記号に '$`\|`$' を使います。これをフェンス記号〈fence symbol〉、あるいは単にフェンス〈fence〉と呼びます。

過去記事「述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則」では、フェンス記号に '$`|`$' を使っていますが、'$`|`$' は OR の意味を持った区切り記号にしたいので、コンテキストの区切り（OR の意味は持たない、むしろ AND）には '$`\|`$' を使うことにします。

さて、型理論の演繹定理ですが、$`T`$ を型理論の導出システムとして、次の2つのメタ命題が、メタに同値であることを主張します。

1. $`\Sigma \Vvdash_T \Gamma \vdash A`$
2. $`\Vvdash_T \Sigma \mathrel{\|} \Gamma \vdash A`$

型理論の導出システム $`T`$ に、コンテキスト〈指標〉 $`\Sigma`$ を組み込み公理系として入れてしまった導出システムを $`T+\Sigma`$ と書くと、次のメタ命題も同値です。

• $`\Vvdash_{T + \Sigma} \Gamma \vdash A`$

演繹定理は構文的な主張ですが、これを意味論的に解釈することは興味深い課題です。