Lean4 学習3

Quantifiers and Equality の演習にて、床屋のパラドックスを示す問題があった。これは排中律を使用すればすぐに解けるのだが、検索してみると構成的証明があるとのことで、やってみると解けた。

  variable (men : Type) (barber : men)
  variable (shaves : men → men → Prop)

  example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := 
    let p := shaves barber barber
    have _ : p ↔ ¬p := h barber 
    have _ : ¬p := fun _ : p => ((‹p ↔ ¬p›).mp ‹p›) ‹p›  
    have _ : p := (‹p ↔ ¬p›).mpr ‹¬p› 
    ‹¬p› ‹p›

新たに覚えた french quotation marks を使った書き方で解いていくと、どこかで見た命題を証明していることに気がついた。前章 Propositions and Proofs の最後の一文に Prove ¬(p ↔ ¬p) without using classical logic. とあるのを見つけた、自分は without using classical logic の部分を見落としていたようだった。

感想

• 排中律は ¬p ∨ p
• 無闇に必要だと決めつけてはいけない
• French quotation marks を使った証明は読みやすい気もするが、入力しにくい問題がある
• 数学記号で書いたコードは検索しにくい問題もある
• 数学用キーボードがあるといい？
• 他の言語と違い、型を明示して変数名を隠す方が読みやすい？
• 証明以外まだ書いていないのでなんとも言えないけど