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?
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)
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.