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$ ?