Propositional Logic - Natural Deduction

Instead of that cumbersome truth table approach we can develop a kind of a calculus which can be used to do proofs. The idea is to use a set of rules to deduce whether the set of premises $ \Phi $ entails the conclusion $ \psi $. Here we use the symbol $ \vdash $, so formally we have $$ \phi_1,\phi_2, \dots \vdash \psi $$ This proof system we call Natural Deduction. Deduction is the idea of using a set of generally accepted rules to show something. It is often easier to prove something using Natural Deduction than for example truth tables. As we will see later one can freely choose between these two approaches since everything that can be shown to be a tautology using truth tabels, can be proven in natural deduction, and vice versa.

We start by introducing the rules. We usually have two types of rules, one called elimination, one called introduction. The former is a rule for deconstruction of the given connective, the latter is a rule for construction of the given connective. As stated in the intro we use BoxProver as a proof assistant. This application helps us by telling us when we do something incorrect. The following boiler plate code are needed in any proof. The markup I have on the page for natural deduction proofs can be outputted as BoxProver code directly by clicking on "send to raw".

%abbrev
proof_name : {p1}{p2} ... {pn} proof ( ... sequent ... ) =
[p1][p2] ... [pn]

 ... proof body ...

.

The rules for Conjunction

The first rule for conjunction is called and-introduction. It is given as $$ \frac{\phi\ \ \ \ \psi}{\phi \land \psi} \land i $$ We simply read it like: we know $ \phi $ is true, we know $ \psi $ is true, hence we can conclude that $ \phi \land \psi $ is true.

We have two rules for elimination, namely $$ \frac{\phi \land \psi}{\phi} \land e_1 $$ and $$ \frac{\phi \land \psi}{\psi} \land e_2 $$ These are also quite intuitive. We know we have $ \phi \land \psi $, hence we can conclude that we have $ \phi $, but we can also conclude that we have $ \psi $.

We can with this rule prove that $ p \land q, r \vdash q \land r $, we get

p /\ q assumption; [l1] r assumption; [l2] q by con_e2 l1 ; [l3] q /\ r by con_i l3 l2 .

We can also go straight ahead and prove that conjunction "commutes", that is $p \land q \vdash q \land p$, we get

p /\ q assumption; [l1] p by con_e1 l1 ; [l2] q by con_e2 l1 ; [l3] q /\ p by con_i l3 l2 .

The rules for Double Negation

We have that $ \neg \neg \phi \vdash \phi $. This one is also quite intuitive. It states that saying "It is not the case that I do not have a cat" is the same as saying "I do have cat" - though the former is way more confusing. We again have two rules, first elimination $$ \frac{\neg \neg \phi}{\phi} \neg \neg e $$ Second introduction $$ \frac{\phi}{\neg \neg \phi} \neg \neg i $$ Now we can prove something like $ \neg \neg (p \land q) \vdash \neg \neg p \land q $, we get:

~ ~ (p /\ q) assumption; [l1] p /\ q by nne l1 ; [l2] p by con_e1 l2 ; [l3] ~ ~ p by nni l3 ; [l4] q by con_e2 l2 ; [l5] ~ ~ p /\ q by con_i l4 l5 .

Rules for Implication

The rule for elimination is pretty straight forward. It is the same as modus ponens that were mentioned in the last chapter. We have $$ \frac{\phi \ \ \ \phi \rightarrow \psi}{\psi} \rightarrow e $$ We can extend it with a rule for modus tollens, (this is called a derived rule, more on those later), that is $$ \frac{\neg \psi \ \ \ \phi \rightarrow \psi}{\neg \phi} MT $$ We can use implication elimination to show that $ p, p \rightarrow q, q \rightarrow r \vdash r $. We get

p assumption; [l1] p => q assumption; [l2] q => r assumption; [l3] q by imp_e l1 l2 ; [l4] r by imp_e l4 l3 .

Conversely we can use MT to show that $ \neg r, p \rightarrow q, q \rightarrow r \vdash \neg p $

~ r assumption; [l1] p => q assumption; [l2] q => r assumption; [l3] ~ q by mt l3 l1 ; [l4] ~ p by mt l2 l4 .

The introduction rule for implication is a bit more involved than what we have seen yet. We want to show that $ \phi $ implies $ \psi $. In order to do so we assume that $ \phi $ is true, and then we show that $ \psi $ follows from this assumption. The rule is stated as $$ \frac{[ \phi \cdots \psi ]}{\phi \rightarrow \psi} \rightarrow i $$ Here the square brackets denotes a proof box. The results herein cannot be used outside, for example we cannot use the assumption $ \phi $ or any intermediate result outside this box. With this rule at hand we can for example prove that implication is transitive, that is $ p \rightarrow q, q \rightarrow r \vdash p \rightarrow r $. We get:

p => q assumption; [l1] q => r assumption; [l2] ( p assumption; [l3] q by imp_e l3 l1 ; [l4] r by imp_e l4 l2 ) ; [imp1] p => r by imp_i imp1 .

With the system we have developed up till now we can show that $ p \land q \rightarrow r \vdash p \rightarrow (q \rightarrow r) $. We get:

p /\ q => r assumption; [l1] ( p assumption; [l2] ( q assumption; [l3] p /\ q by con_i l2 l3 ; [l4] r by imp_e l4 l1 ) ; [imp1] q => r by imp_i imp1 ) ; [imp2] p => (q => r) by imp_i imp2 .

We can also show that $ p \rightarrow (q \rightarrow r) \vdash p \land q \rightarrow r $. We get:

p => (q => r) assumption; [l1] ( p /\ q assumption; [l2] p by con_e1 l2 ; [l3] q => r by imp_e l3 l1 ; [l4] q by con_e2 l2 ; [l5] r by imp_e l5 l4 ) ; [imp1] p /\ q => r by imp_i imp1 .

Note that we now have showed both ways, we write this as $ p \rightarrow (q \rightarrow r) \dashv \vdash p \land q \rightarrow r $. This states that the two formulas are logical equivalent, as discussed in the last article we use the $ \equiv $ meta symbol for this.

Rules for Disjunction

The introduction rule for disjunction is straight forward. It is a composite of two rules given as $$ \frac{\phi}{\phi \lor \psi} \lor i_1 $$ and $$ \frac{\psi}{\phi \lor \psi} \lor i_2 $$ The first one states that if we know $ \phi $, then we know $ \phi \lor \psi $. From the truth table of disjunction we know that $ \phi \lor \psi $ is true if at least one of the formulas is true. So this introduction rule is just an application of the semantics.

The elimination rule for disjunction is quite involved. We can see it as a doubled up version of the introduction for implication. It is given as $$ \frac{\phi \lor \psi \ \ [\phi \cdots \chi]\ \ [\psi \cdots \chi]}{\chi} \lor e $$ So we are given the assumption $ \phi \lor \psi $. From the semantics we know that at least one of these are true, we do not know which one. Hence we have to deal with both. This seems kind of counter intuitive, the nature of a disjunction states that of just one of the operands of the operator is true, then so is the whole disjunction. So why can't we just use one of the operators as assumption in order to show $ \chi $? Well, if we look up the truth table for $ (p \lor q) \rightarrow p $, we see that this is not a tautology. And remember: we want natural deduction to be so that everything that is provable in natural deduction, is a tautology when viewed as a truth table. Hence we have this restrictive elimination for disjunction.

Let's just go right ahead and show that $ p \lor q \vdash q \lor p $. We get:

p \/ q assumption; [l1] ( p assumption; [l2] q \/ p by dis_i2 l2 ) ; [dis1] ( q assumption; [l3] q \/ p by dis_i1 l3 ) ; [dis2] q \/ p by dis_e l1 dis1 dis2 .

Remember that the same rules apply: we cannot use any intermediate result inside an assumption outside of it. The above proof goes both ways, we can just rename the variables and show it again, hence we have that $p \lor q \dashv \vdash q \lor p$, or that these two formulas are logically equivalent. We can do yet an example. We have that disjunction distribute over conjunction, that is $p \land (q \lor r) \vdash (p \land q) \lor (p \land r)$. We get:

p /\ (q \/ r) assumption; [l1] p by con_e1 l1 ; [l2] q \/ r by con_e2 l1 ; [l3] ( q assumption; [l4] p /\ q by con_i l2 l4 ; [l5] (p /\ q) \/ (p /\ r) by dis_i1 l5 ) ; [dis1] ( r assumption; [l6] p /\ r by con_i l2 l6 ; [l7] (p /\ q) \/ (p /\ r) by dis_i2 l7 ) ; [dis2] (p /\ q) \/ (p /\ r) by dis_e l3 dis1 dis2 .

This goes the other way as well, hence we have that $ p \land (q \lor r) \equiv (p \land q) \lor (p \land r) $.

Rules of Negation

The rules for negation involves the notation of a contradiction. As stated in the semantics chapter a contradiction is a formula that has only $ \bot $ in the last column. This whole proof system is build on the idea of an implication. For example the introduction rule for conjunction might as well be stated as "If I know that $ \phi $ is true, and I know that $ \psi $ is true, then I know that $ \phi \land \psi $ is true". The nature of an implication states that if I know that $ \phi $ is false, then I can prove anything. Contradictions basically have the form $ p \land \neg p $, this is reasonable never true, so i can prove any formula $ \psi $ by assuming $ p \land \neg p $. That is $ p \land \neg p \rightarrow \top $. Intuitively this is kind of a mess, I mean now I can use the statement "The earth is flat" to prove anything. However this is part of natural deduction, it is stated as the rule bottom-elimination: $$ \frac{\bot}{\phi} \bot e $$ Now not elimination is given as $$ \frac{\phi \ \ \ \ \neg \phi}{\bot} \neg e $$ We can go right ahead and use this to show that $ \neg p \lor q \vdash p \rightarrow q $. We get:

~ p \/ q assumption; [l1] ( ~ p assumption; [l2] ( p assumption; [l3] bot by neg_e l3 l2 ; [l4] q by bot_e l4 ) ; [imp1] p => q by imp_i imp1 ) ; [dis1] ( q assumption; [l3] ( p assumption; [l4] q by copy l3 ) ; [imp1] p => q by imp_i imp1 ) ; [dis2] p => q by dis_e l1 dis1 dis2 .

Again we have that this goes the other way, too, so we have that $ \neg p \lor q \equiv p \rightarrow q $. The rule for not introduction is a bit more intuitive. Say we assume something which leads to a contradiction. Then this assumption must be false, right? Hence we have the rule as $$ \frac{[\phi \cdots \bot]}{\neg \phi} \neg i $$ These rules can be used to prove that $ \neg p \rightarrow \bot \vdash p $, this kind of formula is called prove by contradiction, or PBC for short. Notice the difference between not introduction and PBC. In the former the assumption is not negated, it is in the latter. We get:

p => bot assumption; [l1] ( ~ ~ p assumption; [l2] p by nne l2 ; [l3] bot by imp_e l3 l1 ) ; [neg1] ~ ~ ~ p by neg_i neg1 ; [l2] ~ p by nne l2 .

We state PBC as $$ \frac{[\neg \phi \cdots \bot]}{\phi} PBC $$ This rule along MT is what is called a derived rule. That is we derive it from the set of basic rules. We have one other noteworthy derived rule, namely Law of the Excluded Middle, shortened as LEM. This rule is quite handy. It is given as $$ \frac{}{\phi \lor \neg \phi} LEM $$ Notice that it has no conditions, that is it is always true, nothing is stated above the line. We call these kind of rules for axioms. This rule is quite intuitive, either you have something or you don't, either the sky is green or it isn't. And so on. We can prove LEM. It seems a bit tricky how to get started, since we do not have any assumptions to work on. However given the rules we have developed up till now, the most reasonable thing to do is to use either not introduction, or even better yet PBC. We get

( ~ (p \/ ~ p) assumption; [l1] ( ~ p assumption; [l2] p \/ ~ p by dis_i2 l2 ; [l3] bot by neg_e l3 l1 ) ; [case1] p by pbc case1 ; [l4] p \/ ~ p by dis_i1 l4 ; [l5] bot by neg_e l5 l1 ) ; [case2] p \/ ~ p by pbc case2 .

Notice that every assumption is within some box.