Seeking help to understand a simple Kripke model

Question

I'm reading A Brief Introduction to the Intuitionistic Propositional Calculus, at page 7, there is a simple Kripke model represented by a graph, I interpret it as:

• $W = \{w_1, w_2\}$
• $w_1 \ge w_2$
• $w_2 \models \alpha$

In this simple Kripke model, the author states that $\lnot \lnot \alpha \Rightarrow \alpha$ (double negation elimination) fails at $w_1$, which I don't follow.

I attempted to prove by contradiction, but failed:

To show $w_1 \models \lnot \lnot \alpha \Rightarrow \alpha$, we want: $\forall v \in W, v \ge w_1, \text{if } v \models \lnot \lnot \alpha, \text{ then } v \models \alpha$

The only instance that satisfies $\forall v \in W, v \ge w_1$ is $w_1$ itself, but since $w_2 \le w_1$ and $w_2 \models \alpha$, we know by definition of Kripke model that $w_1 \models \alpha$. So the conclusion $ v \models \alpha$ always holds.

I don't think this conclusion is right, so I look into the precondition $v \models \lnot \lnot \alpha$, of which the only instance is $w_1 \models \lnot \lnot \alpha$. This holds if and only if $\forall v \ge u, v \not\models \lnot \alpha$.

I got stuck here because I can't find a rule to apply on $v \not\models \alpha$ from page 6.

So far I can only show the law of the excluded middle fails at $w_1$ (not sure if it is correct though) but have no idea about this double negation elimination nor Peirce's law. Since in page 4 it says that triple negation reduction is an intuitionistic tautology, I want to test if $\lnot \lnot \lnot \alpha \Rightarrow \lnot \alpha$ fails, but failed to do so due to a similar reason.

Is there something I missed or am I doing something totally wrong?

Answer 1

I use Polish notation. The formation rules run as follows:

1. All lower case letters of the Latin alphabet are formulas.
2. If x is a formula, then Nx is a formula.
3. If x and y are formulas, then so are Cx y, Ax y, and Kx y.

One can axiomitize intuitionistic propositional calculus as given in your reference as follows under the rules of uniform substitution, and implication elimination/detachment: {Cx y, x} $\vdash$ x, as follows.

1. C p Cqp.
2. C CpCqr C Cpq Cpr. (1 and 2 together allow us to prove the Deduction Meta-Theorem)
3. C p C q Kpq (conjunction introduction)
4. C Kpq p (conjunction elimination left).
5. C Kpq q (conjunction elimination right).
6. C p Apq (disjunction introduction left).
7. C p Aqp (disjunction introduction right).
8. C Apq C Cpr C Cqr r (disjunction elimination).
9. C Cpq C CpNq Np (negation introduction).
10. C Np Cpq (negation elimination).

Using Mace4 I found the following 3-valued model of those axioms and the rule of inference which allows to check the claim here. "2" is the designated element. Also "1" corresponds to "falsum" of two-valued logic:

A  0  1  2  C  0  1  2  K  0  1  2  N
0  0  0  2  0  2  1  2  0  0  1  0  1
1  0  1  2  1  2  2  2  1  1  1  1  2
2* 2  2  2  2  0  1  2  2  0  1  2  1

Notice that C NN0 0=C N1 0=C20=0. Thus, CNNpp does not hold in intuitionistic logic. Now, we only need to check all 10 claims above for each value of one variable.

1. So, for C p Cqp, we have C 0 Cq0. C 0 C00=C02=2, C 0 C10=C02=2, C 0 C20=C02=2. Thus, C 0 Cq0. Notice that $\forall$x, C1x=2. Thus substituting x with Cq1, we have that C 1 Cq1=2. Notice that $\forall$y, C2y=y. Thus, substituting y with Cp2 we have C2Cq2=Cq2. We do have that $\forall$q, Cq2=2. So, we have that C 2 Cq2=2. Thus, since we have C 0 Cq0=2, C 1 Cq1=2, and C 2 Cq2=2, it follows that C p Cqp=2.

2. C C2Cqr C C2q C2r= C Cqr Cqr, since $\forall$x, C2x=x. Note that $\forall$x Cxx=2. Substituting x with Cqr we obtain C Cqr Cqr. Thus, C C2Cqr C C2q C2r=2. C C1Cqr C C1q C1r=C 2 C22=C22=2. C C0Cqr C C0q C0r... C C0C2r C C0q C02=C C0C2r C C0q 2=C C0C2r 2=2. C C0C1r C C01 C0r=C C0C1r C 1 C0r= C C0C1r 2=2. C C0C00 C C00 C00= C C0C00 C C00 2= C C0C00 2=2. C C0C01 C C00 C01=C C0C01 C C00 1=C C0C01 C21=C C0C01 1=C C01 1=C11=2. So, C C0C0r C C00 C0r, C C0C1r C C01 C0r, C C0C2r C C02 C0r all hold leading to C C0Cqr C C0q C0r. And thus we obtain C CpCqr C Cpq Cpr=2.

3. C 0 C q K0q... C 0 C 0 K00=C 0 C 0 0, which is an instance of C p Cqp. So, C 0 C 0 K00=2. C 0 C 1 K01=C02=2. C 0 C 2 K02=C 0 K02=C00=2. Thus, we can infer that C 0 C q K0q=2. C 1 C q K1q=2 by the above. Note that $\forall$y K2y=y. Thus, C 2 C q K2q=C 2 Cqq. Cqq=2, and thus C 2 Cqq=C22=2. Since we've covered all three cases, C p C q Kpq=2.

4. C K0q 0... C K00 0=C00=2. C K01 0=C10=2. C K02 2=C00=2. So, C K0q 0=2. Note that $\forall$y, K1y=1. So, C K1q 1=C11=2. C K2q 2=2 by the above. Therefore, C Kpq p=2.

5. Notice that $\forall$x$\forall$y Kxy=Kyx. Thus, since C Kpq p=2, C Kqp p=2. Therefore, C Kpq q=2.

6. C 0 A0q... C 0 A00=C00=2, C0 A01=C00=2, C0 A02=C02=2. Thus, C 0 A0q. C 1 A1q=2 by the above. Note that $\forall$y, A2y=2. Thus, C 2 A2q=C22=2. Therefore, C p Apq=2.

7. Notice that $\forall$x, $\forall$y, Axy=Ayx. Thus, since C p Apq=2, it follows that C p Aqp=2.

8. C Apq C Cp0 C Cq0 0 ... C A0q C C00 C Cq0 0=C A0q C 2 C Cq0 0=C A0q C Cq0 0... C A00 C C00 0=C 0 C C00 0, which is an instance of CpCqp. So, C A00 C C00 0=2. C A01 C C10 0=C 0 C C10 0... which is an instance of CpCqp. So, C A01 C C10 0=2. C A02 C C20 0=C 2 C20 0. This is an instance of C p C Cpq q. This is provable from the axioms CpCqp, and CCpCqrCCpqCpr under detachment. Since if Cpq=2, as well as p=2, then q=2 holds by the above table, it thus follows that C p C Cpq q=2. Putting those three cases together we have C A0q C Cq0 0=2, and thus C A0q C C00 Cq0 0=2. C A1q C C10 C Cq0 0.... Note that $\forall$x A1x=x. Thus, C A1q C C10 C Cq0 0=C 1 C C10 C Cq0 0. C 1 C C10 C Cq0 0 is an instance of C p C q C Cpr r, which is a theorem of the implicational calculus here. Thus, C A1q C C10 C Cq0 0=2. C A2q C C20 C Cq0 0=C 2 C C20 C Cq0 0=C C20 C Cq0 0=C 0 C Cq0 0... another instance of CpCqp. Thus, C A2q C C20 C Cq0 0. Putting C A2q C C20 C Cq0 0, C A1q C C10 C Cq0 0=2, and C A0q C C00 C Cq0 0 together we obtain C Apq C Cp0 C Cq0 0. C Apq C Cp1 C Cq1 1=C Apq C Np C Nq 1=C Apq C Np NNq... C A0q C N0 NNq=C A0q C 1 NNq=C A0q 2=2. C A1q C N1 NNq=C A1q C 2 NNq=C A1q NNq... C A10 NN0=C 0 NN0=C0 N1=C02=2. C A11 NN1=C 1 NN1=C 1 N2=C11=2. C A12 NN2=C 2 NN2=NN2=N1=2. Thus, C Apq C Np NNq=2, and so C Apq C Cp1 C Cq1 1=2 also. C Apq C Cp2 C Cq2 2=C Apq C Cp2 2=C Apq 2=2. Now since we have C Apq C Cp0 C Cq0 0=2, C Apq C Cp1 C Cq1 1=2, and C Apq C Cp2 C Cq2 2, we can infer that C Apq C Cpr C Cqr r=2.

9. C C0q C C0Nq N0=C C0q C C0Nq 1... C C00 C C0N0 1=C C00 C C01 1=C C00 C11=C22=2. C C01 C C0N1 1=C 1 C C0N1 1=2. C C02 C C0N2 1=C 2 C C01 1=C 2 C11=C22=2. Thus, C C0q C C0Nq N0. C C1q C C1Nq N1=C C1q C C1Nq 2= C C1q 2=2. C C2q C C2Nq N2=C C2q C C2Nq 1... C C20 C C2N0 1=C C20 C C21 1= C C20 C11=C C20 2=2. C C21 C C2N1 1=C 1 C C2N1 1=2. C C22 C C2N2 1=C 2 C C21 1=2. Thus, C C2q C C2Nq N2. Therefore, C Cpq C CpNq Np=2.

10. C 0 C N0 q=C 0 C1q=C02=2. C 1 C N1 q=2. C 2 C N2 q=C 2 C1q=C22=2. Therefore, CpCNpq=2.

And that confirms that the above model does indicate that all the axioms, and the rule of inference {Cx y, x} $\vdash$ y do hold for this model, but CNNpp does not hold. Therefore, CNNpp is not a theorem of intuitionistic logic.

Answer 2

I will use the verb "forces" to refer to $\models$, and I will say $v $ "extends" $w$ if $v \geq w$.

It is not the case that $w_1 \models \alpha$. The only way for a world to satisfy a propositional variable is for the variable to be true in that world, and they have set it up so that neither $\alpha$ nor $\lnot \alpha$ is true in $w_1$.

At the same time, we do have that $w_1 \models \lnot \lnot \alpha$. This is because there exists an extension of $w_1$ (namely, $w_2$) that does not force $\lnot \alpha$. We have that $w_2 \not \models \lnot \alpha$ because there is an extension of $w_2$ (namely, $w_2$ itself) that does force $\alpha$. Note that, in general, a node $x$ forces $\lnot \phi$ if and only if no extension of $x$ (including $x$ itself) forces $\phi$.

Therefore, combining the previous paragraphs, $w_1 \not \models \lnot\lnot \alpha \to \alpha$.

One difficulty for many people the first time they run into the definition of the forcing relation $\models$ is in how it deals with negation:

• $w$ forces $\lnot \phi$ if and only if no extension of $w$ forces $\phi$.

• $w$ does not force $\lnot \psi$ if and only if some extension forces $\psi$

• $w$ forces $\lnot \lnot \theta$ if and only if no extension $v$ forces $\lnot \theta$, if and only if, for every extension $v$ of $w$ there is an extension $v'$ of $v$ that forces $\theta$. We usually abbreviate this as: $w$ forces $\lnot \lnot \theta$ if and only if the set of worlds that force $\theta$ is dense above $w$.

It is also worth knowing that the forcing relation is often written $\Vdash$ instead of $\models$.

Answer 3

Showing that Peirce's law fails isn't too hard here (and you don't have to reference the law of the excluded middle).

Suppose that Peirce's law held in intuitionistic logic. In Polish notation this is CCCpqpp. Note that C Cpq C Cqr Cpr, and CpCNpq are both provable in intuionistic logic (don't believe me... prove them for yourself!), and that {CCpqCCqrCpr, CpCNpq, CCNppp} is an axiom set for classical logic under detachment and uniform substitution. Now in CCCpqpp substitute q with "0", which I'm using here to mean "falsum". We then have CCCp0ppp. Since Np is defined as Cp0, we have that from any unary truth function of Cp0 we can infer any unary truth function of Np. Thus replacing Cp0 in CCCp0pp with Np we obtain CCNppp. So, if Peirce's law held in intuitionistic proposition logic, then intuitionistic propositional logic would end up as having the same theorems as classical propositional logic. But, those theorems are different, and thus Peirce's law fails in intuitionstic propositional logic.