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.