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?
-
$\begingroup$ Which tools have been introduced in your course for showing that a certain sequent is not provable? $\endgroup$– PilcrowCommented Jan 26, 2022 at 20:08
-
$\begingroup$ Model of Kripke for minimal and intuitionistic logic. $\endgroup$– 3m0oCommented 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$– PilcrowCommented 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$– 3m0oCommented 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$– PilcrowCommented Jan 26, 2022 at 21:33
1 Answer
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.
-
$\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$– PilcrowCommented 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$– PilcrowCommented 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$– 3m0oCommented Jan 28, 2022 at 0:09