Is it decidable whether a classically valid first-order formula is also intuitionistically valid?

45 Views Asked by At

Intuitionistic first-order predicate logic is not decidable for arbitrary formulas.

However, suppose that we are given a formula of first-order predicate logic that is classically valid. Is there a decision procedure that will determine whether it is also valid intuitionistically?

1

There are 1 best solutions below

1
On BEST ANSWER

Restricting to classically valid formulas doesn't do anything here. Let $\psi$ be a fixed formula which is classically valid, but not intuitionistically. Now for a given formula $\phi$, consider $\psi \vee \phi$. This formula is classically valid, and it is intuitionistically valid if and only if $\phi$ was.