Leanのaxiom

公理の導入

code:lean(ts)

axiom modus_ponens : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q

項のシグネチャだけを宣言する

Leanのtheoremと異なり、その項は、値を持たない

値(証明)は書かずに、無条件に成り立つ型(命題)の定義をする

「値を持たない」ことで、無条件にその命題は真であると見なす

それが「公理」ということだからねmrsekut.icon

従って、注意しなければ間違った公理も導入できてしまう ref

code:laen

axiom unsound : False

-- False(偽)からは任意の命題を示すことができる

theorem ex : 1 = 0 := -- 本来は偽の命題

False.elim unsound

この:の位置の違いはなにか意味があるのか

code:lean

axiom and_comm (p q : Prop) : Proof ((And p q) -> (And q p))

axiom and_comm : (p q : Prop) -> Proof ((And p q) -> (And q p))