1
$\begingroup$

I'm having difficulty understanding the sequent/Gentzen proof system in section 8 of a paper by Gurevich [G1977], and he defines that system by telling the reader to modify the system G1 from Kleene's Introduction to Metamathematics (1952). Screenshots of the relevant pages from [G1977] and I.M. are posted below. I'm not sure I understand exactly what the rules are of Gurevich's system, since I'm not sure I understand the intuitionistic version of Kleene's G1 (I wish Gurevich had reproduced in his paper the needed rules of G1, as he understood them).

The difficulty is that I'm not sure how to interpret Kleene's statement:

The difference between the classical and intuitionistic systems G1 is secured by the intuitionistic restriction stated for two of the postulates.

Indeed, there are two rules which have a stated restriction: it says "with $\Theta$ empty for the intuitionistic system" beneath both the right negation rule (the rule with conclusion $\Gamma \to \Theta,\neg A$) and the right thinning rule (the rule with conclusion $\Gamma \to \Theta,C$). I have trouble believing that this is truly what Kleene meant however, since it seems that no restriction at all is put on the right implication rule (the rule with conclusion $\Gamma \to \Theta,A \supset B$). This seems like a problem because that rule is always restricted in other multi-conclusion intuitionistic sequent systems that I've seen (such as LJpm from Mint's "A short introduction to intuitionistic logic").

So perhaps the rules were presented with a typo? Or maybe alternatively Kleene means that $\Theta$ should be empty in every rule for the intuitionistic version of G1. However, this seems wrong as well because it isn't consistent with his comment on "two of the postulates". Additionally, it seems wrong because then there is a problem with the left implication rule (with conclusion $A \supset B,\Delta,\Gamma \to \Lambda,\Theta$): the left subderivation in that rule will have more than one formula in the succedent if $\Lambda$ is not empty.

Can anyone explain the correct interpretation of Kleene's rules for the intuitionistic case? Thanks.

[G1977] Gurevich, Y. (1977). Intuitionistic logic with strong negation.

screenshot of Gurevich system

screenshot of Kleene's G1 (part i)

screenshot of Kleene's G1 (part ii)

$\endgroup$
0

1 Answer 1

Reset to default
1
$\begingroup$

The two rules that you’re concerned about are sufficient for a sound and complete system for Intuitionistic Logic since you won’t be able to get “multiple” conclusions on the right unless $Θ$ is empty or Contraction is used. This follows from the restrictions on Thinning and $\neg$-right as well as the fact that ID is formulated as

$C \vdash C$

as opposed to

$\Gamma, C \vdash C, \Delta$

or something similar.

$\endgroup$
3
  • $\begingroup$ That makes sense. So essentially to confirm this observation you would prove by induction on the complexity of an intuitionistic derivation, that the number of formulas in the succeedent is one or zero. If I understand your answer correctly, this works out because the right negation and the right thinning rules are only two rules that allow the succedent of all the subderivations to get smaller (the left implication and cut rules are setup in a way that prevents either subderivation succeedent from getting smaller than the conclusion succeedent). $\endgroup$
    – tuiowalu
    Commented Jan 23 at 22:08
  • $\begingroup$ Based on your observation, it seems that the intuitionistic version of G1 is free to make unrestricted use of the right contraction rule. However, it is pointless to ever use that rule because the premise of the rule could never be provable. $\endgroup$
    – tuiowalu
    Commented Jan 23 at 22:10
  • $\begingroup$ After re-reading your answer I just noticed that you are viewing the rules from the perspective of "leaves to root / ground to conclusion", whereas my comments assume the perspective of "root to leaves / conclusion searching for ground". These are both equivalent, but I just wanted to point that out to clarify my comments. Please let me know if I am misunderstanding anything, thanks. $\endgroup$
    – tuiowalu
    Commented Jan 23 at 22:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .