Inference in propositional logic



If we have a tautology, then we can substitute the formula of any propositional variable with any formula to arrive at any other tautology.

For example, we know that \(\theta \lor \neg \theta \) is a tautology. This means that an arbitrary formula for \(\theta \) is also a tautology.

An example is \((\gamma \land \alpha )\lor \neg (\gamma \land \alpha )\), which we know is a tautology, without having to examine each variable.

Syntactic consequence

Let us call the first formula \(A\) and the second \(B\). We can then say:

\(A\vdash B\)

This says that: if \(A\) is true, then we can deduce that \(B\) is true using steps such as substitution.

Modus Ponens

Modus Ponens is a deduction rule. This allows us to use stpes other than substitution to derive new tautologies.

If \(A\) implies \(B\), and \(A\) is true, then \(B\) is also true.

\((\theta \rightarrow \gamma )\land \theta \Rightarrow \gamma \)

That is, if we can show that the following are true:

\(\theta \rightarrow \gamma \)

\(\theta \)

We can infer that the following is also true:

\(\gamma \)


Results derived from substitution or induction are called theorems. Theorems often divided into:

  • Theorems - important results

  • Lemmas - results used for later theorems

  • Corollaries - readily deduced from a theorem

We take a set of axioms, as true, and a deduction rule which enables us to derive additional formulae, or theorems. The collection of axioms and theorems is known as the theory.

Principle of explosion

If axioms contradict each other then it is possible to derive anything. That is:

\(P\land \neg P\vdash Q\)

We can prove this. If \(P\) and \(\neg P\) are true, then the following is also true:

\(P\lor Q\)

We can then use \(P\lor Q\) and \(\neg P\) to imply \(Q\).

This works for any proposition \(Q\), including \(\neg Q\).

As we can derive \(Q\) and \(\neg Q\), our axioms are not consistent.

Resolution rule

Proof by resolution

If we have a string of or statements, \(A\lor B\lor C\), and another which contains the completement of one element \(X\lor \neg B\lor Y\), we can infer:

\(A\lor C\lor X\lor Y\)

If the second statement has only one formula, then we have:

\(A\lor B\lor C\) and \(\neg B\) implying \(A\lor C\)

Clauses and horn clauses

A clause is a disjunction of atomic formulae.

\(A\lor \neg B\lor C\)

This can be written in implicative form.

\((A\lor \neg B)\lor C\)

\(\neg (A\lor \neg B)\rightarrow C\)

\((\neg A\land B)\rightarrow C\)

A horn clause is a clause where there is at most one positive literal. This means the implicative takes the form.

\((A\land B\land C )\rightarrow X\).

Inference with horn clauses

If the horn clause is true, and so is the normal form part, then \(X\) is also true.

As all inference with horn clauses uses Modus Ponens, it is sound.

Inference with horn clauses is also complete.