0
$\begingroup$

Determine if the following sequent is provable in the classic logic, intuitionistic logic or minimal logic. $$ ( \exists x \psi(x) \rightarrow \forall x \theta(x) ) \vdash \forall x ( \psi(x) \rightarrow \theta(x) ) $$ Where $ \psi, \theta$ are two formula such that the only free variable is $x$. I can't use $\forall R$ to go up because $ \psi(x) \rightarrow \theta(x) $ possesses a free variable. I have no idea how to do it. Anyway how do understand in which logic is provable and in which one is not?

$\endgroup$
7
  • $\begingroup$ Which tools have been introduced in your course for showing that a certain sequent is not provable? $\endgroup$
    – Pilcrow
    Commented Jan 26, 2022 at 20:08
  • $\begingroup$ Model of Kripke for minimal and intuitionistic logic. $\endgroup$
    – 3m0o
    Commented Jan 26, 2022 at 21:19
  • $\begingroup$ Well, then you just try to prove it step by step in a sequent calculus. And if it seems like you can't, look for a counterexample in the form of a Kripke model. It is useful to work backwards. How do you prove a sequent of the form $\Gamma \vdash \forall x ~ \varphi$? Then, how do you prove a sequent of the for $\Gamma \vdash \psi \rightarrow \theta$? Etc. until you either find a proof or are convinced that one does not exist. $\endgroup$
    – Pilcrow
    Commented Jan 26, 2022 at 21:28
  • $\begingroup$ Yes, but for $ \Gamma \vdash \forall x \varphi $ you are supposing that $\varphi$ does not contain free variable, here i have a free variable... $\endgroup$
    – 3m0o
    Commented Jan 26, 2022 at 21:32
  • 1
    $\begingroup$ No, that's not what the restriction on this rule says. The restriction states that you may infer $\Gamma \vdash \forall x ~ \varphi$ from $\Gamma \vdash \varphi$ provided that $x$ is not free in $\Gamma$. $\endgroup$
    – Pilcrow
    Commented Jan 26, 2022 at 21:33

1 Answer 1

0
$\begingroup$

I try to answer my own question since I think i get how to prove it (at least in classic logic)

$$ \vdash \exists x \psi(x), \forall x( \psi(x) \rightarrow \theta(x) ; \forall x \theta(x) \vdash \forall x( \psi(x) \rightarrow \theta(x) $$ $$ \text{--------------------------------------------------- } \rightarrow L $$ $$ (\exists x \psi(x) \rightarrow \forall x \theta(x)) \vdash \forall x( \psi(x) \rightarrow \theta(x) $$

then for

$$ \text{--------------------------------------------------- axiom } $$ $$ \psi \vdash \psi $$ $$ \text{--------------------------------------------------- } P $$ $$ \psi \vdash \psi, \theta $$ $$ \text{--------------------------------------------------- } \rightarrow R $$ $$ \vdash \psi, \psi \rightarrow \theta $$ $$ \text{--------------------------------------------------- } L \exists , L \forall $$ $$ \vdash \exists x \psi(x), \forall x( \psi(x) \rightarrow \theta(x)$$ and for $$ \text{--------------------------------------------------- axiom } $$ $$ \theta \vdash \theta $$ $$ \text{--------------------------------------------------- } P $$ $$ \theta, \psi \vdash \theta $$ $$ \text{--------------------------------------------------- } R \rightarrow $$ $$ \theta \vdash \psi \rightarrow \theta $$ $$ \text{--------------------------------------------------- } R \forall $$ $$ \theta(t) \vdash \forall x( \psi(x) \rightarrow \theta(x) $$ $$ \text{--------------------------------------------------- } R \forall $$ $$ \forall x \theta(x) \vdash \forall x( \psi(x) \rightarrow \theta(x) $$

Hence it is prouvable in the classic logic. And since I don't think there exist a prove in sequent calculus with less than 1 right rule used then it is not provable in the intuitionistic logic, a fortiori in the minimal.

$\endgroup$
3
  • $\begingroup$ Firstly, the inference from "I don't think there exists a proof" to "it is not provable" is not valid. Secondly, you are proving the sequent in a valid but rather roundabout way. Instead, you should ask yourself: how do you prove a sequent of the form $\Gamma \vdash \psi \rightarrow \theta$? $\endgroup$
    – Pilcrow
    Commented Jan 27, 2022 at 14:42
  • $\begingroup$ (The point being that if you prove this in a more natural way, you might see that this can also be proved in intuitionistic logic.) $\endgroup$
    – Pilcrow
    Commented Jan 27, 2022 at 15:44
  • $\begingroup$ Yeah... the point is that I'm an idiot :) the variable $x$ is not free, so I can apply the rule that I wanted to apply $\endgroup$
    – 3m0o
    Commented Jan 28, 2022 at 0:09

You must log in to answer this question.

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