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

  • 1
    $\begingroup$ I just rolled back the edit by @jeq - the mistakes of English in the original post did not, in my view, prevent one from understanding or reading the underlying question. $\endgroup$ – Yemon Choi Aug 21 '13 at 5:30
  • 1
    $\begingroup$ I would also ask @jeq if he or she has plans to ask or answer some questions on this site, or participate in exchanges in the comments? $\endgroup$ – Yemon Choi Aug 21 '13 at 5:31
  • 1
    $\begingroup$ @YemonChoi perhaps having a working link nevertheless could have been convenient. $\endgroup$ – user9072 Aug 21 '13 at 6:00
  • $\begingroup$ @quid in that case, why not correct the grammar in the 2nd sentence and the inconsistent capitalization? Why italicize the Latin tag and partially correct it without actually getting it right? This kind of tinkering says more to me about the tinkerer than anything else, I'm afraid $\endgroup$ – Yemon Choi Aug 21 '13 at 6:22
  • 1
    $\begingroup$ There was an other suggested edit, correcting the name of the mentioned author (which was already present in the first edit, essentially). Thus, I approved it and added the link in the process. @YemonChoi I don't know I am not so firm on such things myself. Still the edit seemed like a genuine improvement to me, even if it was not perfect. $\endgroup$ – user9072 Aug 21 '13 at 6:22

$\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.

| cite | improve this answer | |
  • $\begingroup$ I thought this answer correct until I recalled that there exist Hilbert style calculi with functorial variables (not just propositional variables). For example, there's a Hilbert calculus for conditional [C]-negation[N] classical logic with just the axiom C$\delta$pC$\delta$Np$\delta$q under substitution (which applies to all variables) and detachment. How does one obtain the theorem CpCNpq or the theorem CC$\delta$ppCC$\delta$NpNpC$\delta$qq in a sequent calculus? $\endgroup$ – Doug Spoonwood Apr 23 '14 at 5:01
  • $\begingroup$ I’m not familiar with your calculus, and I can’t say I fully understand the description, but I don’t see where is the problem. Just take the usual sequent calculus for classical logic augmented with $\Longrightarrow\delta(A)\to(\delta(\neg A)\to\delta(B))$ as an axiom. $\endgroup$ – Emil Jeřábek Apr 24 '14 at 11:42
  • $\begingroup$ ... Or rather $\Longrightarrow C(A)\to(C(\neg A)\to C(B))$, as you seem to allow substitution for $\delta$ as well. Or just include the relevant substitution rule in the sequent calculus. $\endgroup$ – Emil Jeřábek Apr 24 '14 at 15:08
  • $\begingroup$ I guess my question is, how is the substitution rule for δ, or "C" in your latest formula, expressible in sequent calculus? The notation I've seen writes something like $\delta$/C ' ' to indicate that $\delta$ should get substituted with C, then the argument belonging to $\delta$, and then the argument belonging to $\delta$ again. That is " ' " indicates that the argument that follows $\delta$ should go in that place. For instance, from the axiom C$\delta$pC$\delta$Np$\delta$q, $\delta$/ ' yields CpCNpq. $\delta$/C ' C N ' q yields CCpCNpqCCNpCNNpqCqCNqq. $\endgroup$ – Doug Spoonwood Apr 24 '14 at 16:22
  • $\begingroup$ I can’t make heads or tails of your notation, but then again, I fail to see what the notation for substitutions has to do with anything. The substitution rule is not expressible in either sequent or Hilbert calculus, it is expressed in the metatheory where the calculi are being defined. A substitution is a particular operation $A\mapsto\sigma(A)$ on formulas. The substitution rule in Hilbert calculus is “from $A$ infer $\sigma(A)$”, and in sequent calculus it’s “from $A_1,\dots,A_n\Longrightarrow B_1,\dots,B_m$ infer $\sigma(A_1),\dots,\sigma(A_n)\Longrightarrow\sigma(B_1),\dots,\sigma(B_m)$”. $\endgroup$ – Emil Jeřábek Apr 25 '14 at 11:07

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.