暫定版証明図シリアル化構文 - (保存用) 檜山正幸のキマイラ飼育記メモ編

αを名前を表すメタメタ変数として：

項メタ変数 %α
命題メタ変数 _α
式パスメタ変数 @α

自然言語（英語）としての自然さよりは、人工言語としての整合性を重視する。

使う前置詞：

by
with
to
of
from

byとwithは区別しない。by/withはどちらでもいいことを示す。

論理記号に対応する推論規則

∧、∨、¬、False、∀、∃

∧導入 concat-by/with

concat [_A] by/with _B
_A ∧ _B

concatはconcatenateの省略。_Bを右にAND連接する操作。concatenate _A and _B がたぶん英語的に正しい。

∧除去 select-from

select $.1 from _A∨_B
_A

select $.2 from _A∨_B
_B

より一般には、

// _Bは_Aにconjunction factorとして含まれる
select @x from _A
_B

∨導入 add-by/with

add [_A] by/with _B
 _A ∨ _B

add _B to _A がたぶん英語的に正しい。が、ここではtoを使わない。省略不可能な入力はby/withを使う。

∨除去 cases-of__end-cases

casesブロック／caseサブブロック

cases [of_A ∨ _B]
 case $.1
   _A
   :
   C
 case $.2
   _B
   :
   C
end cases [of_A ∨ _B]
 C

disjunction factorsを網羅する式パスを使ってcasesを書いてもよい。

¬導入 contradiction__end-contracidtion

contradictionブロックは、背理法をブロック内で行う。contradictコマンドとの混同注意。

 contradiction
  _A
  :
  False
 end contradiction
  ¬ A

¬除去 contradict-by/with

contradictionブロックとの混同注意。

 contradict [¬_A] by/with A
  False

⇒導入 use-condition-to

use [condition] _A [to _B]
 _A ⇒ _B

_A は含意命題の条件部だから。

⇒除去 apply-to

法則の適用。

apply _A⇒_B [to _A]
 _B

関数適用 f(a) が apply f to a なので。

False導入 contradict-by/with

¬除去と同じ。

contradict [_A] by/with ¬_A
 False

False除去 produce

 False
produce
 _A

False produces any proposition の意味。

∀導入 introduce-universal

 introduce universal  [on %x] [to _P]
  ∀%x._P

∀除去 instantiate-by/with

 instantiate [∀x%.P] by/with %t
  P[%t/%x]

∃導入 itroduce-existential

 introduce existential [on %x] [to _P] witness %t
  ∃%x._P[%x/%t]

∃除去 choice-of__end_choice

choiceブロック、Mizarのtakeをブロック構文にした。

choice %a [of ∃%x._P]
 P[%a/%x]
 :
 C
end choice [of ∃%x._P]
 C

命題の提示

ラベル付け put

put
 _A ---(α)

仮定の提示 assume

assume
 _A

公理の提示 axiom

公理の宣言ではない。既に宣言された公理の引用再掲。

axiom [(α)]
 _A

前提の提示 premise

マクロ推論規則の定義に使われる。

premise
 _A ---(α)

定義と法則の利用

定義による展開 expand-by/with

// _D は _A :⇔ _B
expand [_A] by/with _D
 _B

定義による縮約 contract-by/with

// _D は _A :⇔ _B
contract [_B] by/with _D
 _A

法則による書き換え rewrite-by/with

rewrite [_A] by/with _R
  _B

証明

証明 proof-of

proof [of _A]
 :
 [thus]
 _A
end proof [of A]
[_A]

証明規則呼び出し

call α[_A1, ..., _An]
 _B

サブ証明 now__end-now

now proof [of A]
  :
 [thus]
  A
end proof
 A

nowはMizarキーワード。別に使わなくてもよい。証明は単純に入れ子にしてよい。

事例

前の記事の例。再掲。

// SerND 差集合の像
put
 f(A)＼f(P) ⊆ f(A＼P) ---(goal)
proof of (goal)
 assume
  y∈(f(A)＼f(P)) ---(ass)
 expand by DefSetDiff
  y∈f(A) ∧ ¬(y∈f(P))
 expand $.1 by DefMapImage; expnad $.2.1 by DefMapImage
  ∃x.(x∈A ∧ f(x) = y) ∧ ¬(∃x.(x∈P ∧ f(x) = y)
 apply LawDeMor to $.2
  ∃x.(x∈A ∧ f(x) = y) ∧ ∀x.(¬(x∈P) ∨ ¬(f(x) = y)) ---(ass')
 select $.1
  ∃x.(x∈A ∧ f(x) = y)
 choice a
    a∈A ∧ f(a) = y ---(ch)
   select $.2 of (ass')
    ∀x.(¬(x∈P) ∨ ¬(f(x) = y))
   instantiate by a
    ¬(a∈P) ∨ ¬(f(a) = y) ---(inst)
   select $.2 of (ch)
    f(a) = y ---(ch2)
   call RuleDistNeg[(inst), (ch2)]
    ¬(a∈P)
   concat with (ch)
    ¬(a∈P) ∧ (a∈A ∧ f(a) = y)
   rewrite by LawConjAsoc, LawConjComm
    (a∈A ∧ ¬(a∈P)) ∧ f(a) = y
   introduce existential witness a
    ∃x.((x∈A ∧ ¬(x∈P)) ∧ f(x) = y)
 end choice
  ∃x.((x∈A ∧ ¬(x∈P)) ∧ f(x) = y)
 contract $.1.1 by DefSetDiff
  ∃x.(x∈A＼P ∧ f(x) = y)
 contract by DefMapImage
  y∈f(A＼P)
 use condition (ass)
  y∈(f(A)＼f(P)) ⇒ y∈f(A＼P)
 contract by Def SetInc
  f(A)＼f(P) ⊆ f(A＼P)
end proof of (goal)