Formal Derivations and First-Order Logic

Natural Deduction §

A judgement of the form $A_1,...,A_n⊢A$ states that the proposition formula $A$ can be derived from the assumption of propositional formulae $A_1,...,A_n$. It is customary to represent a list of propositional formulae with $\Gamma$ (capital gamma), so that a judgement can be more concisely written as $\Gamma ⊢A$. A judgement is valid (correct) if $(A_1\wedge ...\wedge A_n)\leftrightarrow A$ is a tautology. A simple demonstration of this tautology (such as using a truth table) is sufficient as a#proof that a judgement is valid.

Inference Rules §

An inference rule

$$\frac{{\Gamma }_1⊢A_1,{\Gamma }_2⊢A_2,...,{\Gamma }_n⊢A_n}{\Gamma ⊢A}$$

states that the derived judgement (or conclusion) below the horizontal line can be deduced from the premises above the line. There are two general types of inference rules, introductions and eliminations. There are introduction and elimination rules for conjunction, disjunction, implication, negation and double negation. There are two other important rules:

• Axiom (starting point):

$$\frac{}{\Gamma ,A⊢A}$$

• Weakening:

$$\frac{\Gamma ⊢B}{\Gamma ,A⊢B}$$

Tip

See the full list of Natural Deduction Rules.

Proof §

To prove that the judgement $P,Q⊢P\wedge Q$ is valid, the following deduction can be offered:

$$\begin{array}{rlr}& P,Q⊢P& \text{Axiom.}\\ & P,Q⊢Q& \text{Axiom.}\\ & P,Q⊢P\wedge Q& \text{1, 2, }\wedge \text{ Intro.}\end{array}$$

Arguing Backwards §

It can be difficult to determine which assumptions must be made in order to prove a judgement, especially for more complex judgements. As such, it can be helpful to first identify one or more “subgoals” that are known to lead to a successful proof, and then attempt to prove those. For example, it is easy to see that the judgement $A\to (B\to C)⊢B\to (A\to C)$ may be deduced from the judgement $A\to (B\to C),B⊢A\to C$ using the implication introduction rule, so this becomes our first subgoal. The same reasoning can then be applied again, resulting in a second subgoal of $A\to (B\to C),B,A⊢C$. This subgoal can be easily deduced using the Axiom rule and Implication Elimination.

Definitions §

This natural deduction system is sound as every possible judgement can be proven using these rules if and only if the judgement is valid. This natural deduction system is complete as every possible valid judgement can be proven using these rules.

Exercise Sheet §