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.