# Inference in propositional logic

## Inference

### Substitution

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$$

### Theory

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.