File CoMoEx.Laws
In diesem File soll es um übliche und (teilweise) bekannte klassische logische Gesetze gehen. Eine weitere Annotierung bleibt hier aktuell aus, da die Gesetze ja eh schon ausgeschrieben sind.
Section trivial_iff.
Variable p : Prop.
Theorem trivial_iff_true : (p ↔ True) ↔ p.
Proof.
Admitted.
Theorem trivial_iff_false : (p ↔ False) ↔ ¬p.
Proof.
Admitted.
End trivial_iff.
Section comm.
Variables p q : Prop.
Theorem and_comm : (p ∧ q) → (q ∧ p).
Proof.
Admitted.
Theorem or_comm : (p ∨ q) → (q ∨ p).
Proof.
Admitted.
End comm.
Section assoc.
Variables p q r : Prop.
Theorem and_assoc : ((p ∧ q) ∧ r) ↔ (p ∧ (q ∧ r)).
Proof.
Admitted.
Theorem or_assoc : ((p ∨ q) ∨ r) ↔ (p ∨ (q ∨ r)).
Proof.
Admitted.
End assoc.
Section de_morgan.
Variables p q : Prop.
Theorem de_morgan_1 : (p ∧ q) ↔ ¬ (~p ∨ ¬q).
Proof.
Admitted.
Theorem de_morgan_2 : (p ∨ q) ↔ ¬ (~p ∧ ¬q).
Proof.
Admitted.
End de_morgan.
Section implsem.
Variables p q : Prop.
Theorem impl_with_disj : (p → q) ↔ (¬p ∨ q).
Proof.
Admitted.
Theorem impl_with_conj : (p → q) ↔ ~(p ∧ ¬q).
Proof.
Admitted.
End implsem.
Section distr.
Variables p q r : Prop.
Theorem distr_1 : (p ∧ q) ∨ r ↔ (p ∨ r) ∧ (q ∨ r).
Proof.
Admitted.
Theorem distr_2 : (p ∨ q) ∧ r ↔ (p ∧ r) ∨ (q ∧ r).
Proof.
Admitted.
End distr.
Section p_not_p.
Variables p : Prop.
Theorem p_and_not_p : ¬ (p ∧ ¬p).
Proof.
Admitted.
Theorem excluded_middle : (p ∨ ¬p).
Proof.
Admitted.
End p_not_p.
Section idem.
Variables p : Prop.
Theorem idem_and : p ∧ p ↔ p.
Proof.
Admitted.
Theorem idem_or : p ∨ p ↔ p.
Proof.
Admitted.
End idem.
Section absorb.
Variables p q : Prop.
Theorem absorb_and : p ∧ (p ∨ q) ↔ p.
Proof.
Admitted.
Theorem absorb_or : p ∨ (p ∧ q) ↔ p.
Proof.
Admitted.
End absorb.
Section neutr.
Variables p : Prop.
Theorem neutr_and : p ∧ True ↔ p.
Proof.
Admitted.
Theorem neutr_or : p ∨ False ↔ p.
Proof.
Admitted.
End neutr.
Section contrapos.
Variables p q : Prop.
Theorem contrapos : (p → q) ↔ (¬q → ¬p).
Proof.
Admitted.
Corollary mod_tollens : ((p → q) ∧ ¬q) → ¬p.
Proof.
Admitted.
End contrapos.
Section impl_trans.
Variables p q r : Prop.
Hypothesis A1 : p → q.
Hypothesis A2 : q → r.
Theorem impl_trans : p → r.
Proof.
Admitted.
End impl_trans.
Section currying.
Variables p q r : Prop.
Theorem curry : ((p ∧ q) → r) ↔ (p → q → r).
Proof.
Admitted.
End currying.
Section peirce_law.
Variables p q : Prop.
Theorem peirce : ((p → q) → p) → p.
Proof.
Admitted.
End peirce_law.