We now turn our attention to a formal axiom system that is based on one first formulated by Gerhard Gentzen in 1934 as a formal system that closely imitates the way mathematicians actually reason when writing traditional expository proofs.
The language of propositional logic has two constants $\mathtt{true}$ and $\mathtt{false}$. We sometimes will abbreviate these as $\mathtt{T}$ and $\mathtt{F}$ respectively. The statements in the language are all expressions of this type, namely, they all represent a truth value which is either $\mathtt{true}$ or $\mathtt{false}$.
Any variable can be used to represent a statement in this system. Such variables, and the constants $\mathtt{true}$ and $\mathtt{false}$ are the atomic statements in the language of propositional logic. In addition, we can form compound statements by first defining five constants, “$\neg$”, “$\xand$”, “$\xor$”, “$\implies$”, and “$\iff$”, and using them to define compound statements as follows.
Definition. Let $\varphi ,\psi$ be statements. Then the five expressions $$\begin{gathered} \neg \varphi \\ \varphi \xand \psi \\ \varphi \xor \psi \\ \varphi \implies \psi \\ \varphi \iff \psi \end{gathered}$$ are also statements whose truth values are completely determined by the truth values of $\varphi$ and $\psi$ as shown in the following table:
| $\varphi$ | $\psi$ | $\neg \varphi$ | $\varphi\xand \psi$ | $\varphi\xor \psi$ | $\varphi\implies \psi$ | $P\iff \psi$ |
|---|---|---|---|---|---|---|
| T | T | F | T | T | T | T |
| T | F | F | F | T | F | F |
| F | T | T | F | T | T | F |
| F | F | T | F | F | T | T |
We can also write not for $\neg$,
if and only if or iff for $\iff$, and
implies for $\implies$. A statement of the form
$\varphi\implies\psi$ is called a conditional statement or
an implication, and can be written in English in several
different ways: '$\varphi$ implies $\psi$, 'if $\varphi$ then
$\psi$, '$\psi$ follows from $\varphi$, or '$\psi$, if $\varphi$.
Thus, the statements of Propositional Logic consist of
Note: Recall the precedence of these operators in the following order (from highest to lowest).
| Precedence of Notation |
|---|
| parentheses, brackets, $(), {}, [ ]$ etc. |
| arithmetic operations$^*$ $\wedge,\cdot,+,\ldots$ etc. |
| set operations $\times,-,\cap,\cup,\ldots$ etc. |
| arithmetic and set relations $=,\subseteq,\leq,\neq,\ldots$ etc. |
| $\neg$ |
| $\xand$, $\xor$ |
| $\ximplies$ |
| $\xiff$ |
| $\forall,\exists,\exists!$ |
Natural deduction generally defines a pair of rules for each definition. A plus or introduction rule is used to prove statements that contain the thing being defined from statements that do not, while minus or elimination rules do the opposite. In the following rules, the variables $W$ and $V$ can be any statement.
Rules of Propositional Logic
| Name | Rule |
|---|---|
| and$+$ | $W,V \vdash (W \xand V)$ |
| and$-$ | $(W\xand V) \vdash W, V$ |
| or$+$ | $W \vdash (W\xor V), (V\xor W)$ |
| or$-$ (proof by cases) | $(W\xor V), (W\implies U), (V\implies U) \vdash U$ |
| $\implies\!+$ | $(W\vdash V) \vdash (W\implies V)$ |
| $\implies\!-$ (modus ponens) | $(W\implies V), W \vdash V$ |
| $\iff\!+$ | $(W \vdash V),(V\vdash W) \vdash (W\iff V)$ |
| $\iff\!-$ | $(W\iff V), W \vdash V$ $(W\iff V), V \vdash W$ |
| not$+$ (proof by contradiction) | $(W \vdash ,\xcont) \vdash \xnot W$ |
| not$-$ (proof by contradiction) | $(\xnot W \vdash ,\xcont) \vdash W$ |
| $\xcont+ $ | $W, (\xnot W) \vdash ,\xcont$ |
We can also list these rules in if-then rule notation that mirrors how they are used in proofs.
Definitions of Propositional Logic
Declare $\neg$, and, or, $\implies$, $\iff$ and $\xcont$ to be constants.
and+
Given
$W$
$V$
Conclude $W\xand V$
and-
Given
$W\xand V$
Conclude $W$
Conclude $V$
implies+
Given
$W$
Assume $W$
$V$
Conclude $W\implies V$
implies-
Given
$W$
$W\implies V$
Conclude $V$
iff+
Given
Assume $W$
$V$
Assume $V$
$W$
Conclude $W\iff V$
iff-
Given
$W$
$W\iff V$
Conclude $V$
iff-
Given
$V$
$W\iff V$
Conclude $W$
or+
Given
$W$
Conclude $W\xor V$
Conclude $V\xor W$
or- (proof by cases)
Given
$W\xor V$
Assume $W$
$U$
Assume $V$
$U$
Conclude $U$ by cases
not- (proof by contradiction)
Given
Assume $\neg W$
$\xcont$
Conclude $W$
not+ (proof by contradiction)
Given
Assume $W$
$\xcont$
Conclude $\neg W$
$\xcont+$
Given
$W$
$\neg W$
Conclude $\xcont$
Remarks:
Definition . A compound statement of propositional logic is called a tautology if it is true regardless of the truth values the atomic statements that comprise it. Its column in its truth table contains only T’s.
It can be shown that a statement can be proved with Propositional Logic if and only if the statement is a tautology.
One way to write down the proof of a theorem is called a formal proof.
This style of proof consists must satisfy the following.
A semi-formal proof is written in the same style as a formal proof, but citing reasons and their premises to justify each statement is optional.
Prove the following tautologies using formal proofs. In the following, $P,Q,R,S$ are statements. Sometimes we add additional parentheses for legibility.
implies plus warmup $P \implies P$
iff plus warmup $P \iff P$
and plus warmup $P \implies (P \xand P)$
or plus warmup $P \implies P \xor Q$
and minus warmup $(P \xand P) \implies P$
iff minus warmup $(P \iff Q) \implies (Q \implies P)$
implies minus warmup $((P \implies Q) \xand P)\implies Q$
or minus warmup $P \xor Q \implies Q \xor P$
contradiction plus warmup $(Q \xand \neg Q) \implies \xcont$
not plus warmup $(Q \xand \neg Q) \implies \neg P$
not minus warmup $(Q \xand \neg Q) \implies P$
a contradiction implies anything $\xcont \implies P$
double negation $\neg\neg P \iff P$
modus tollens $((P \implies Q) \xand \neg Q) \implies \neg P$
transitivity of $\implies$ $(P \implies Q) \xand (Q \implies R) \implies (P \implies R)$
contrapositive $(P \implies Q) \iff (\neg Q \implies \neg P)$
true! $\neg \xcont$
excluded middle $P \xor \neg P$
Pierce’s Law $((P \implies Q) \implies P) \implies P$
alternate $\xor!-$ $\left((P \xor Q) \xand \neg P\right) \implies Q$
exclusive or $\neg (P \xiff Q) \iff (\neg P \xand Q) \xor (P \xand \neg Q) $
alternate $\implies$ $(P \implies Q) \xiff, (\neg P \xor Q)$
alternate $\xor!+$ $(\neg P \implies Q) \implies (P \xor Q)$
not implies $\neg\left(P\ximplies Q\right)\xiff \left(P\xand\neg Q\right)$
shunting $((P \xand Q) \ximplies R) \iff (P\implies (Q \implies R))$
De Morgan’s Law $\neg(P\xand Q) \ximplies \neg P \xor \neg Q$
De Morgan’s Law $\neg(P\xor Q) \xiff \neg P \xand \neg Q$
alternate definition of $\xor$ $P\xor Q ,\xiff, (P\implies Q)\implies Q$
the most beautiful tautology? $P \implies (P \iff P \xor (\neg P \xand P))$
$\left(g \text{ is upper semi-computable }\right) \implies \left(g \text{ is a finite simplicial complex}\right) \xor \left(g \text{ is }\text{upper semi-computable }\right)$
$\left(\left(0<x \implies 0<x^3\right) \xand \left(x<0 \implies x^3<0\right)\right) \xand \left(0<x \xor x<0\right) \ximplies \left(0<x^3 \xor x^3<0\right)$
The claim “If you like pizza and pizza is available then you will eat pizza” is true if and only if the claim “If you like pizza, then if pizza is available then you will eat pizza” is true.
It is not the case that $(M$ is representable over $\mathbb{F}_2 \xor M$ has an empty cokernal$)$ if and only if $(M$ is not representable over $\mathbb{F}_2) \xand (M$ does not have an empty cokernal$)$
$P \xand Q \iff Q \xand P$
$P \xor Q \iff Q \xor P$
$(P \iff Q) \iff (Q \iff P)$
Give examples of statements, $P$ and $Q$ such that $(P \implies Q) \implies (Q \implies P)$ is false.
$\left(\left(P \xand Q\right) \xand R\right) \iff \left(P \xand \left(Q \xand R\right)\right)$
$\left(\left(P \xor Q\right) \xor R\right) \iff \left(P \xor \left(Q \xor R\right)\right)$
$\left(\left(P \iff Q\right) \iff R\right) \iff \left(P \iff \left(Q \iff R\right)\right)$
$P \xand \left(Q \xor R\right) \iff \left(P \xand Q\right) \xor \left(P \xand R\right)$
$P \xor \left(Q \xand R\right) \iff \left(P \xor Q\right) \xand \left(P \xor R\right)$
