コマンド動詞、ブロック、根拠名詞、その他

コマンドは、先頭が動詞原型または動詞過去分詞形、それに続いてキーワード目的語名詞が続いてもいい。apply, make conjunction, found inconsistency など。

「命題 by 根拠名詞 引数並び」でも証明が書けるとする。以下、根拠名詞とコマンド動詞の対応表。

規則	名詞	動詞
∧I	conjunction	make conjunction
∧E	selection	select
∨I	disjunction	make disjunction
∨E	case of ブロック	case of ブロック
⊃I	presupposition	presuppose
⊃E	application	apply
¬I	contradiction ブロック	contradiction ブロック
¬E	inconsistency	found inconsistency
∀I	for ブロック	for ブロック
∀E	instanciation	instanciate
∃I	example	found example
∃E	choice ブロック	choice ブロック

以前、∃Iに witness ofブロックを使うとしたが、found example t of a for P; ∃x.P でもいいような気がする。

例

// 最大元の存在
∀x.(x≦t)
found example t of a for ∀x.(x≦a)
∃x∀x.(x≦x)

// または
∀x.(x≦t)
∃y.∀x.(x≦y) by example t

found example（または、found witness）コマンドを使うことにすると、ブロック構造は4つしかない：

1. ∨E規則のcase ofブロック … 場合分け証明
2. ¬I規則のcontradictionブロック … 背理法
3. ∀Iのforブロック … 自由変数から全称閉包
4. ∃Eのchoiceブロック … 条件付き変数の消去

推論規則以外に、次のコマンドが必要。

1. 「assume 命題」コマンド、仮定を追加する。
2. 「use 命題」コマンド、前提（仮定とは別）から命題を引用する。
3. 「use axiom」とか「use theorem」とかがある。
4. call 証明 コマンド、他の証明に引数を渡して呼び出す。

普通の証明以外に証明テンプレートがあり、命題パラメータを受け取って、実際の証明が生成される。

用語を少し整理しておくと：

• 定理：フルカリー化された証明＝1→? の形の射＝インハビタントを伴う対象
• 公理：生成射であるインハビタントを伴う対象
• 証明： 任意の射
• 証明命題： 射のフルカリー化をインハビタントとする対象
• 証明判断： 証明と命題の圏のワイヤーフレーム圏の射

証明と命題の圏では、公理や定理は命題ではない。そうではなくて、特殊な形の射（＝証明）を公理・定理と呼んでいる。インハビタント t:1→A があれば、Aは定理の命題と言っていいが、定理はインハビタントtそのものの事である。

• 定理＝インハビタント＝1を域とする射
• 定理の命題＝定理命題＝インハビタント射の余域
• したがって、定理も公理も特殊な証明である。
• 定理・公理をアンカリー化して使ってよい。
• 推論規則は証明とは全然別物で、自然変換を含む圏論的オペレーターで、その成分（component）が証明となるものである。成分は、命題パラメータの具体化で与えれるから、推論規則を呼び出すには、具体化用の実パラメータ命題が必要。
• 証明の呼び出し call 証明 giving 命題1, 命題2 end のよう。
• 証明テンプレートの呼び出しは、call テンプレート with 命題1, 命題2 giving 命題3, 命題4 end のよう。

template proof IDENT %A
 ensures %A⊃%A
begin
 assume %A ---(a)
 %A by assumption
 presuppose (a)
 %A⊃%A
end

これを呼ぶには、

• call IDENT with P end therefor P⊃P （証明の仮定がないのでgivingは不要）

template proof EMBED %B
 given %A
 ensures %B⊃%A
begin
 assume %B ---(b)
 %A ---(a) by assumption
 presuppose (b)
 %B⊃%A
end

これを呼ぶには、

• call EMBED with Q giving P end therefor P⊃Q

thereforよりshowsやobtainsがいいかもしれない。

ところで、inhabitedの訳語は「被住」にするか？ inhabitanceは「被住性」。