I'm not sure to understand how I should see the role of deductions systems like the Sequent Calculus.
- I've always see them as mere syntactic "tools" to formalize deductions/inferences in a logical system.
But it is said in the Blind Spot, Chapter 3.1.1, (J-Y Girard) that
Sequent calculus is due to Gentzen (1934). It is a formulation, among others, of predicate calculus. [...]
Before Gentzen, logic was formulated in "Hilbert-style" formal systems [...]
What does he meant by a "formulation of predicate calculus". Can we see the Sequent Calculus as an independant primitive definition of a logic i.e An alternative to the usual presentation of logic ?
So what is the relation between these systems and the usual formalization of logic as we can often see under the form Syntax + Semantic.
We start with a language: a set of basic symbols and a set of syntactical rules.
Syntax defines the "well formed" expressions of the language: the formulae.
Semantics defines the meaning of the expressions and their truth-value.
First order logic is defined by the use of quantifiers restricted to individual variables: no quantification of predicate symbols is allowed.
We focus the attention on a subset of the "meaningful" formulae : the (universally) valid ones.
The calculi or proof systems are aimed at deriving all and only the valid formulae.
Historically, various "styles" of proof systems has been found : from Frege to Russell & Whitehead's Principia Mathematica and then Hilbert, the first formalizations of the logical calculus (first the predicate one and then the propositional one) were organized with axioms (many) and rules (typically one or two : modus ponens and generalization).
The modern "codification" can be found into Hilbert & Ackermann's Grundzüge der theoretischen Logik (1928), and thus we usually call this formulation as : "Hilbert-style".
In the '30s Gerhard Gentzen formulated the rules-only calculus of Natural Deduction and the related Sequent Calculus.
All them are alternative formulations of (propositional and first-order) logic and they are equivalent in the sense that the respective calculus are all sound and complete for (propositional and first-order) validity.
Maybe of interest :
John Corcoran, Three Logical Theories (1969)
John Corcoran, Conceptual Structure of Classical Logic (1972)
Stewart Shapiro, Varieties of Logic (2014).