0

Recently I posted a question concerning the Deduction Theorem. However, I have seen rules written in sequent notation as well (i.e. φ⊢ψ⊢φ→ψ). I am confused as how the two are related. Particularly, I am wondering what is the difference between consequences and sequents. I have seen modus ponens and a lot of inference rules written in sequent notation. Can you write these rules as consequences (for example sets) as well? Any help would be greatly appreciated.

Mauro ALLEGRANZA
  • 94,169
W. G.
  • 1,766
  • Sequent Calculus is a proof system with a peculiar formalization. Formulae are the "usual" ones, written wit connectives (like: $\lnot, \to$) and quantifiers, but the "basic object" of the calculus is not the formula but the sequent: $\Gamma \vdash \Delta$, where $\Gamma$ and $\Delta$ are sets of formulas and the "turnstile" $\vdash$ express the relation of consequence. – Mauro ALLEGRANZA Apr 24 '17 at 13:52
  • The rules of the calculus are stated in term of sequents and they formalize the way we can "transform" one or more sequents into a new one, like the rule for $\to$-R (corresponding to $\to$-intro) : from the sequent: $\Gamma, A \vdash \Delta,B$ the new sequent $\Gamma \vdash \Delta, A \to B$ can be derived. – Mauro ALLEGRANZA Apr 24 '17 at 13:55
  • I thought sequents are not sets as (as hyperlinked for sequents under the question). Does that mean that deduction theorem written in sequent form (for the i.e.) is different than that of the other form? – W. G. Apr 24 '17 at 16:23
  • I did not know that. I know what those are! Isn't the deduction theorem https://en.wikipedia.org/wiki/Deduction_theorem as shown here not a multiset though because of the union? – W. G. Apr 24 '17 at 16:30
  • One more question if you can answer it in the answer box that will be fantastic! If you have a syntactic consequence as shown here, https://en.wikipedia.org/wiki/Logical_consequence are these multisets? That would make complete sense if that was a multiset. The union part makes sense then. – W. G. Apr 24 '17 at 16:35
  • Why "That would make complete sense if that was a multiset. The union part makes sense then." The union $\cup$ operation works for sets... – Mauro ALLEGRANZA Apr 24 '17 at 16:43
  • The use of sets vs multisets is only nitpicking... In Hilbert-style and ND the sets of premises (see $\Gamma \vdash \varphi) are sets because in a derivation we can re-use a premise multiple times. – Mauro ALLEGRANZA Apr 24 '17 at 16:46

1 Answers1

1

Sequent Calculus is a proof calculus with a peculiar formalization.

Formulas are the "usual" ones, written wit connectives (like: $¬,→$) and quantifiers, but the "basic object" of the calculus is not the formula but the sequent: $Γ⊢Δ$, where $Γ$ and $Δ$ are multisets of formulas and the "turnstile" $⊢$ express the relation of consequence.

The rules of the calculus are stated in term of sequents and they formalize the way we can "transform" one or more sequents into a new one, like the rule for $→$-R (corresponding to $→$-intro of Natural Deduction):

$$\dfrac {Γ,A ⊢ Δ,B}{Γ⊢Δ,A→B}$$

that reads: from the sequent: $Γ,A ⊢ Δ,B$ the new sequent $Γ⊢Δ,A→B$ can be derived.

As you can see, this rule embeds the feature of the Deduction Theorem.

The same is for Natural Deduction with the $→$-intro rule.

Mauro ALLEGRANZA
  • 94,169