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.
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 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.
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.
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\)
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\).
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.