How to prove that a formula is intuitionistically valid using Kripke semantics?

Question

I want to know how to use Kripke semantics so that I can prove that a formula is intuitionistically valid.

I think that all others cases will clear out if I understand the case of implication.

Let's say that I have the formula $\phi=((((p\rightarrow q) \rightarrow p)\rightarrow p)\rightarrow q)\rightarrow q$ which I know to be intuitionistically valid.

The definition using Kripke models in Sorensen says that

$c \Vdash a \rightarrow b$ iff $c' \Vdash b$ for all $c' \geq c$ with $c' \Vdash a$

($c, c' \in C$)

So how could I prove that the formula $\phi$ is valid?

Should I start with arbitrary $c \Vdash p$ and $c' \Vdash q$? Should I start with arbitrary $c \Vdash \phi$? How do I proceed in the first case?

If I follow the second case I get

$g \Vdash \phi $ iff $a \Vdash q$ for all $a \geq g$ with $a \Vdash \psi=(((p\rightarrow q) \rightarrow p)\rightarrow p)\rightarrow q$

$a \Vdash \psi $ iff $b \Vdash q$ for all $b \geq a$ with $b \Vdash \sigma=((p\rightarrow q) \rightarrow p)\rightarrow p$

$b \Vdash \sigma $ iff $d \Vdash p$ for all $d \geq b$ with $d \Vdash \tau=(p\rightarrow q) \rightarrow p$

$d \Vdash \tau $ iff $e \Vdash p$ for all $e \geq d$ with $e \Vdash \tau=p\rightarrow q$

$z \Vdash p\rightarrow q $ iff $h \Vdash q$ for all $h \geq z$ with $h \Vdash p$

But how do I conclude that it is valid for EVERY Kripke model?

Answer 1

So, contrary to my comment, you don't actually need any cases to prove this, although maybe that path would be easier for some people. Rather, the Kripke proof can be systematically built from the normal derivation, and the derivation follows a pretty rigidly determined series of moves:

1. The last step will be using $→$ introduction after $ψ ⊢ q$
2. The step preceding that will be $→$ elimination with the only premise, as that is the only way to derive $Q$. So we need to derive $ψ ⊢ σ$
3. This will be done by another $→$ introduction to prove $ψ,τ⊢p$
4. The only move before that is to use $→$ elimination with $τ$, requiring that we prove $ψ,τ⊢p→q$
5. This will be done by $→$ introduction, so we prove $ψ,τ,p⊢q$
6. $q$ follows from $→$ elimination with $ψ$ and weakening of $p$

All these steps have corresponding Kripke versions:

1. Suppose we know $Ψ = w_1 \Vdash ψ = ∀w_2\geq w_1. w_2 \Vdash σ → w_2 \Vdash q$. We need to derive $w_1 \Vdash q$
2. Instantiate $Ψ$ at $w_1 \geq w_1$ to get $w_1 \Vdash σ → w_1 \Vdash q$, so now we need to derive the premise
3. Suppose $Φ = w_2 \Vdash τ = ∀w_3\geq w_2. (w_3 \Vdash p→q) → w_3 \Vdash p$ for $w_2 \geq w_1$
4. Instantiate $Φ$ at $w_2 \geq w_2$ to get $(w_2 \Vdash p→q) → w_2 \Vdash p$. Now we need to derive $w_2 \Vdash p → q$
5. Suppose $w_3 \Vdash p$ for $w_3 \geq w_2$
6. Now instantiate $Ψ$ at $w_3 \geq w_1$ which holds by transitivity. Then in $w_4 \geq w_3$ we still have $w_4 \Vdash p$ by monotonicity, which will allow us to derive $w_4 \Vdash σ$, which in turn lets us derive $w_3 \Vdash q$ from our instantiation of $Ψ$

I don't know how clear it is, but all the deduction steps turn into Kripke steps that do essentially the same thing, but involve managing more premises, and sometimes making use of the preorder axioms.

Here is an Agda program that mechanizes the translation. On line 30, I proved your theorem in the embedding of the implication-only logic (without using the fact that that the type is technically empty). Then on line 61 and below, I ran the translation on the derivation, and the result was something very similar to what I described above.