5
$\begingroup$

I have been reading Florian Steinberger's PhD thesis on harmony in sequent calculus, when he asserts that the left-intro rule is functionally equivalent to elimination rule.

His argument is attached at the bottom, but there are two things I don't understand:

  1. Why is $C$ being provable from $\Gamma, A\land B$ a fortiori? $\{\Gamma, A\land B\}$ is not really a stronger set of premises than $\{\Gamma, A\}$, since the latter can be strengthened to the former by left-$\land$ rule, but the former cannot revert back to the latter. In other words, it would seem that the former can prove less than the latter. So why is it a fortiori/for a stronger reason?

  2. Why is the upward extension (at the end of quotation) a justification of the two being functionally equivalent? I don't at all understand what he is trying to do with the last natural deduction ($\land$ elimination).


enter image description here enter image description here enter image description here

$\endgroup$
  • $\begingroup$ What is "Harmony in Sequent Calculus"? $\endgroup$ – David Tonhofer May 28 at 23:00
  • 1
    $\begingroup$ IMO "stronger" must be read as "more restrictive". Hypotheses $A$ is true when $A$ is true (trivial) while hypo $A \land B$ is true when $A$ and $B$ are true, i.e. in a more limited number cases (consider each valuation/truth assignment as a "model"). $\endgroup$ – Mauro ALLEGRANZA May 29 at 14:30
  • $\begingroup$ @DavidTonhofer Very simply put, in proof theoretic semantics, harmony is a restriction on logical constants so that the 'rogue' ones like tonk can be avoid. However almost all accounts of harmony are formulated exclusively on natural deduction, therefore whether a formulation for sequent calculus is possible is an interesting issue. $\endgroup$ – Daniel Mak May 29 at 19:51
  • $\begingroup$ @DanielMak Thanks. I found this: Proof-Theoretic Semantics. Yet more to read. Seriously, sometimes Logic feels like something invented by Jorge Luis Borges. $\endgroup$ – David Tonhofer May 29 at 20:16
  • 1
    $\begingroup$ @DavidTonhofer You may also find concise and accessible references here: web.archive.org/web/20120717025653/http://consequently.org/edit/… $\endgroup$ – Daniel Mak May 29 at 20:21
7
$\begingroup$
  1. You can say that the hypothesis $\Gamma, A \land B$ is stronger than $\Gamma, A$ because in $\Gamma, A \land B$ you have more hypotheses than in $\Gamma, A$. But the statement $\Gamma, A \land B \vdash C$ (i.e. $C$ is derivable from the hypotheses $\Gamma, A \land B$) is weaker (in the sense of less general or less informative) than the statement $\Gamma, A \vdash C$ (i.e. $C$ is derivable from the hypotheses $\Gamma, A$). The latter statement means that actually the hypothesis $B$ is not needed to derive $C$ from $\Gamma, A$. So, if you can derive $C$ from $\Gamma, A$, then a fortiori you can derive $C$ from $\Gamma, A$ plus another hypothesis ($B$) that actually is not needed.

  2. Technically, the issue is to show that any derivation in sequent calculus can be translated into a derivation in natural deduction, with the same conclusion and the same hypotheses. This translation is defined by induction on the size of the derivation in sequent calculus that has to be translated. Let us consider the case of the following derivation in sequent calculus (whose last rule is a left introduction of the conjunction): \begin{align}\tag{1} \dfrac{\quad \Pi \\ \Gamma, A \vdash C}{\Gamma, A \land B \vdash C} \land_{L_1} \end{align} By induction hypothesis applied to the derivation $\Pi$ (whose conclusion is $\Gamma, A \vdash C$), there is a derivation in natural deduction \begin{align} \Gamma, A \\ \vdots \Pi_0 \\ \!\!\!\!\!\!\!\!\!C \end{align} But if we add an elimination rule for the conjunction above $A$, we get the following derivation in natural deduction \begin{align} \Gamma,& \dfrac{A \land B}{A}\land_{E_1} \\ &\vdots \Pi_0 \\ &C \end{align} which is the translation of the derivation $(1)$ into natural deduction, with the same conclusion and hypotheses. In this sense, the introduction rule for the conjunction in $(1)$ corresponds to an upward extension of the derivation in natural deduction beginning with an elimination rule for the conjunction.


EDIT: Context and Preliminaries for the Two Questions.

I guess the context of what Streinberger wrote is to show the equivalence (or ''coextensivenes'') of natural deduction and sequent calculus: every proof in the former system can be translated into a proof in the latter formalism, with the same hypotheses and conclusion, and vice versa. In particular, the passage you cited is about the translation of a sequent calculus derivation into a natural deduction derivation. To be precise in the statement that you want to prove, you have to take into account a difference between sequent calculus and natural deduction: inference rules in natural deduction have an effect on formulas, whereas inference rules in sequent calculus have an effect on sequents, which are pairs of the form $\Gamma \vdash A$ where $A$ is a formula and $\Gamma$ is a sequence or multiset of formulas. For instance, look at the difference between the left rule for conjunction in the sequent calculus ($\land_{L_1}$) and the elimination rule for the conjunction in the natural deduction ($\land_{E_1}$, see above).

So, a derivation in natural deduction has the form \begin{align}\tag{2} \Gamma \\ \vdots \\ A \end{align} where $\Gamma$ is the set of undischarged hypotheses (roughly, the top formulas in the derivation), and $A$ is the conclusion (the bottom of the derivation).

A derivation in the sequent calculus has the form \begin{align}\tag{3} &\vdots \\ \Gamma &\vdash A \end{align} where the sequent at the bottom of the derivation contains both the hypotheses $\Gamma$ and the actual conclusion $A$.

Thus, in the passage you cited, Streinberger aims to prove that every sequent calculus derivation of the form $(3)$ can be translated into a natural deduction derivation of the form $(2)$ (in the passage you cited he does not consider the vice versa, I suppose he deals with it somewhere else). The idea of the proof is to define a rule-by-rule translation, i.e. to show that every inference rule in the sequent calculus can be translated into one or more inference rules in the natural deduction. This translation is quite easy to define for the right rules in the sequent calculus, since their behavior is analogous to the introduction rules in the natural deduction. The translation of the left rules in the sequent calculus is more delicate, since in the natural deduction apparently there are no similar rules. As shown by Steinbergerer in the case of conjunction (see above), the idea is that left rules in the sequent calculus modify the part of hypotheses in a sequent, so they can be simulated in the natural deduction by elimination rules.

$\endgroup$
  • $\begingroup$ @DanielMak - No, from what Streinberger wrote (or at least, in the passage you cited), he starts from a proof in sequent calculus of the sequent $\Gamma A \land B \vdash C$, whose last rule is a left introduction of $\land$. $\endgroup$ – Taroccoesbrocco May 29 at 20:13
  • $\begingroup$ There he seems to be explaining the meaning of what that sequent proof is (the 'a fortiori' sentence), then by constructing the same natural deduction proof that goes from $\Gamma, A$ proving C, to $\Gamma, A\land B$ proving C with the help of $\land$-E, he is justifying that the sequent proof is functionally equivalent to $\land$-E because the natural deduction proof can only prove the same provability with $\land$-E...no? $\endgroup$ – Daniel Mak May 29 at 20:37
  • $\begingroup$ So instead of a co-extension proof which proves that both sequent calculus and natural deduction can prove the same results, it seems to be just a qualitative argument for why $\land$-L is 'the same' as $\land$-E (but the idea is very similar to yours; in fact what I wrote above was inspired by your explanation) $\endgroup$ – Daniel Mak May 29 at 20:39
  • $\begingroup$ I've added the paragraph above the original excerpt in the edit if that helps $\endgroup$ – Daniel Mak May 29 at 20:43
  • $\begingroup$ @DanielMak - I edited my answer, adding a part about the context of your questions. I hope it can help you! $\endgroup$ – Taroccoesbrocco Jun 1 at 18:24

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.