SOURCE: https://hrmacbeth.github.io/math2001/05_Logic.html

This repository contains a series of logical proofs written in Lean 4. Each proof demonstrates fundamental concepts in propositional logic and predicate logic. The proofs use various Lean tactics to establish equivalences, implications, and other logical relationships.

Given hypotheses $P$ and $Q$, the proof shows that $P \lor Q$ holds.

This proof demonstrates that if $P \to Q$ and $P \to R$, and $P$ holds, then $Q \land R$ both hold.

The proof shows that $\neg (P \land \neg P)$ holds, which is a demonstration of the law of non-contradiction.

Given that $P \leftrightarrow \neg Q$ and $Q$ holds, the proof shows that $\neg P$ must hold.

The proof demonstrates that if $P \lor Q$ holds and $Q \to P$, then $P$ holds.

This proof shows that $(P \land R) \leftrightarrow (Q \land R)$ given that $P \leftrightarrow Q$.

The proof demonstrates that $P \land P \leftrightarrow P$.

This proof establishes that $P \lor Q \leftrightarrow Q \lor P$.

The proof shows that $\neg (P \lor Q) \leftrightarrow (\neg P \land \neg Q)$.

This proof demonstrates that $\neg (\neg P) \leftrightarrow P$.

The proof shows that $\neg (P \to Q) \leftrightarrow (P \land \neg Q)$.

The proof demonstrates that if $\forall x, (P x \to Q x)$ and $\forall x, P x$, then $\forall x, Q x$.

The proof establishes that $(\exists x, P x) \leftrightarrow (\exists x, Q x)$ given that $\forall x, (P x \leftrightarrow Q x)$.

The proof shows that $(\exists x y, P x y) \leftrightarrow (\exists y x, P x y)$.

This proof demonstrates that $(\forall x y, P x y) \leftrightarrow (\forall y x, P x y)$.

The proof shows that $(\exists x, P x) \land Q \leftrightarrow \exists x, (P x \land Q)$.

The proof establishes that $\neg (\forall x, P x) \leftrightarrow \exists x, \neg P x$.