10
$\begingroup$

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.

$\endgroup$
  • 5
    $\begingroup$ The Grinch did. And he's holding them hostage until you cancel Christmas. $\endgroup$ – Asaf Karagila Mar 13 '14 at 21:44
  • 1
    $\begingroup$ @AsafKaragila - according to von Plato, Gentzen was "a genius"... Are you suggesting that he was the "bad genius" who stole "my beloved" axioms ??? $\endgroup$ – Mauro ALLEGRANZA Mar 14 '14 at 8:46
  • $\begingroup$ "It is well-known that sequent calculus and natural deduction have their common origin in Gentzen's work." No, this is not well-known. Jaskowski's paper predates Gentzen's paper. sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf The axioms were not stolen from propositional calculus, because the axiomatic approach came as the new approach to begin with (and there does not exist any set of "natural" axioms to begin with). A better question comes as "who stole the rules?" since having only modus poenendo ponens is awkward. And the thief of rules appears to be Frege. $\endgroup$ – Doug Spoonwood Mar 18 '14 at 3:43
7
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks for your comments; I know that, in general, a sequent $A_1, ... , A_n \rightarrow B_1, ... , B_m$ must be "read" as : $A_1 \land ... \land A_n \supset B_1 \lor ... \lor B_m$. When $n=m=1$, this boils down to : $A \supset B$ $\endgroup$ – Mauro ALLEGRANZA Mar 13 '14 at 21:40
  • 1
    $\begingroup$ NO you are not careful enough, they are different formal entities $ A_1,...., A_n \rightarrow B_1, ..., B_m $ is a sequent while $A \supset B$ is a formula. more examples $ \rightarrow B \supset B$ is a sequent as is $ B \supset B \rightarrow $ and even just $ \rightarrow $, but $ A \rightarrow ( B\rightarrow B) $ and $ \supset $ are not wellformed. A sequent is something between the meta language and formulas in $\endgroup$ – Willemien Mar 13 '14 at 22:11
  • $\begingroup$ I agree that "$\rightarrow$" is sequent calculus is not a conncetive; see Negri & von Plato [page 14] : "Sequent calculus is a formal theory of the derivability relation. To make a difference to writing $\Gamma \vdash C$, where the turnstile is a metalevel expression, not part of the syntax as are the formulas, we use the now common symbol $\implies$." $\endgroup$ – Mauro ALLEGRANZA Mar 14 '14 at 15:45
  • $\begingroup$ rewritten my answer, (more info) and some more and so $\endgroup$ – Willemien Mar 14 '14 at 19:53
  • $\begingroup$ Thanks: I appreciate the new comments. About Wittgenstein, I rewrite a little bit the passage : of course, I'm not alluding to an influence (from W to G ...) but "to a possible way of 'reinterpreting' some pasages from Wittgenstein's Tractatus" that has been suggested to me by the study of sequent calculus. $\endgroup$ – Mauro ALLEGRANZA Mar 15 '14 at 7:48
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I agree with you about Induction rule,but Negri & von Plato modify Gentzen's sequent calculus without $\lnot$ and $\bot$ instead. They add the rule : $(void)/\bot, \Gamma \rightarrow C$. I suppose that, in the same way, Gentzen's "math sequent" $\rightarrow C$ can be stated as a rule : $(void)/\rightarrow C$. So, I understand that we may "play with" the two "baskets" of axioms and rules... But still I was struck by the "difference" between the "triavial" $A \rightarrow A$ and the not trivial $\rightarrow C$, and I'm wondering if this fact can be read as a "significant" fact. You say: NO. $\endgroup$ – Mauro ALLEGRANZA Mar 13 '14 at 18:07
  • $\begingroup$ There is a subtle issue with phrasing axioms as rules of inference. In many cases the rule of inference is strictly weaker than the corresponding axiom in the sense that there are models (of the remaining axioms) whose truth set is closed under the rule of inference but which do not satisfy the original axiom. And, in certain cases, the deduction theorem will fail when we turn previous axioms into new rules of inference. See mathoverflow.net/a/132295/5442 . I think this is a more important reason why we don't routinely convert axioms to rules of inference. $\endgroup$ – Carl Mummert Mar 13 '14 at 22:17
  • 1
    $\begingroup$ @Carl: Yes, generally each rule of inference needs some specific supporting machinery in order for the deduction theorem to go through. That's why I specified natural deduction for the example, since the deduction theorem is a primitive there, rather than a derived rule. On the other hand, I had not properly considered the extra demand such rules place on the "models" relation. $\endgroup$ – Henning Makholm Mar 13 '14 at 23:45
  • $\begingroup$ @Henning: I miswrote what I meant to say above. What happens (as in the other answer I linked) is not that the truth set is closed under the rule of inference; that would also close the truth set under the corresponding conditional axiom of course. What happens is that the closure of the other axioms under the inference rules does not contain the remaining axiom, which does mean there is a model of a certain kind that negates that remaining axiom. I am still thinking about what this means, in particular, when we work in a natural deduction system. $\endgroup$ – Carl Mummert Mar 14 '14 at 0:14
  • 1
    $\begingroup$ @Carl: Hmm, my intention was that you could derive the usual induction axiom by wrapping my rule in a couple of $\to$ introduction instances and a bit of quantifier footwork. Did I overlook something? $\endgroup$ – Henning Makholm Mar 14 '14 at 0:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.