How to prove consistency of Natural Deduction systems

Question

In Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965), we have the system I of intuitionistic (first-order) logic based on eleven introduction- and elimination-rules : the 3 couples for the connectives $\lor$, $\land$ and $\rightarrow$, the two couples for the quantifiers and the $\bot_I$ rule [page 20].

The system C of classical logic is obtained with the addition of the $\bot_C$ rule.

The system C’ is obtained from C excluding $\lor$ and $\exists$ and treating them as defined in the usual way [page 39].

It is assumed that the negation $\lnot A$ is an abbreviation for $A \rightarrow \bot$ [page 16] so that we do not need it.

A notion of consistency (if I’m not wrong) is not defined; Prawitz does not introduce a semantics, so that we can assume that a system is inconsistent if we have a proof [see page 24 for the definition] of $\bot$.

The first reference to consistency is on page 44 :

COROLLARY 3 [to the Theorem on normal deductions for classical logic] [the system] C’ is consistent; in particular, $\bot$ is not provable in C’.

A similar result is not stated for I; may we say that it is “implicit” in the above result ?

Regarding both systems, it seems to me that we can prove their consistency simply “by inspection”, due to the fact that there are no rules that “introduce” $\bot$. Where is the flaw in this argument ?

Added following a comment by Peter Smith

In Prawitz's book [page 14] the symbol $\bot$ is a sentential constant (absurdity).

In absence of the negation symbol, we must apply Post's definition of consistency. So, proving that $\bot$ is underivable is equivalent to proving that not every proposition is derivable ?

Added Jan,30

I made a research into Sara Negri & Jan von Plato, Structural Proof Theory (2001), due to the similarity between Natural Deduction and sequent calculus.

They say [page 16] :

The $\bot$E rule of natural deduction gives a zero-premiss sequent calculus rule: $$\frac{}{\bot \implies C}$$

Also, about the subformula property [pages 40-41] :

Since structural rules can be dispensed with in G3ip [intuitionistic propositional calculus], we find by inspection [emphasis added] of its rules of inference that no formulas disappear from derivations [...]. Similarly, a connective that has once appeared in a derivation cannot disappear. From this it follows in particular that $\implies \bot$ is not derivable, i.e., the calculus is syntactically consistent.

So, my question becomes :

May I exploit the similarity between the two calculus and conclude that, also for the system I of Prawitz, we can prove the consistency simply “by inspection”, due to the fact that there are no rules that “introduce” $\bot$ ?

Answer 1

See the article of Andrés Raggio, DIRECT CONSISTENCY PROOF OF GENTZEN'S SYSTEM OF NATURAL DEDUCTION (Notre Dame Journal of Formal Logic, 1964).

The proof "by inspection" does not work in Natural Deduction : we have for example the $\lor$-elimination rule that allows us to "introduce" a new formula $C$ that is not a subformula of the major premisse $A \lor B$.

The same for $\lor$-introduction, where we pass from $A$ to $A \lor B$.

We need induction on the derivation-tree.

Added March, 5

Now I've got it !

See the detailed study of Gentzen's unpublished manuscript thesis of 1932 in Jan von Plato, Gentzen's Proof Systems: byproducts in a work of genius (The Bull of Sumb Log, 2012), page 329.

In Gentzen's thesis there is a conjecture about the normalization theorem for derivation in intuitionistic natural deduction, then transformed into a proof.

In Gentzen's original presentation of natural deduction, finished formal derivations ended with the closing of all open assumptions. [...] With the closing of all open assumptions in the end, the conclusion became the longest formula in a derivation that also contained all the formulas in the derivation as subformulas, if no detours had been taken [emphasis mine].

"A closer inspection of the natural deduction calculus led me in the end to a general theorem that I want to call the 'Hauptsatz'. [...] The natural calculus proved not to be suitable."

Then, Gentzen "moved to" sequent calculus, but von Plato in his paper shows that he was able to find a proof (unpublished) also for intuitionistic natural deduction.

In conclusion, the conjecture that, if we do not have $\bot$ in the axioms (assumptions) the system is consistent, is not in general true; in order to assert it, we must be able to "avoid detours". The result must be attained in natural deduction through the normalization theorem.

Note. In natural deduction the presence of $\supset$-E (modus ponens) plays the role of cut : from $A$ and $A \supset B$ we derive $B$; in this way, we lose the "trace" of $A$.

In a system based on sequent calculus, instead, the consistency proof "by inspection" works because the "no detours" condition is "built in" into the rules: no assumption is lost during the derivation.

So, if $\bot$ is not present into the axioms, we may conclude that it will not be present in the conclusion.

Answer 2

About the question :

May we exploit the similarity between ND and sequent calculus in order to prove the consistency of I system simply “by inspection”, due to the fact that there are no rules that “introduce” $\bot$ ?

After having browsed Sara Negri & Jan von Plato, Structural Proof Theory (2001), Ch.8 : Back to Natural Deduction, I think that the "insight" is sound but it is not straightforward to transform into a proof, due to the nature of ND's rules , that admits assumptions.

They say [page 16] :

The $\bot$E rule of natural deduction gives a zero-premiss sequent calculus rule: $$\frac{}{\bot \implies C}$$

Also, about the subformula property [pages 40-41] :

Since structural rules can be dispensed with in G3ip [intuitionistic propositional calculus], we find by inspection [emphasis added] of its rules of inference that no formulas disappear from derivations [...]. Similarly, a connective that has once appeared in a derivation cannot disappear. From this it follows in particular that $\implies \bot$ is not derivable, i.e., the calculus is syntactically consistent.

We have that [page 183] :

by the translation of a normal derivation in natural deduction to sequent calculus, each formula in the former appears in the latter. We therefore have, by the subformula property of G0i, a somewhat surprising proof of

Corollary 8.3.3: Subformula property. In a normal derivation of $C$ from open assumptions $\Gamma$, each formula in the derivation is a subformula of $\Gamma$, $C$.

So (I think) is only after having obtained normalization that, from the subformula property we can conclude that a derivation of $\bot$ (i.e.inconsistency) is possible only if $\bot$ is a subformula of some of the premises.

If we apply this to the "pure" calculus, now we have consistency due to the fact that a proof of $\bot$ (i.e. $\vdash \bot$) would implies that $\bot$ is a subformula of the premises; but we have no premises.