過去記事「矢印記号の使用法と読み方 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つのメタ命題が、メタに同値であることを主張します。
- $`X \Vvdash_N A`$
- $`\Vvdash_N X\Rightarrow A`$
$`X`$ を前提〈仮定〉して $`A`$ が証明できることは、何の前提もなしに含意命題 $`X\Rightarrow A`$ が証明できることと同じことだ、という内容です。
型理論の演繹定理
自然演繹の演繹定理と類似の定理を型理論（あるいはシーケント計算）で考えてみます。
ここで、もうひとつ記号を導入します。コンテキスト（$`\vdash`$ の左辺）を幾つか並べるときの区切り記号に '$`\|`$' を使います。これをフェンス記号〈fence symbol〉、あるいは単にフェンス〈fence〉と呼びます。
過去記事「述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則」では、フェンス記号に '$`|`$' を使っていますが、'$`|`$' は OR の意味を持った区切り記号にしたいので、コンテキストの区切り（OR の意味は持たない、むしろ AND）には '$`\|`$' を使うことにします。
さて、型理論の演繹定理ですが、$`T`$ を型理論の導出システムとして、次の2つのメタ命題が、メタに同値であることを主張します。
- $`\Sigma \Vvdash_T \Gamma \vdash A`$
- $`\Vvdash_T \Sigma \mathrel{\|} \Gamma \vdash A`$
型理論の導出システム $`T`$ に、コンテキスト〈指標〉 $`\Sigma`$ を組み込み公理系として入れてしまった導出システムを $`T+\Sigma`$ と書くと、次のメタ命題も同値です。
- $`\Vvdash_{T + \Sigma} \Gamma \vdash A`$
演繹定理は構文的な主張ですが、これを意味論的に解釈することは興味深い課題です。
