2
$\begingroup$

I know that if $A$ is a theorem of classical propositional logic, then $\neg \neg A$ is a theorem of intuitionistic propositional logic. I read in a previous question I asked long ago, that the corresponding statement for first order logic is false. Can someone give an explicit counterexample $A$?

$\endgroup$
3
$\begingroup$

$$ \neg \neg \forall x(p(x)\lor \neg p(x)) $$ is not a theorem of pure intuitionistic first-order logic.

Namely, it is false in the Kripke model with a countable infinity of worlds $$ w_0 \le w_1 \le w_2 \le \cdots \le w_n \le \cdots $$ where the individuals in each world are $\{1,2,3,\ldots\}$, and $p(n)$ is true from world $w_n$ onwards.

Then $p(n)\lor \neg p(n)$ is false in $w_{n-1}$, and therefore $\forall x(p(x)\lor \neg p(x))$ is false everywhen, so its double negation is equally false.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.