含意の定義について

[Seasawher]

なぜ前件が偽なら真になるのか？
2変数真理関数が、含意っぽい性質を満たしていれば必ずそうなることを証明する問題を紹介したい

[Seasawher]

これは「論理学をつくる」という本に載っている例

[Seasawher]

ここまで公理を足したけどたぶんまだ足りない

opaque Imp (P Q : Prop) : Prop

/-- 推移的 -/
axiom imp_transitive {P Q R : Prop} (hpq : Imp P Q) (hqr : Imp Q R) : Imp P R

/-- 反射的ではない -/
axiom imp_not_reflexive : ¬ (∀ (P Q : Prop), Imp P Q ↔ Imp Q P)

/-- モーダスポネンス -/
axiom modus_ponens {P Q : Prop} (hP : P) (h : Imp P Q) : Q

/-- 前件が真なときは Imp P Q は Q に一致する -/
axiom imp_of_true (Q : Prop) : Imp True Q = Q