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$ ?
Best Answer
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.
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.