Assignment 1

Proof Theory - 2nd semester, 2017-2018

Teodor Calinoiu
MoL, ILLC, UvA
February 16, 2018

Exercise 1(a). Let M  pW, R, f q be an intuitionistic Kripke model. Let tp1 , ..., pk u be a set of proposi-
tional variables. Let w P W be a state such that it satisfies the following condition:

(P re) If wRw1 , then f pwq X tp1 , ..., pk u  f pw1 q X tp1 , ..., pk u.

Let φ be a formula containing only propositional variables in tp1 , ..., pk u.

Prove that M, w , φ iff Mw ( φ (where Mw is a classical model defined by f pwq).

I will first prove two lemmas that will be instrumental in proving the main result.
I find it useful to make the following definitions.

Definition w PM satisfies pP req with respect to S  tp1 , ..., pk u „ P iff if wRw1 , then f pwq XS 
f pw1 q X S.

Definition Atpφq =df. {p PP : p appears in φu, where P is the class of all propositional variables in the
language.

Definition w PM satisfies pP req with respect to a formula φ iff w PM satisfies (P re) with respect
to Atpφq.

Let M  pW, R, f q be an arbitrary intuitionistic model, w P W an arbitrary state, S an arbitrary set of

propositional variables and φ an arbitrary formula of the propositional language to the extent Atpφq „ S.

Lemma (P req
preservation. If w satisfies (P re) with respect to S and wRw1 , then w1 satisfies (P re)
with respect to S.

Proof. [(P req
preservation] Suppose w satisfies pP req with respect to S. Let w1 P W be such that wRw1 .
Then f pwq X S  f pw1 q X S. Given that R is transitive, then for all w2 P W , if w1 Rw2 , then wRw2 . It
follows that if w1 Rw2 , then f pw1 q X S  f pw2 q X S. Hence w1 satisfies (P re) with respect to S.

Lemma pP re q. If w satisfies (P re) with respect to φ and wRw1 , then Mw ( φ iff Mw1 ( φ.
Proof. [pP re q] Let M be an arbitrary intuitionistic Kripke model. Let w P M be an arbitrary state such
that it satisfies pP req with respect to tp1 , ..., pk u containing all the propositional variables in some arbitrary
formula φ. Let w1 P W be arbitrary to the extent that wRw1 . I prove by induction on the complexity of
sentences that Mw ( φ iff Mw1 ( φ.
[Base case] Suppose φ  p P tp1 , ..., pk u. Suppose Mw ( p. Then p P f pwq. Then, b pP req and wRw1 ,
p P f pw1 q. Therefore, by the definition of satisfaction (i.e. (), Mw1 ( p.
[Induction case] Let ψ and χ be formulas containing only propositional variables in tp1 , ..., pk u. Suppose
both ψ and χ have the induction property, i.e. Mw ( ψ iff Mw1 ( ψ and Mw ( χ iff Mw1 ( χ - this is the
induction hypothesis (IH).

1
 [^] Let φ  ψ ^ χ. / Suppose Mw ( ψ ^ χ. Then Mw ( ψ and Mw ( χ. By IH, then Mw1 ( ψ and
Mw1 ( χ. Therefore, by the definition of satisfaction, Mw1 ( ψ ^ χ.
Suppose Mw1 ( ψ ^ χ. Then Mw1 ( ψ and Mw1 ( χ. By IH, then Mw ( ψ and Mw ( χ. Therefore, by
the definition of satisfaction, Mw ( ψ ^ χ.
[_] Let φ  ψ _ χ.
Suppose Mw ( ψ _ χ. Then Mw ( ψ or Mw ( χ. Then, by IH, Mw1 ( ψ or Mw1 ( χ. Therefore, by the
definition of satisfaction, Mw1 ( ψ _ χ.
Suppose Mw1 ( ψ _ χ. Then Mw1 ( ψ or Mw1 ( χ. Then, by IH, Mw ( ψ or Mw ( χ. Therefore, by the
definition of satisfaction, Mw ( ψ _ χ.
[Ñ] Let φ  ψ Ñ χ.
Suppose Mw ( ψ Ñ χ. Then Mw * ψ or Mw ( χ. Suppose Mw * ψ. Then, by IH, Mw1 * ψ. Then
Mw ( ψ Ñ χ. Suppose the later: Mw ( χ. Then, by IH, Mw1 ( χ. Then Mw1 ( ψ Ñ χ. Either way,
1
Mw1 ( ψ Ñ χ.
Suppose Mw1 ( ψ Ñ χ. Then Mw1 * ψ or Mw1 ( χ. Suppose Mw1 * ψ. Then, by IH, Mw * ψ. Then
Mw ( ψ Ñ χ. Suppose the later: Mw ( χ. Then, by IH, Mw ( χ. Then Mw ( ψ Ñ χ. Either way,
Mw ( ψ Ñ χ.
Hence, by induction on the complexity of sentences it follows that for all w, w1 P W such that w satisfies
pP req (with respect to some set of propositional variables such that φ only contains propositional variables
from it) and wRw1 , Mw ( φ iff Mw1 ( φ.
Given that M, w, S and φ are arbitrary, (P re)-preservation and (P re ) generalize: both lemmas hold
for all intuitionistic models M , states w P M , sets of propositional variables S and formulas φ such that
Atpφq „ S.

Proof. [1(a)] Let M  pW, R, f q be an arbitrary intuitionistic Kripke model, S an arbitrary set of proposi-
tional variables and φ an.
I will prove by induction on the complexity of sentences that for any w P W such that it satisfies pP req
w.r.t. S, if φ is a formula such that Atpφq „ S, then M, w , φ iff Mw ( φ1 .
[Base case] Suppose φ  p P S and w P W is an arbitrary state to the extent that it satisfies (P re) with
respect to S.
Suppose M, w , p. Then p P f pwq. Then Mw ( p.
Suppose Mw ( p. Then p P f pwq. Then M, w , p.
[Induction case] Let ψ and χ be formulas such that they only contain propositional variables from S.
Suppose that both ψ and χ have the induction property, i.e. for all w P W satisfying pP req with respect
S, if M, w , ψ, then Mw ( ψ and if Mw ( ψ, then M, w , ψ (and similarly for χ) - this is the induction
hypothesis (IH).
[^] Suppose φ  ψ ^ χ and w P W is an arbitrary state to the extent that it satisfies (P re) with respect
to S.
Suppose M, w , ψ ^ χ. Then M, w , ψ and M, w , χ. Then, by IH, Mw ( ψ and Mw ( χ. Therefore,
Mw ( ψ ^ χ.
Suppose Mw ( ψ ^ χ. Then Mw ( ψ and Mw ( χ. Then, by IH, M, w , ψ and M, w , χ. Therefore,
M, w , ψ ^ χ.
[_] Let φ  ψ _ χ and w P W is an arbitrary state to the extent that it satisfies (P re) with respect to S.
Suppose M, w , ψ _ χ. Then M, w , ψ or M, w , χ. Then, by IH, Mw ( ψ or Mw ( χ. Therefore,
Mw ( ψ _ χ.
Suppose Mw ( ψ _ χ. Then Mw ( ψ or Mw ( χ. Then, by IH, M, w , ψ or M, w , χ. Therefore,
M, w , ψ _ χ.
[Ñ] Let φ  ψ Ñ χ and w P W is an arbitrary state to the extent that it satisfies (P re) with respect to
S.
Suppose M, w , ψ Ñ χ. That is, for all w1 P W such that wRw1 , if M, w1 , ψ, then M, w1 , χ. Given
that R is reflexive, then if M, w , ψ, then M, w , χ. That is iff M, w . ψ or M, w , χ. Suppose the
former: M, w . ψ. Then, by the contrapositive of the right conjunct of IH (i.e. if M, w . ψ, then Mw * ψ),
,
1 I.e. if M, w φ, then Mw ( φ and if Mw ( φ, then M, w , φ. Notice that this is a slightly different result than the one
asked for in the statement of the exercise; anyway, the result asked for is an instance of the result proved here.

2
Mw * ψ. Therefore, Mw ( ψ Ñ χ. Suppose the later: M, w , χ. Then, by IH, Mw ( χ. Therefore,
Mw ( ψ Ñ χ.
Either way, Mw ( ψ Ñ χ.
Suppose that Mw ( ψ Ñ χ. That is iff Mw * ψ or Mw ( χ. Suppose the former: Mw * ψ. Then,
by (P re ), for all w1 P W such that wRw1 , Mw1 * ψ. By pP req
preservation, for all w1 P W such that
wRw1 , w1 satisfies (P re) with respect to S. Therefore IH applies and, then, for all w1 P W such that wRw1 ,
M, w1 . ψ. Therefore, for all w1 P W such that wRw1 , if M, w , ψ, then M, w , χ. Hence, by the definition
of forcing, M, w , ψ Ñ χ. Suppose the later: Mw ( χ. By pP req
preservation, for all w1 P W such that
wRw1 , w1 satisfies (P re) with respect to S. Then, by (P re ), for all w1 P W such that wRw1 , Mw ( χ. 1

Then, by IH (which applies for the same reasons noticed before), for all w1 P W such that wRw1 , M, w1 , χ.
Therefore, for all w1 P W such that wRw1 , if M, w , ψ, then M, w , χ. Hence, by the definition of forcing,
M, w , ψ Ñ χ.
Either way, M, w , ψ Ñ χ.
Hence, by induction on the complexity of sentences, it follows that for all w P W such that w satisfies
pP req w.r.t. S, if φ is a formula such that Atpφq „ S, then M, w , φ iff Mw ( φ. Given that M and S were
arbitrary, this result generalizes to all intuitionistic models all sets of propositional variables.

Exercise 1(b). Prove that (C φ iff (I φ using the result from 1paq.

[ñ] : Prove: If (C φ, then (I φ.

Consider the following propositions:

Proposition [2]. If for all w1 P W such that wRw1 , exists w2 P W such that M, w2 , φ, then M, w , φ.
Proposition [3]. For all w1 P W such that wRw1 , there is w2 P W such that w1 Rw2 and for all w3 P W
such that w2 Rw3 , f pw2 q X Atpφq  f pw3 q X Atpφq.

Proposition [4]. For all R
paths P  xw, w1 , ..., wi , ...y starting in w, for all states w1 on P , there is w2
on P such that w1 Rw2 and w2 satisfies pP req with respect to φ.

I first prove Prop. 4. Then I go on to prove the following lemmas. I divide the proof for [ñ] in the proofs
of the following lemmas:

Lemma [43]. Prop. 4 entails Prop. 3.

Lemma [32-a]. if (C φ, then Prop. 3 entails the antecedent of Prop. 2.

Next I prove Prop. 2. I will finish the proof for the left-to-right direction of 1(b) by showing how the
above lead to the desired result.

Suppose (C φ. Let φ be an arbitrary formula.

Proof. Prop. [4]: Let M be an arbitrary intuitionistic Kripke model and w P W be an arbitrary state.
Let a R-path starting in w be a linearly ordered sequence P  xw, w1 , ..., wi , ...y of states from W such
that any two neighboring states wi , wi 1 are such that wi Rwi 1 and wi  wi 1 . Notice that, given that R
is reflexive, there is no empty path (a path of length 0). Every R
path is either empty, finite or infinite.
If P is empty, then Prop. [4] trivially holds.
Let P  xw, w1 , ..., wn y be a arbitrary finite R
path (for some finite n) starting in w such that Rpwn q 
twn u.
Given that R is transitive, for all wi on P , wi Rwn .
Consider wn . Given that Rpwn q  twn u, then, trivially, for all w1 P W such that Rwn w1 , f pwn q  f pw1 q.
A fortiori, for all w1 P W such that Rwn w1 , f pwn q X Atpφq  f pw1 q X Atpφq. Therefore, wn satisfies pP req
with respect to φ. Moreover, given that R is transitive (and reflexive), for all wi on P , wi Rwn .
Suppose alternatively that P is infinite2 : xw, w1 , ...wi , ...y.
2 Notice that theproof I provide for the infinite case also works for the finite case. Anyway, I consider the proof I gave for

the finite case to be superior with respect to the fact that I can define the state I take, namely wn , which I’m not able to do in
the case of the proof for the infinite case; the proof for the infinite case only tells us that there is such a state.

3
 Notice that any formula is a finite string of symbols; therefore Atpφq is finite. Then for every p P Atpφq,
either there is some wi on P at finite distance i from w at which p is first satisfied (i.e. the closest(/first
from w) wi such that M, wi , p3 ), or there is no wi on P such that M, wi , p. Therefore, there is a finite i
such that for all for all w1 such that wi Rw1 , f pwi q X Atpφq  f pw1 q X Atpφq; that is, there is a last (/furthest
away from w) state where a p P Atpφq which was not forced at is forced at wi
1 is now forced, and this state
is at a finite distance from w.
Consider the wi on P . By Persistence, for all j ¡ i, f pwi q X Atpφq  f pwj q X Atpφq. Therefore, for all
j ¥ i, wj satisfies pP req with respect to φ. Moreover, given that R is transitive, for all states w1 on P , there
is a state w2 , such that w1 Rw2 and w2 satisfies pP req with respect to φ.
Proof. Lemma [43]: Let M be an arbitrary intuitionistic Kripke model and w P W be an arbitrary state.
By Prop. 4, all the states on all the R-paths starting in w accesses a state which satisfies (P re) with
respect to φ. Moreover, we have that the reunion of all the states appearing on all the paths stating in w is
the set Rpwq  tw1 : wRw1 u. Hence, For all w1 P W such that wRw1 , there is w2 P W such that w1 Rw2 and
for all w3 P W such that w2 Rw3 , f pw2 q X Atpφq  f pw3 q X Atpφq; That is, all the states accessible from w
access a state which satisfies pP req with respect to φ. This conclusion generalizes to every M, w.
Proof. Lemma [32-a]: Let M be an arbitrary intuitionistic Kripke model and w P W be an arbitrary state.
Suppose that, (C φ.
By the supposition and the result in 1(a), it follows that for every state w1 P W satisfying pP req with
respect to φ, M, w , φ. Hence, by Prop. 3, for all w1 P W such that wRw1 , exists w2 P W such that
M, w2 , φ. This conclusion generalizes to every M, w.
Proof. Prop. 2: Let M be an arbitrary intuitionistic Kripke model and w P W be an arbitrary state.
Suppose for all w1 P W such that wRw1 , exists w2 P W such that M, w2 , φ. Therefore for all w1 P W
such that wRw1 , M, w1 . φ, that is, M, w1 . φ Ñ K. Therefore, M, w , pφ Ñ Kq Ñ K; that is
M, w , φ.
Proof. Main proof: 1(b) Let M be an arbitrary intuitionistic Kripke model and w P W be an arbitrary state.
Suppose that, (C φ.
Given Prop. 4, by Lemma [43], Prop. 3 holds and, thus, for all w1 P W such that wRw1 , exists w2 P W
such that M, w2 , φ. Hence, given Prop. 2, M, w , φ.
Given that M, w re arbitrary, this conclusion generalizes to all M, w. Hence (I φ.
[ð]: If (I φ, then (C φ.
I will first prove the following lemmas:

Lemma 1. If (C φ, then (C φ.
Proof. Lemma 1 Suppose (C φ. Therefore for all classical models M , M ( φ. Let M be an arbitrary
classical model: M ( φ. Therefore M * φ. Then M ( φ. Given that M is arbitrary, this conclusion
generalizes to all M and, hence, (C φ.

Lemma 2. Let I1  tM  pW, R, f q intuitionistic Kripke model: |W |  1u, where |X | is the cardinality of
the set X. Then if I1 (I φ (that is, for all M P I1 , M (I φ) then (C φ.

Proof. [Lemma 2] Define first the following. Let M „ P (P is the set of propositional variables of the
propositional language) be a classical model. Then M   pW, R, f q is an intuitionistic Kripke model such
that W  tMu, R  tpM, Mqu and f pMq  M. Clearly every M  P I1 .
Let ρ be an arbitrary formula. Suppose I1 (I ρ and assume .C ρ. By assumption it follows that there
is a classical model M such that M .C ρ. Consider then M  .
I prove by induction on the complexity of formulas that if M .C φ, then M  .I φ.
Let M be an arbitrary classical model such that M .C φ: this will be our supposition at every stage in
the induction.
[Base case] Let φ  p P p. Then p R f pMq; then M  , M *I p and, hence M  * p.
3 Notice that the sequence is linearly order and, therefore, there is one such wi

4
 [Induction case] Let ψ and χ be formulas such that they have the induction property - this is the induction
hypothesis (IH).
[^] Let φ  ψ ^ χ. Then M *C ψ or MnvDashC χ. (I will consider only one disjunct; the other goes in
a similar manner). Suppose M *C ψ. Then, by IH, M  *I ψ. Hence M  *I ψ ^ χ. Similarly for χ. Either
way, M  *I ψ ^ χ.
[_] Suppose φ  ψ _ χ. Then M *C ψ and MnvDashC χ. By IH, M  *I ψ and M  *I χ. Hence

M *I ψ _ χ.
[Ñ] Suppose φ  ψ Ñ χ. Then M (C ψ and MnvDashC χ. Notice that M P M  satisfies (P re) with
respect to ψ. Therefore, by the result in 1(a), M  , M , ψ. By IH, M  * χ; therefore, M  , M . χ. Therefore
M  , M . ψ Ñ χ. Hence M  *Ñ χ.
It follows by induction on the complexity of formulas that if M *C φ, then the corresponding M  *I φ,
for all φ formulas.
Therefore if *C ρ, then I1 *I ρ: contradiction with our supposition. Hence our assumption is false and,
thus, if I1 (I φ, then (C φ, for all propositional formulas φ.4 .
I turn now to proving rðs.
Proof. [ð] Suppose (I φ. That is, for all intuitionistic Kripke models M , M (I φ. In particular
then, for all M P I1 , M (I φ; that is, I1 (I φ. By Lemma 2, then (C φ. By Lemma 1, then
(c φ.

4 Clearly, this is not an intuitionistically valid piece of reasoning!