コマンドとブロック

• 最初の案： 暫定版 証明図シリアル化構文 - 檜山正幸のキマイラ飼育記 メモ編
• その後の変更： 証明図シリアル化構文 キーワードの現状 - 檜山正幸のキマイラ飼育記 メモ編

BLKと書いてあるのはブロック、そうでなければコマンド。

論理記号	導入	削除
∧	make conjunction of/with	select - from
∨	make disjunction of/with	case of BLK
¬	contradiction of BLK	found inconsistency of/with
⊃	use assumption - to	appy - to
∀	for BLK	instanciate - with
∃	witness of BLK	choice - of BLK

• conjunction, disjunction の動詞はないようだ。
• contradiction は proof by contradiction から。
• forはfixに変えるかも知れない。
• absurdは the absurd で名詞に使える。

ブロックには引数命題と最終命題と結論命題がある。

ブロック	引数命題	最終命題	結論命題
proof of	P	P	P
contradiction	P	absurd	¬P
for x:X	なし	P(x)	∀x:X.P(x)
case of	P∨Q	R	R
choice a:X	∃x:X.P(x)	Q	Q
witness of	x:X, P(x)	P(t)	∃x:X.P(x)

直前のブロックから結論命題を取り出すコマンドがtherefor。

コマンド構文

make conjunction コマンド

• [make] conjunction [of P] with Q ...
• 出力： 結論命題 P∧Q

select コマンド

• select e [from P] eはパス式
• 出力： パスで選択された命題

make disjunction コマンド

• [make] disjunction [of P] with Q ...
• 出力： 結論命題 P∨Q

found inconsistency コマンド

• [found] inconsistency [of P] with Q
• 出力： absurd

assume コマンド

• assume P
• 出力： なし

use assumption コマンド

• [use] assumption P [to Q]
• 出力： 結論命題 P⊃Q

instanciate コマンド

• instanciate [∀x:X.P(x)] with t
• 出力： 結論命題 P(t)

apply コマンド

• apply P⊃Q [to P]
• 出力：結論命題 Q

therefor コマンド

• therefor
• 出力： ブロックの結論命題

ブロック構文

proof ブロック

• proof [of P] end
• 自動仮定： なし
• 要求最終命題： P
• 結論： P 最終命題

contradiction ブロック

• contradiction [of P] / end
• 自動仮定： ¬P
• 要求最終命題： absurd
• 結論：P 最終命題

case ブロック

• case [of P∨Q ...] / whenブロック ... / end
• 自動仮定： なし
• 要求最終命題： すべてのwhenブロックで同じ結論R
• 結論： R 最終命題

for ブロック

• for x:X / end
• 自動仮定： なし
• 要求最終命題： なし だがPとする
• 結論： ∀x:X.P

witness ブロック

• withness [of P(x)] / end
• 自動仮定： なし
• 要求最終命題： P(t)
• 結論： ∃x:X.P(x)

choice ブロック

• choice a:X [from ∃x:X.P(x)] / end
• 自動仮定： P(a)
• 要求最終命題： aを含まないQ
• 結論： Q 最終命題