2. Propositional and Predicate Logic

Propositional and Predicate Logic

Review of propositional and predicate logic

Propositional logic deals with propositions, which are statements that are either true or false. It studies logical connectives such as AND, OR, NOT, and implications, and how they can be used to form compound propositions. For example, the proposition "P AND Q" is true only when both P and Q are true.

Predicate logic extends propositional logic by introducing predicates, which are statements that depend on variables. It deals with quantifiers such as ∀ (for all) and ∃ (there exists), allowing us to make statements about entire sets of objects. For example, the statement "For all x, if x is a natural number, then x is greater than 0" can be expressed in predicate logic as "∀x, Nat(x) → x > 0".

Introduction to proof techniques in Coq

Coq provides a powerful environment for constructing formal proofs of mathematical statements and logical propositions. It supports various proof techniques, including direct proofs, proof by contradiction, and structural induction. Coq's proof language allows users to express logical statements and manipulate them using tactics, which are commands that guide the proof process. By combining tactics, users can construct complex proofs step by step, ensuring their correctness at each stage.

Lab Activities

Basic Logical Propositions in Coq

In this lab activity, we will use Coq to write and prove basic logical propositions. We will demonstrate the use of Coq's proof tactics to construct formal proofs of simple statements.

Lemma and_comm : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros P Q H.
  destruct H as [HP HQ].
  split.
  - apply HQ.
  - apply HP.
Qed.

The above Coq code demonstrates a proof of the commutativity of conjunction (AND) in propositional logic. The lemma "and_comm" states that if propositions P and Q are both true, then Q and P are also both true. The proof uses the "destruct" tactic to break down the conjunction into its constituent parts, and then applies the properties of conjunction to rearrange them.

Lemma or_comm : forall P Q : Prop,
  P \/ Q -> Q \/ P.
Proof.
  intros P Q H.
  destruct H as [HP | HQ].
  - right. apply HP.
  - left. apply HQ.
Qed.

This Coq code proves the commutativity of disjunction (OR) in propositional logic. The lemma "or_comm" states that if either proposition P or proposition Q is true, then the other proposition is also true. The proof again uses the "destruct" tactic to consider both cases of disjunction, and then applies the properties of disjunction to rearrange them.

Lemma not_or : forall P Q : Prop,
  ~(P \/ Q) -> (~P /\ ~Q).
Proof.
  intros P Q H.
  split.
  - intro HP. apply H. left. apply HP.
  - intro HQ. apply H. right. apply HQ.
Qed.

This Coq code proves De Morgan's law for negation of disjunction. The lemma "not_or" states that if neither proposition P nor proposition Q is true (i.e., their disjunction is false), then both propositions P and Q are false. The proof uses the "split" tactic to prove the conjunction of two negations by showing that each proposition leads to a contradiction.