1
$\begingroup$

I know that this sequent is true for classical logic. But is it true in minimal or intuitionistic logic?

What would be a Kripke model that doesn't satisfy the property?

I would appreciate some (as many as possible) Kripke model examples where classically true formulas are false.

I already have one where $\forall x\neg\phi\lor\neg\neg\phi$ is not true:

Kripke model

Here we have $\alpha\nvDash \neg P(a)\lor\neg\neg P(a)$

$\endgroup$

1 Answer 1

3
$\begingroup$

Yes, it is.

We can prove it without LEM or Double Negation.

1) $∃xψ(x) → ∀xθ(x)$ --- premise

2) $ψ(a)$ --- assumed [a]

3) $∃xψ(x)$ --- from 2) by $\exists$-I

4) $∀xθ(x)$ --- from 3) and 1)

5) $θ(a)$ --- from 4)

6) $ψ(a)→θ(a)$ --- from 1) and 5) by $\to$-I, discharging [a]

$∀x(ψ(x)→θ(x))$ --- from 7) by $\forall$-I.

$\endgroup$

You must log in to answer this question.

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