1. Introduction to Informal Proofs

Formal vs. Informal Proofs

We aim to present a formal deductive system which:

• shows how a conclusion follows from a set of premises via a sequence of well-defined proof steps.
• fully agrees with the semantical concept of logical consequence
• is purely syntactical

Informal proofs

The term “informal” here is used in the sense that we may omit some steps and / or use some “accepted” results or statements in the proof: axioms, theorems, etc

Our interim objective is to relate reasoning patterns in the proofs with known tautologies. We will then formalise the notion of proof, to completely forbid any assumptions outside the set of premises or any steps which are not fully defined at the outset.

Common Proof Patterns

Direct proof

A direct proof involves successive application of valid inference steps to demonstrate that a conclusion follows from a set of assumptions.

Link to original

title: Example 1: Prove $n^2$ is odd if $n$ is odd.
**Assume**: $n$ is even iff $n = 2k$ for some integer $k$;
and $n$ is odd iff $n = 2k + 1$ for some integer $k$
 
**Example**: If $n$ is an odd integer, then $n^2$ is odd.
 
**Proof**: Assume that $n$ is any odd integer, and then show that $n^2$ is odd.
If $n$ is odd, then $n = 2k + 1$ for some integer $k$.
Therefore $n^2 = (2k + 1)^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$.
If $k$ is an integer, then $2k^2 + 2k$ is also an integer and hence $n^2$ is odd.

Proof by contradiction

A proof by contradiction is where we show $A \land \neg B$ is a contradiction in order to prove that $A \rightarrow B$.

Link to original

title: Example 2: Prove $A \rightarrow B$ by contradiction.
To prove $A \rightarrow B$, construct a proof of $A \land \neg B \rightarrow 0$.
$$
	\begin{aligned}
		A \land \neg B &\equiv \neg(A \land \neg B) \\
		&\equiv (\neg A \lor B) \\
		&\equiv A \rightarrow B
	\end{aligned}
$$
 
**Example**: If $3n+2$ is odd, then $n$ is odd.
 
**Proof**: Suppose $3n+2$ is odd but $n$ is not odd (i.e. even).
Since $n$ is even, we know that $n = 2k$ for some integer $k$.
Thus, we can expand $3n + 2$ as $3(2k) + 2 = 2(3k + 1)$.
Since $3k + 1$ is an integer, $3n + 2$ can be expressed as $2(3k + 1)$, then $3n + 2$ must be even, and this contradicts out original assumption.
 
Therefore, by contradiction, if $3n+2$ is odd, then $n$ is odd.

Proof by contraposition

A proof by contraposition is where we show $\neg B \rightarrow \neg A$ in order to show that $A \rightarrow B$.

Link to original

title: Example 3: Prove $A \rightarrow B$ by contraposition.
We can show that $\neg B \rightarrow \neg A$.
$$
	\neg B \rightarrow \neg A \equiv A \rightarrow B
$$
 
**Example**: If $3n + 2$ is odd, then $n$ is odd.
 
**Proof**: Suppose that $n$ is not odd (i.e. even), we show that $3n + 2$ is also not odd (i.e. it is even).
 
If $n$ is even, then $n = 2k$, for some integer $k$.
Then $3n + 2 = 3(2k) + 2 = 6k + 2 = 2(3k + 1)$ which is an even number.

Proof by cases

A proof by cases or proof by exhaustion is a method where we split up the argument into different sub-proofs.

Link to original

title: Example 4: Proof by cases.
To prove $(A_1 \lor A_2 \lor ... \lor A_n) \rightarrow B$, you can show that:
$$
	(A_1 \rightarrow B) \land (A_2 \rightarrow B) \land ... \land (A_n \rightarrow B)
$$
 
**Example**: If $n$ is an integer, then $n^2 \ge n$.
 
**Proof**: Let us divide the set of integers into three classes:
- $0$
- positive numbers
- negative numbers
 
And show that in each case that $n^2 \ge n$.
- If $n = 0$, then $n^2 = 0^2 = 0 \ge 0$.
- If $n \ge 1$, then $(n\cdot n) \ge (1\cdot n)$ and therefore $n^2 \ge n$.
- If $n \le 1$, then again we know that $n^2 > 0$, hence $n^2 \ge n$.
 
In all cases, we show that for all of $n$, $n^2 \ge n$.

Fallacies

We want every step in our proof to be correct, we mean that if we apply a step of the form “from $P$ and $P\to Q$, we can conclude $Q$”, or otherwise:

$$\frac{P,P\to Q}{Q}$$

then the formula $(P\wedge (P\to Q))\to Q$ is a tautology.

Fallacy

A fallacy resembles a correct inference, but it is not valid, leading to incorrect reasoning.

Link to original

Fallacy of affirming the conclusion

Suppose the following argument: “If you do every problem in this book ($P$) then you will learn discrete mathematics ($M$). You learned discrete mathematics ($M$). Therefore, you did every problem in this book ($P$).”

$$P\to M,M\models P\text{ is not valid!}$$

Affirming the consequent of the implication $P\to M$ does not guarantee the truth of its antecedent $P$.

Notice when $v(P)=0$ and $v(M)=1$, all the assumptions of the argument are true but the conclusion is false.

This incorrect reasoning pattern is based on the formula

$$((P\to M)\wedge M)\to P$$

which is not a tautology, only a contingency.

Fallacy of denying the hypothesis

Using the same language, consider the argument: “If you do every problem in this book ($P$) then you will learn discrete mathematics ($M$). You did not do every problem in this book ($\neg P$). Therefore, you did not learn discrete mathematics ($\neg M$).”

$$P\to M,\neg P\models \neg M\text{ is not valid!}$$

Denying the antecedent of the implication $P\to M$ does not guarantee the falsity of its consequent $M$.

Notice that $v(P)=0$ and $v(M)=1$ makes all assumptions true but conclusion false.

This incorrect reasoning pattern is based on the formula

$$((P\to M)\wedge \neg P)\to \neg M$$

which is not a tautology, only a contingency.

Link to original

2. Forward Reasoning Systems

Forward Reasoning Systems

Consider the following argument

$$\begin{array}{c}P\\ R\vee S\\ T\\ P\to Q\\ Q\end{array}$$

To check this using truth-tables, we would need to check $2^5$ rows. By just looking at the argument, we can see that we only need to check the 2 premises ($P$ and $P\to Q$).

Formal Proof

Proof

A proof (or deduction) of a formula $B$ from a set of premises $A_1,...,A_n$ is a finite sequence of formulas ending in $B$ such that each formula in the sequence is either a [[Premise|premise]], an [[Axiom|axiom]], or can be obtained from previous formulas in the sequence using an inference rule.

Link to original

Consequence relation

We can define a consequence relation between a set of formulas and a formula using $\vdash$, we can denote $B$ can be derived from $A_1, ..., A_n$ by $A_1, ..., A_n \vdash B$.

This is a syntactical process, hence we use $⊢$ instead of the semantic $\models$ counterpart.

Link to original

Common presentation of an inference rule

Inference rule

An inference rule is a representation of a valid step in a formal proof, indicating the conditions that must be satisfied before a conclusion can be obtained in the proof.

A rule will be presented in the form: $R:\frac{A_1,A_2,...,A_n}{B}$

$A_1,A_2,...,A_n$ are the premises or conditions of the rule, and $B$ is the conclusion.

Informally, $R:$ “if $A_1,A_2,...,A_n$ are true, then $B$ is also true.”

Alternatively, we use the syntax:

$$\begin{array}{c}{A}_1\\ A_2\\ ⋮\\ A_n\\ B\end{array}$$Link to original

Modus ponens

Modus ponens comes from the Latin “method of affirming (the antecedent)”. Sometimes referred to as “elimination of the implication” ($\to E$): ?

$$\frac{A,A\to B}{B}(\to E)\text{ or "modus ponens"}$$

For example, if A was born in Britain, they are British. A was born in Britain. Therefore, A is British.

Link to original

Notation for proofs

Proof sequence

A proof sequence $W_1,W_2,...,W_n$ will be represented in the following way: ?

$$\begin{array}{rlrlrl}& 1.& & W_1& & \text{justification for }{W}_1\\ & 2.& & W_2& & \text{justification for }{W}_2\\ & ⋮& & ⋮& & ⋮\\ & n.& & W_n& & \text{justification for }{W}_n\end{array}$$

If the derivation of formula in a line depends on other formulas, then the line numbers of those formulas must be indicated as part of its justification.

If a proof contains premises, then those are justified by the words ‘given’, ‘assumption’ or ‘data’.

Link to original

title: Example 1
Our initial argument was $P, R \lor S, T, P \rightarrow Q \vdash Q$.
 
Using the sample rules we provided, a possible proof of its validity could be:
 
$$
	\begin{aligned}
		&1. &&P &&\text{data} \\
		&2. &&P \rightarrow Q &&\text{data} \\
		&3. &&Q &&\text{from 1. and 2. and } (\rightarrow E) \\
	\end{aligned}
$$
 
We can use the premises for "free" (they are assumptions).
Thus justifications for 1-2 are given or "data".
Line 3 demonstrates that $Q$ is a valid conclusion because lines 1-2 fulfil the conditions of the modus ponen rule.

Deduction Theorem

Deduction Theorem

If there is a proof of $B$ that uses a formula $A$ as a premise, then there is a proof of the implication $A\to B$ that does not use $A$ as a premise. Formally:

$$\mathcal{S}\cup \{A\}⊢B⟺\mathcal{S}⊢A\to B$$

If we consider the special case when $\mathcal{S}$ is empty, this becomes $\{A⊢B\}⟺⊢A\to B$. Essentially, we are saying proving $B$ follows from $A$ is equivalent to proving that $A\to B$ is a tautology.

Link to original

title: Example 2
Earlier, we wanted to show "If $n$ is an odd integer ($N_1$), then $n_2$ is odd ($N_2$)".
This means we need to show that $\vdash N_1 \rightarrow N_2$.
 
The deduction theorem tells us that we can show this if we assume $N_1$,
then show that $N_2$ follows: $N_1 \vdash N_2$.
 
We can describe our previous direct proof as follows:
 
$$
	\begin{aligned}
		&1. &&n \text{ is odd} &&\text{assume} \\
		&2. &&n = 2k + 1 \text{ for some } k &&\text{property of odd numbers} \\
		&3. &&n^2 = (2k + 1)^2 = 4k^2 + 4k + 1 &&\text{square of sums} \\
		&4. &&n^2 = 2(2k^2 + 2k) + 1 &&\text{factorising} \\
		&5. &&n^2 \text{ is odd} &&\text{from 4. and prop. of odd numbers} \\
	\end{aligned}
$$

Notes about proofs

• Only premises are allowed as assumptions.

• Only rules explicitly defined can be used. Steps must be fully justified.

• Proof patterns seen before can be used as a strategy to find a proof, but the proofs can only use the rules defined.

• Do not use unnecessary premises. The conjunction of the premises used to prove something is precisely the atecedent (premise) of the tautology proved.

  To show $P,R\vee S,T,P\to Q⊢Q$, we only need $P$ and $P\to Q$. We could see this as proof that $P\to ((P\to Q)\to Q)$ is a tautology, hence the other premises are not needed.

• Classical logic is a monotonic reasoning system: adding assumptions preserves conclusions.

• Order of the premises in proofs are irrelevant. You can use the premises right at the point they are needed.

title: Example 3: Incorrect Argument
$$
	\neg (A \lor B), \neg C \rightarrow A \vdash C
$$
 
$$
	\begin{aligned}
	&1. &&\neg(A \lor B) &&\text{data} \\
	&2. &&\neg A \land \neg B &&\color{red}\text{since } \neg(A \lor B) \equiv \neg A \land \neg B \\
	&3. &&\neg A &&2. \text{ and } (\land E) \\
	&4. &&\vdots
	\end{aligned}
$$
 
The $\color{red}\text{step 2.}$ is not permitted unless we have a specific natural deduction rule whose premise we can instantiate with $1.$ to produce $2.$ But can be proven using [[1. Natural Deduction Rules#Rules for land lor and neg|the basic rules]], since they are complete.

Proof theory vs. semantics

In general, we want the proof system to closely match the semantics for of the logic it is used for. There are two important properties describing this relationship.

• Soundness of a proof system

  Soundness: A proof system is sound (or correct) if all of its rules are sound, whenever $A_1, ..., A_n \vdash B$ then $A_1, ..., A_n \models B$.

  Link to original

• Completeness of a proof system

  Completeness: A proof system is complete if whenever $A_1, ..., A_n \models B$, then $B$ can be derived from $A_1, ..., A_n$ using its inference rules.

  Link to original

Suppose a proof system $⊢$ is sound and complete. Then we know that:

$$A_1,...,A_n⊢B⟺A_1,...,A_n⊢B$$

So if $A_1,...,A_n/\models B$, then we know that $A_1,...,A_n/⊢B$.

This only means that we will not be able to find a proof for $B$ from $A_1,...,A_n$ but we may try to find it… if we are confident that $A_1,...,A_n/⊢B$ this means that $A_1,...,A_n/\models B$, so there must be a model of $A_1,...,A_n$ that is not a model of $B$.

Natural Deduction

Natural Deduction

Natural deduction is a type of forward reasoning proof system: the objective is to derive the conclusion of the argument, starting from its premises.

There are two ways of generating new conclusions in natural deduction: ?

• We either eliminate a connective from a formula in the proof to generate a new conclusion (via a connective elimination rule)
• We produce a new conclusion with a connective, by combining formulas in the proof (via a connective introduction rule)

Link to original

In general, coming up with a strategy to complete the proof is the hardest part.

Applying a rule

A rule may have premises or conditions. Consider the ($\wedge E$) “and-elimination” rule:

$$\wedge E:\frac{A\wedge B}{A}$$

Since this rule has $A\wedge B$ as a premise, before it can be applied you need to have $A\wedge B$ in the proof. The result of the application of the rule is a new item in the proof with the formula $A$ and the justification “from x. and ($\wedge E$)”.

title: Example 4
$$
	A \land B, A \rightarrow C \land D \vdash C
$$
 
$$
	\begin{aligned}
		&1. &&A \land B &&\text{data} \\
		&2. &&A \rightarrow C \land D &&\text{data} \\
		&3. &&A &&\text{from 1. and } (\land E) \\
		&4. &&C \land D &&\text{from 2., 3. and} (\rightarrow E) \\
		&5. &&C &&\text{from 4. and } (\land E) \\
	\end{aligned}
$$
 
Notice that every line in the proof is a logical consequence of the set of premises of the argument, and the proof is successful because it ends with the argument's conclusion.

Link to original