Talk:Sequent calculus

Untitled

In fact, since Wikipedia has changed its layout recently, the tabular layout of the rule system included here looks awfully. Please feel free to typeset it in LaTeX... --Markus Krötzsch 22:49, 8 Jun 2004 (UTC)

A good layout for derivations as a wiki-table/TeX hybrid is given in the example derivation. The html-or does not display well on many browsers, so I prefer the TeX version. --Markus Krötzsch 14:48, 27 Jul 2004 (UTC)

I am typesetting all the derivations on (La)TeX my version --Miguel Pagano 20:35, 25 July 2005 (UTC)[reply]

@Dedalus (your wiki-email seems to be unavailable): Thanks for the extension -- your tabular layout via "hr" instead of underline is a good idea. I corrected some minor errors and changed the table to the more readable wikitable style. Other than this, the center tags do not work as expected (try to view your prior version without being logged in). I used align=center tags instead. --Markus Krötzsch 14:48, 27 Jul 2004 (UTC)

To add: extensions of sequent calulus; eg. 2-sequents, hypersequents, display logic, etc. --- Charles Stewart 02:50, 12 Aug 2004 (UTC)

HTML rendering problems on Firefox (Windows) of `&and;`, `<math>\and</math>` and `<math>\land</math>`

I am experiencing some html (i.e. not png) rendering problems on the sequent calculus page on Firefox (Windows) for quite some time. I have tried to fix this, but it has been without results so far.

The problem is in the html rendering of &and;, <math>\and</math> and <math>\land</math>. In Firefox, they show up as a small square (∧) most of the times.

I have been able to reproduce this problem in the sandbox, but this generates unpredictable results: sometimes the results are displayed correctly, and sometimes not! Refreshing the page can even toggle between right and wrong results. The problem is also present at other pages such as natural deduction and first-order logic.

I have confirmed this problem on a number of machines running Windows. I am aware of the fact this is possibly not the best place to post this problem, but I have no idea where to post it elsewhere.

Cheers, eboy 15:02, 7 November 2006 (UTC).[reply]

Weakening?

The intuitive explanations of the rules were very helpful - but the section on Structural Rules lists Weakening, PR, and Contraction, gives intuitive explanations of PR and Contraction but skips Weakening -- can anyone add to this? Zero sharp 06:36, 19 December 2006 (UTC)[reply]

I believe the axiom WR is wrong as stated. The A which should be in the bottom is at the top. Changing this right now. Jul 4 2011 — Preceding unsigned comment added by 75.94.102.93 (talk) 08:13, 5 July 2012 (UTC)[reply]

I believe the axiom WR is now incorrect, and the A should be at the top. What your edit now says is that if $\Gamma \vdash \Delta$ , then for any other formula $A$ , $\Gamma \vdash A$ which is patently incorrect. I've reverted your edit; if I'm in error then please let me know. Jetbeard (talk) 18:00, 21 October 2012 (UTC)[reply]

You are in error. The rule actually says that if

\Gamma \vdash \Delta

, then

\Gamma \vdash A,\Delta

for any formula

A

-- what's important is that the formulas

\Delta

remain in the conclusion. In terms of the standard classical semantics of sequents described in the introduction, this rule can be justified by saying that it is possible to weaken an assertion ("the conjunction of the

\Gamma

implies the disjunction of the

\Delta

") by adding an extra disjunctive possibility ("the disjunction of the

\Delta

or

A

"). Noamz (talk) 03:26, 22 October 2012 (UTC)[reply]

LK means Logistischer Kalkül

… I think. Gentzen says in the beginning of the paragraph in which he introduces it: “Die Kalküle LJ und LK. (Logistischer intuitionistischer und klassischer Kalkül.)”. He calls it “logistisch” because there are no assumptions. H. (talk) 15:53, 27 May 2009 (UTC)[reply]

I don't know for certain what it stands for, but I am sure that the "L" indicates the sort of calcus (sequent, vs. "N" for natural deduction), and the "K" indicates which logic (classical, vs. "J" for intuitionistic). It was asserted to me once that "J" was chosen over "I" for intuitionistic so that Gentzen was freed from arguing that his system was intuitionistic in the Brouwerian sense.

If you are right, then LK would abbreviate the adjectives applied to Kalkül, so that one could talk of the LK calculus as a particular subclass of the sequent calculus. Takeuti seems to have used the term in this way.

It all seems like guesswork to me, and I don't think we should be baldly asserting this as fact without a proper source. — Charles Stewart (talk) 10:54, 28 May 2009 (UTC)[reply]

Some web searches seem to confirm Hamaryns' "logistischer intuitionistischer und klassischer...", though a real source would be nice. Hamaryn: where are you reading the original German? In any case, I've removed the incorrect expansion of LK from the lede, replacing it by non-expansion. Noamz (talk) 06:44, 29 September 2009 (UTC)[reply]

I just looked it up in Gentzen (1934). He takes some time till he spells out what LK stands for, but on page 191, you finally find this: „Bei dem im folgenden anzugebenden logistischen klassischen Kalkül LK [...]“, meaning roughly: “In the logistic classical calculus LK specified below [...]”. So, the full German for LK is logistischer klassischer Kalkül (in nominative case).

BTW: What H. cites above („Die Kalküle LJ und LK [...]“) is the heading of the same section (Section 3, §1, page 190). When reading on, it is confirmed that „logistischer“ should be put in front of both „intuitionistischer Kalkül“ and „klassischer Kalkül“ (German allows for elliptic conjunctions at the expense of some ambiguity). I will clarify the article accordingly. --Thüringer ☼ (talk) 12:16, 29 September 2009 (UTC)[reply]

An example derivation

I cut the discussion following "This very rigid reasoning may at first be difficult to understand, but it forms the very core of the difference between syntax and semantics in formal logics". First of all, it doesn't. Finite sequences are no more formal than finite multisets (so I added a sentence about the possibility of giving a multiset presentation, which seems to have been discussed in a previous version of the article anyways, referenced in "Minor structural alternatives"). Second, the rest of the paragraph built on a confusion between the permutation rule and the disjunction right rules -- in this presentation of sequent calculus, A ∨ B is different from B ∨ A because there are two different right rules for disjunction, regardless of whether permutation is treated explicitly. Noamz (talk) 06:32, 17 October 2009 (UTC)[reply]

Little Myth Busting

Main Property of LJ is not that we have a single formula on the right side, i.e. the invariant:

  G |- A

Can easily make a classical logic by keeping the invariant by dispising (CR) and adding the following rule (X):

  G, B* |- A*
  -----------
  G, A |- B

With (~C)* = C and C* = (~C). And also vice versa, there are intuitionist logics with multiple formulas on the rightside.

One would need to dig deeper into the rules for negation to see what it means to be intuitionist or classical for a calculus.

Janburse (talk) 23:59, 13 April 2012 (UTC)[reply]

Edit: If we allow multiple formulas on the right hand side and structural rules on the right hand side, we can derive Peirce's law:

   ------ (I)
   A |- A
   --------- (WR)
   A |- B, A
   ------------(->R)   ------ (I)
   |- A -> B, A        A |- A
   -------------------------- (->L)
     (A -> B) -> A |- A, A
     --------------------- (CR)
       (A -> B) -> A |- A

I have seen the above proof recently in On the formulae-as-types correspondence for classical logic, Charles Alexander Stewart Worcester College, July 2000, p. 118. But the reference gives no original source, so don't know whether folklore or genuine.

LJ Rules

Considering space is not an issue for wikipedia, it would be kind to be explicit about the modified rules for LJ.

Perhaps create a new page LJ inference rules and place them there.

86.5.129.198 (talk) 20:43, 24 January 2013 (UTC)[reply]

Assessment comment

The comment(s) below were originally left at Talk:Sequent calculus/Comments, and are posted here for posterity. Following several discussions in past years, these subpages are now deprecated. The comments may be irrelevant or outdated; if so, please feel free to remove this section.

I think that there is a minor omission in the sentence that begins 'Restrictions:' at the end of the inference rules section. It fails to cover the case that the variables x and y may turn out to be the same variable. A very small correction (e.g. replacing '... the variable y must not be free ...' by '... unless the variable y is the same as the variable x it must not be free ...'.

Last edited at 11:29, 28 July 2009 (UTC). Substituted at 02:35, 5 May 2016 (UTC)

Are the restrictions in the quantifier rules correct?

After the rules for the quantifiers, the entry says:

Restrictions: In the rules $({\forall }R)$ and $({\exists }L)$ , the variable $y$ must not occur free within $\Gamma$ and $\Delta$ . Alternatively, the variable $y$ must not appear anywhere in the respective lower sequents.

How come the second part is an alternative to the first? In Gentzen's original paper, only the alternative was included. Also, and please correct me if I am wrong, the part before "Alternatively" seems insufficient: if this is the only restriction, that you can derive $\Rightarrow \forall x.x=y$ from $\Rightarrow y=y$ by taking $A$ to be $x=y$ .

If there isn't any mistake in this argument, I propose to include only the "alternative" restriction. — Preceding unsigned comment added by Yoni206 (talk • contribs) 18:48, 18 November 2017 (UTC)[reply]

The wording regarding substitution in LK

In the wording:

""" $A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the restriction that the term $t$ must be free for the variable $x$ in $A$ (i.e., no occurrence of any variable in $t$ becomes bound in $A[t/x]$ ). """

It was not defined what "term free for the variable in a formula" means and that confused me at first reading. But it was clarified with "(i.e., no occurrence of any variable in $t$ becomes bound in $A[t/x]$ )". This math.se QA also helps explain what "term free for the variable in a formula" means:

https://math.stackexchange.com/questions/2659471/what-does-it-mean-for-a-variable-to-be-free-for-something