Who stole the axioms in Natural Deduction?

The study of Gentzen's sequent calculus give me the opportunity to propose some reflections about the concept of logical truth.

I'll refer to the english edition of Gentzen's works : The collected papers (1969), with additional references to Gaisi Takeuti, Proof Theory (2nd ed - 1987).

Sequent calculus LK and LJ assume as basic logical sequent a sequent of the form :

$A \rightarrow A$,

where $A$ can be any arbitrary formula [page 151].

A sequent of the form $A \rightarrow A$ is called also an initial sequent, or axiom [see Takeuti].

We may restrict the above sequents to atomic formulas $A$ [see Takeuti, page 19 : If a sequent is provable, then it is provable with a proof in which all the initial sequents consist of atomic formulas.]

As Gentzen explain [page 82], the "informal meaning" of $A \rightarrow A$ is $\vdash A \supset A$ [from the axiom $A \rightarrow A$, by $\supset$-R, we have $\rightarrow A \supset A$: i.e. we have a proof of $A \supset A$].

We have that [Takeuti, page 11] a formula $A$ is called LK-provable (or a theorem of LK) if the sequent $\rightarrow A$ is LK-provable, where a proof LK (or LK-proof), is a tree of sequents satisfying the following conditions:

(i) The topmost sequents are initial sequents

(ii) Every sequent except the lowest one is an upper sequent of an inference whose lower sequent is also in the proof.

Due to soundeness and completeness theorems for LK, we have that all and only the valid formulas are provable.

If we consider the basic logical sequents $A \rightarrow A$, with $A$ atomic, we may say that they are the quintessence of tautology (in the non technical sense of "trivial" logical truth).

This suggest to me a possible way of "reinterpreting" some pasages from Wittgenstein's Tractatus (1921) :

6.1 The propositions of logic are tautologies.

See in SEP Logical Truth :

"[Wittgenstein] claims that logical truths do not “say” anything (6.11). [...] Wittgenstein calls the logical truths analytic (6.11), and says that “one can recognize in the symbol alone that they are true” (6.113). He seems to have in mind the fact that one can “see” that a logical truth of truth-functional logic must be valid by inspection of a suitable representation of its truth-functional content (6.1203, 6.122). But the extension of the idea to quantificational logic is problematic [...]"

In sequent calculus we have also, as a corollary to the cut-elimination theorem, the subformula property [Takeuti, page 29] :

In a cut-free proof in LK (or LJ) all the formulas which occur in it are subformulas of the formulas in the end-sequent.

Gentzen's "Hauptsatz" is often described : "as stating that a proof can be so organized that the premisses of each step of inference are always simpler [or not more complicated] than its conclusion" [Sara Negri & Jan von Plato, Structural Proof Theory (2001), page xii].

This property seems to me the precise counterpart of Frege goal of the formalization :

that through formalization “we arrive at a small number of laws in which, if we add those contained in the rules, the content of all the laws is included, albeit in an undeveloped state” (Frege, Begriffsschrift, 1879).

My exposition boil down to the question :

May we say that sequent calculus support the idea that logical truth are the formulas provable from basic logical axioms, i.e. from fomulas that are "tautologies" (in the sense of "trivial" truth whose truth we may ascertain "by inspection") formed with "elementary propositions" (again Wittgenstein) ? And that these formulas are "analytic" (in the sense of Kant and Frege)?

In support of this interpretation (and this fact clarify, for me, also the interreletionship between logic and mathematics), I suggest to consider also the way in which Gentzen extends sequent calculus to arithmetic [page 151] :

A basic mathematical sequent is a sequent of the form $\rightarrow C$, where the formula $C$ represents a 'mathematical axiom'.

According to the above interpretation, the formula $C$ is not a "tautology", and the mathematical theorems proved in the sequent calculus with the addition of "mathematical axioms" are clearly nor more "analytic".

It is well-known that sequent calculus and natural deduction have their common origin in Gentzen's work.

There is a "standard" translation from cut-free derivations in the sequent calculus to natural deduction derivations [see Negri & von Plato, chapter 8].

In natural derivation there are no axioms : the said translation maps the sequent $A \rightarrow A$ into an assumption $A$.

So my final question is :

What is wrong in the above interpretation of logical truth "according to" sequent calculus ? Is it possible to reconcile it with natural deduction ?

Added March, 15

Following some comments, It's seems that is a little bit "improper" to call axioms the initial sequents; Gentzen did not do so. He uses the term only in the context of 'mathematical axioms', i.e. for basic mathematical sequent [page 151].

So we may "restore the simmetry" between sequent calculus and natural deduction : initial sequents are - exactly as assumptions - a way to "bootstrap" the inferences.

In conclusion, sequent calculus (exactly as natural deduction) support the idea that a logical calculus is based on inference rules : in this sense, it is eminently "formal".

Only when we "apply" it, i.e.introduce mathematical axioms (or axioms partaining to other sciences), we "introduce meaning".

If this view is sound, it seems to me to maintain a "strictly formal" characterization of logical truth; in order to characterize it we need semantics, via the concept of validity.

Solution 1:

I don't think there's necessarily anything deep going on here.

Your initial observation seems to be simply that we can trade logical axioms for rules of inference and vice versa. A Hilbert-type system tries to have as few rules of inference as possible (namely modus ponens; it needs at least one in order to be able to do anything) and puts all the work in the axioms, whereas sequent calculus goes to the other extreme and does all the work with a plethora of inference rules while sticking to the simplest imaginable axiom.

In principle it would be equally possible to phrase most of the non-logical axioms of a theory as rules of inference rather than axioms. For example, if we're doing Peano Arithmetic in natural deduction, we could choose to write the induction rule as $$\frac{n=0\to\psi \qquad (\forall n. n=x\to\psi)\to(\forall n.n=S(x)\to\psi)}{\psi} x\text{ not free in }\psi$$

The only reason why we're not routinely doing that is that we often want to collect the non-logical axioms as "objects of interest" themselves, to be manipulated, put into sets and so forth, which is technically more convenient if they are formulas than if they're rules of inference.

Thus I think the rule/axiom scale exemplified by Hilbert or Gentzen style is more or less orthogonal to the concept of "logical truth", taken to mean formulas that can be proved by purely logical means (whether these logical means are axioms or rules), without using any of the theory-specific rules/axioms.

Solution 2:

Be very careful here:

Wittgensteins tractatus

Wittgensteins tractatus was written long before Gentzens "Untersuchungen uber das logischen schliessen" (1916 vs 1933) so there is no real relation between them. (I think it is doubtful that Gentzen read Wittgenstein but that is quite another matter)

Natural deduction:

Gentzen found axiomatic logic not very like normal mathematical proofs (I think we can agree with him in this) and invented natural deduction, what he hoped works more like how mathematical proofs actualy are done. (Gentzen writes quite nice about this, "art of making mathematical proofs" and so, I cannot do justice to him in translation)

Normal mathematical proofs don't really reason with logical axioms but with inference rules so natural deduction therefore also has no logical axioms, the main difference is that while in most mathematical proofs the inference rules are implicit (not really mentioned) in Natural deduction these rules are explicitly mentioned.

Sequent calculus

Sequent calculus is more technical form of Natural Deduction, it allows more formula's at either side of the $ \rightarrow $ (except in the intuitionistic case where only one formula may be on the right side) and has so its own inference rules. (and it therefore again not like how mathematical proofs are really done, but still sequent calculus is a furtile logical study area , especially for the many different types of substructural logics (see http://en.wikipedia.org/wiki/Substructural_logic )

While informal as Gentzen explains the "informal meaning" of $A \rightarrow A$ is $A \supset A$. there is a fundamental difference between them.

The $ \rightarrow $ is not a connective, it is more like a boundary marker between the right (succesent) and left (antecedent) sections of a sequent (and so in every sequent you need one and can only have one)

And while informally it means that the conjunction of all formula's on the left side entails the disjunction of the formula's on the right side. Formally you have to be very careful, formula's and sequents are different formal entities $ A_1,....,A_n \rightarrow B_1,...,B_m $ is a sequent while $ A \supset B $ is a formula.

So calling $ B \rightarrow B $ an axiom is a bit a misnomer. an axiom is a formula, and this is a sequent so the name initial sequent is more in line. (but of course informaly calling it an axiom, as long as you realise that it is only informally so)

The sides of a sequent can be empty if the antecedent (left) side is empty the succesent (right) side is a theorem, if the right side is empty you may place the contradiction sign there. So $ \rightarrow B \supset B $ (empty antecedent) is a sequent as is $ B \supset B \rightarrow $ (empty succedent) and even just $ \rightarrow $ (both empty ) are welformed sequents.

But $ A \rightarrow (B \rightarrow B )$ and $ \supset $ are not wellformed.

A sequent is something between the meta language and formulas in, (compareble to the $ \vdash $ or $ \Rightarrow $ sign that is sometimes used instead of it.)

Sequent calculus has so its own inference rules and they are of the form on one or more sequents in , one sequent out. (quite like natural Deduction)

Ending with Godel

A last point not often enough mentioned (if at all), in Godels incompletenes theorems a proof is an axiomatic proof not a proof using natural deduction or sequent calculus.

Because an axiomatic proofs is just a list of formulas (where each formula in the list is a theorem) it is (relatively) easy codable.

Natural deduction and sequent calculus proofs, on the other hand, where not every formula is an theorem coding is just horrible.

Hopes this helps.