aconite-ac / theorem_proving_in_lean4

Theorem Proving in Lean 4 日本語訳
https://aconite-ac.github.io/theorem_proving_in_lean4_ja/
Apache License 2.0
10 stars 2 forks source link

3章 命題と証明 - Negation and Falsity の訳文について #4

Closed Seasawher closed 7 months ago

Seasawher commented 10 months ago
原文

Negation, ¬p, is actually defined to be p → False, so we obtain ¬p by deriving a contradiction from p.

現在の訳文

否定 ¬p は p → false と定義される。したがって、¬p の証明は p から矛盾を導くことで得られる。

改善案

否定 ¬p は p → False と定義される。したがって、¬p の証明は p から矛盾を導くことで得られる。

理由

false と False の違い.