Natural Deduction

01.02.2021

Contents/Index

1. Introduction
2. Propositional Extension
3. Syntax
4. Semantics
@5. Natural Deduction
6. Equivalences

For the proof theoretical part of predicate logic we again just extend what we have developed for propositional logic. That is the natural deduction system. We extend it with a set of rules for the new operators.

Rules for equality

This rule is quite central to any reasoning system. A given term is equal to itself. We state this as $$\frac{}{t = t} = i$$ This is an axiom since it does not depend on any premises. Using semantic terminology the rule is a tautology. These appears in natural language as a figure of speech, like "a child is a child". You can't argue with that.

The rule can only be used on terms. As stated for propositional language equality between formulas is denoted with $\equiv$, and this operator is not part of the language - it is a meta operator.

The elimination rule for equality is given as $$\frac{t_1 = t_2 \ \ \ \phi[t_1 / x]}{\phi[t_2 / x]} = e$$ Here $t_1,t_2$ have to be free for $x$ in $\phi$. We can use this rule to prove that the relation = is symmetric. We get:

t_1 == t_2 assumption; [l1] t_1 == t_1 by eq_i ; [l2] t_2 == t_1 by eq_e ([x] x == t_1) l2 l1 .

We can also prove that the relation is transitive, we get

t_1 == t_2 assumption; [l1] t_2 == t_3 assumption; [l2] t_1 == t_3 by eq_e ([x] t_1 == x) l1 l2 .

Note in both proofs that we substitute from left to right. That is the second assumption in the last proof allow us to substitute the term $t_2$ with the term $t_3$.

Rules for forall quantifier

The elimination rule is given as follows $$\frac{\forall x . \phi}{\phi[t / x]} \forall e$$ It states that you given $\forall x . \phi$, a term $t$ and that $t$ is free for $x$ in $\phi$, can do $\phi[t/x]$. That is you can substitute $x$ with $t$ in $\phi$, and $\forall x . \phi$ remains true. This is quite straight forward.

The introduction rule for forall is a bit more complicated. It is given as $$\frac{x_0 \cdots \phi[x_0 / x]}{\forall x . \phi} \forall i$$ It involves a proof box as we have seen in propositional logic. However here the box is a scope for the variable/term $x_0$. The rule states that if we are given some arbitrary $x_0$ and can use this to prove $\phi$, then we conclude that every $x$ can be used to prove $\phi$. The idea is that since $x_0$ is picked arbitrary/random, any $x$ taken from the domain can take its place. Note that the instance $x_0$ cannot occur anywhere outside the scope box. This ensures that $x_0$ is not preconditioned, that is $x_0$ is truly arbitrarily picked.

We can use these forall-rules to prove that $$\forall x . P(x) \rightarrow Q(x), \forall x . P(x) \vdash \forall x . Q(x)$$ We get

all ([x] P x => Q x) assumption; [l1] all ([x] P x) assumption; [l2] (var [x_0] P x_0 => Q x_0 by all_e x_0 l1 ; [l3] P x_0 by all_e x_0 l2 ; [l4] Q x_0 by imp_e l4 l3 ) ; [all1] all ([x] Q x) by all_i all1 .

Rules for existential quantifier

The introduction rule for the existential quantifier is given as $$\frac{\phi[t / x]}{\exists x . \phi} \exists x i$$ It is pretty straight forward. It states that given $t$ is free for $x$ in $\phi$, and we can use this concrete $t$ to prove $\phi$, then we know that there exists some term that can prove $\phi$. Hence we travel from concrete to general. That is I have this $t$ that can be used as a instance for a proof, hence we know that there is some term that can be used in a proof.

The elimination involves a proof box (a scope). It is given as $$\frac{\exists x . \phi \ \ \ (x_0) \phi[x_o / x] \cdots \chi}{\chi} \exists e$$ It states that given $\exists x. \phi$, if we assume some fresh $x_0$ that is fresh for $x$ in $\phi$, we do substitution and are able to prove $\chi$, then we end know $\chi$. The behind reasoning is kind of the same as for $\lor e$. Since we do not know which of all possible $x_0$ that is used to prove $\chi$, we need examine all of them. Since we can't exhaust cases (there might be infinite many), we instead pick $x_0$ arbitrarily. Hence $x_0$ cannot appear outside the proof box/scope.

We can combine these rules to prove that $$\forall x . P(x) \rightarrow Q(x) , \exists x P(x) \vdash \exists x Q(x)$$ We get

all ([x] P x => Q x) assumption; [l1] exi ([x] P x) assumption; [l2] (var [x_0] P x_0 assumption; [l3] P x_0 => Q x_0 by all_e x_0 l1 ; [l4] Q x_0 by imp_e l3 l4 ; [l5] exi ([x] Q x) by exi_i x_0 l5 ) ; [exi1] exi ([x] Q x) by exi_e l2 exi1 .

We can also use the rules to prove that $$\forall x . P(x) \vdash \exists x . P(x)$$ Note that we have to restrict any model to be based on a non-empty set. Else the above is not generally true. That is let the domain be empty. Now $\forall x . P(x)$ is trivially true. But $\exists x . P(x)$ is never true. Anyway, we get

all ([x] P x) assumption; [l1] P x_0 by all_e x_0 l1 ; [l2] exi ([x] P x) by exi_i x_0 l2 .

...