名前でだまされない

axiom, constant, parameter, hypothesis などは同義語であり、どれを選ぶかは好みの問題。

• axiom exclusive_middle {P :Prop} : P∧￢P → False : Prop
• constant exclusive_middle {P :Prop} : P∧￢P → False : Prop
• parameter exclusive_middle {P :Prop} : P∧￢P → False : Prop
• hypothesis exclusive_middle {P :Prop} : P∧￢P → False : Prop

theorem, lemma は同義語。rule とか principle も同義。

theorem Or.elim {c : Prop} (h : Or a b) (leftPoof : a → c) (rightProof : b → c) : c :=
  match h with
  | Or.inl h => leftProof h
  | Or.inr h => rightProof h

これは次のようにも書ける。

-- 連言消去ルール
rule Or.elim {c : Prop} (h : Or a b) (leftPoof : a → c) (rightProof : b → c) : c :=
  match h with
  | Or.inl h => leftProof h
  | Or.inr h => rightProof h

-- 連言消去原理
principle Or.elim {c : Prop} (h : Or a b) (leftPoof : a → c) (rightProof : b → c) : c :=
  match h with
  | Or.inl h => leftProof h
  | Or.inr h => rightProof h

ほとんど区別しなくていいモノの名前がイッパイ。

• 公理、定数、パラメータ、仮説、
• 定理、証明、推論、規則〈ルール〉、原理、演繹、{判断の}?証拠、保証
• 判断、主張、事実
• 質問、問い合わせ、問題、ゴール、要求
• コンテキスト、指標、前提、引数
• 結論、結果、ターゲット、戻り値型
• シーケント、プロファイル、ゴール