I am puzzling with the question which of the two proof systems (Hilbert style axiomatic proofs or substructural Sequent Calculi) is the most discriminatory?
With discriminatory I mean is which proof system is more able to distinguish between different logics.
So are there logics that differ in Hilbert style axiomatic proof that are the same or not differently formalizable in sequent Calculi?
and
Are there logics that differ in sequent Calculi that are the same or not differently formalizable in Hilbert style axiomatic proof?
I was thinking that Hilbert style proofs are more discriminatory and as example I give minimal logic with the extra rule to keep the disjunctive syllogism valid
It is described in Johansson's minimal logic. See 'Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus'
In paragraph 3 she suggest to add to minimal logic an extra inference rule:
|- b v (a & ~a)
—————
|- b
To keep the disjunctive syllogism valid without making (a -> ( ~a -> b) (ex falso quodlibed) a theorem.
Can a similar rule be added to minimal logic as sequent calculi also without making
(a -> ( ~a -> b) a theorem?
Are there counter examples of logics that do differ in Sequent calculi but that cannot be differentiated in Hilbert style proof systems?
I made this on purpose a soft question, I would like to have some discussion over this problem.
Best Answer
$\let\seq\Longrightarrow$You can simulate any Hilbert calculus by a sequent calculus. In this particular example, there is nothing preventing you from adding the rule $$\frac{\seq B\lor(A\land\neg A)}{\strut\seq B}$$ (with no side formulas) to the usual sequent calculus for minimal logic. This calculus does not derive $A\to(\neg A\to B)$, and it is equivalent to your Hilbert calculus in the usual sense (the Hilbert calculus derives $A$ from $B_1,\dots,B_n$ iff the sequent calculus derives $\seq A$ from the sequents $\seq B_1,\dots,{}\seq B_n$, and conversely, a sequent $S$ is derivable from sequents $S_1,\dots,S_n$ iff the Hilbert calculus derives the characteristic formula of $S$ from the characteristic formulas of $S_1,\dots,S_n$.)
Whether that’s a useful thing to do is a different matter. The primary reason why sequent calculi are considered instead of the more simple Hilbert calculi is because they tend to have helpful structural properties like cut elimination, and throwing random rules into the calculus breaks that.
In the other direction, sequent calculi are more general than Hilbert calculi as in some situations, sequents have more expressive power than formulas. One example is the monotone calculus: the language consists of sequents built from propositional formulas using the connectives $\land,\lor,\bot,\top$. A sequent $A_1,\dots,A_n\seq B_1,\dots,B_m$ is satisfied under a valuation $v$ of formulas in a bounded distributive lattice if $v(A_1)\land\dots\land v(A_n)\le v(B_1)\lor\dots\lor v(B_m)$, and you define a logic (i.e., consequence relation) by postulating that a sequent $S$ follows from sequents $S_1,\dots,S_k$ iff every such valuation that satisfies $S_1,\dots,S_k$ also satisfies $S$. This logic can be axiomatized in a natural way by a sequent calculus (with the usual additive rules for the lattice connectives), but it cannot be directly expressed by a Hilbert calculus as there is no implication connective in the language to replace the sequent arrows.