Contextual-Hierarchical Reconstructions of the Strengthened Liar Problem

Abstract

In this paper we shall introduce two types of contextual-hierarchical (from now on abbreviated by ‘ch’) approaches to the strengthened liar problem. These approaches, which we call the ‘standard’ and the ‘alternative’ ch-reconstructions of the strengthened liar problem, differ in their philosophical view regarding the nature of truth and the relation between the truth predicates T r ⁿ and T r ⁿ⁺¹ of different hierarchy-levels. The basic idea of the standard ch-reconstruction is that the T r ⁿ⁺¹-schema should hold for all sentences of $\mathcal {L}^{n}$. In contrast, the alternative ch-reconstruction, for which we shall argue in section four, is motivated by the idea that T r ⁿ and T r ⁿ⁺¹ are coherent in the sense that the same sentences of $\mathcal {L}^{n}$ should be true according to T r ⁿ and T r ⁿ⁺¹. We show that instances of the standard ch-reconstruction can be obtained by iterating Kripke’s strong Kleene jump operator. Furthermore, we will demonstrate how instances of the alternative ch-reconstruction can be obtained by a slight modification of the iterated axiom system KF and of the iterated strong Kleene jump operator.

Appendix :

Proof of lemma 3.2

By Lemma 3.1, $\mathcal {M}^{1}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$. Since $\mathcal {M}^{2}$ is an expansion of $\mathcal {M}^{1}$, we have $\mathcal {M}^{2}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$. In addition, we have $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \varphi \urcorner )\leftrightarrow \varphi$ for any sentence φ of $\mathcal {L}^{1}$, which follows from the definition of $E_{\mathcal {M}^{1}}^{lf}$. From this, together with $\mathcal {M}^{2}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$, we can derive $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \neg Tr^{1}(\ulcorner \lambda \urcorner )\urcorner )$ □

Proof of lemma 3.3

Let E be the extension of any fixed point (E,A) of $\kappa _{\mathcal {M}^{n}}$. Then:

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi \urcorner )$ iff

• c ⁿ⁺¹(φ)∈E iff

• $Val_{\mathcal {M}^{n}(E,A)}(\varphi )=t$ (since E={c ⁿ⁺¹(φ)∈D:c ⁿ⁺¹(φ)∈L ⁿ⁺¹ and $Val_{\mathcal {M}^{n}(E,A)}(\varphi )=t\}$) iff

• $Val_{\mathcal {M}^{n}(E,A)}(\psi )=t$ (since φ and ψ are $\mathcal {M}^{n}$-logically equivalent) iff

• c ⁿ⁺¹(ψ)∈E iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi \urcorner )$

□

Proof of lemma 3.4

By lemma 3.1, $\mathcal {M}^{1}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$. By Lemma 3.2 and substitution of $\mathcal {M}^{0}$-logical equivalents in T r ², which follows from Lemma 3.3, we have $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \lambda ^{1}\urcorner )$. We obtain the first claim of Lemma 3.4 analogously.

In the proof of lemma 3.2 we have already demonstrated that $\mathcal {M}^{2}\vDash Tr^{2}\left (\ulcorner \varphi \urcorner \right )\leftrightarrow \varphi$ for all sentences φ of $\mathcal {L}^{1}$. By the same argument schema, we obtain $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner \varphi \urcorner )\leftrightarrow \varphi$ for all sentences φ of $\mathcal {L}^{n}$ and for n=0 and m=1, and for each n,m with 1<n<m □

Proof of lemma 4.1

From Section 3 we have $\mathcal {M}^{1}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$. Since $\mathcal {M}^{2}$ is a {T r ²}-expansion of $\mathcal {M}^{2}$, $\mathcal {M}^{2}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$. From $\mathcal {M}^{2}\vDash \text {KF}^{\prime }_{2}$ it follows that $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \varphi \urcorner )\leftrightarrow Tr^{1}(\ulcorner \varphi \urcorner )$ for all φ of $\mathcal {L}^{1}$ (see axiom 1 of $\text {KF}^{\prime }_{2}$). Thus we obtain $\mathcal {M}^{2}\vDash \neg Tr^{2}(\ulcorner \lambda ^{1}\urcorner )$.

By $\mathcal {M}^{2}\vDash \text {KF}^{\prime }_{2}$, $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \neg Tr^{2}(\ulcorner \varphi \urcorner )\urcorner )\leftrightarrow \neg Tr^{1}(\ulcorner \varphi \urcorner )$ for all φ of $\mathcal {L}^{1}$ (see axiom 3a of $\text {KF}^{\prime }_{2}$). Because of $\mathcal {M}^{2}\vDash \neg Tr^{1}(\ulcorner \lambda ^{1}\urcorner )$, we obtain $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \neg Tr^{2}(\ulcorner \lambda ^{1}\urcorner )\urcorner )$ □

Proof of lemma 4.2

Claim 1 By Lemma 3.4, we have $\mathcal {M}^{1}\vDash Sent_{\mathcal {L}^{0}}(\ulcorner \varphi \urcorner )\rightarrow (Tr^{1}(\ulcorner \varphi \urcorner )\leftrightarrow \varphi )$, and therefore $\mathcal {M}^{n}\vDash Sent_{\mathcal {L}^{0}}(\ulcorner \varphi \urcorner )\rightarrow (Tr^{1}(\ulcorner \varphi \urcorner )\leftrightarrow \varphi )$. Because of $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$ for each n≥2, it follows that $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \varphi \urcorner )\leftrightarrow Tr^{1}(\ulcorner \varphi \urcorner )$ for each sentence φ of $\mathcal {L}^{1}$, and thus $\mathcal {M}^{n}\vDash Sent_{\mathcal {L}^{0}}(\ulcorner \varphi \urcorner )\rightarrow (Tr^{n}(\ulcorner \varphi \urcorner )\leftrightarrow \varphi )$.Claim 2 The claim is proved by induction over formulas. It is enough to prove the case where φ=¬ψ, as all other cases follow directly from the axioms of $\text {KF}^{\prime }_{2}$. If $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \neg \psi \urcorner )$, then $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \psi \urcorner )$, and thus, by the induction hypothesis, $\mathcal {M}^{2}\vDash Tr^{2}(\ulcorner \psi \urcorner )\leftrightarrow \psi$. Therefore $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \neg \psi \urcorner )\rightarrow (\neg Tr^{2}(\ulcorner \psi \urcorner )\leftrightarrow \neg \psi )$, and so it is enough to show that $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \neg \psi \urcorner )\rightarrow (Tr^{2}(\ulcorner \neg \psi \urcorner )\leftrightarrow \neg Tr^{2}(\ulcorner \psi \urcorner ))$. $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \neg \psi \urcorner )\rightarrow (\neg Tr^{2}(\ulcorner \psi \urcorner )\rightarrow Tr^{2}(\ulcorner \neg \psi \urcorner ))$ follows from the definition of W ²(x). $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \neg \psi \urcorner )\rightarrow (Tr^{2}(\ulcorner \neg \psi \urcorner )\rightarrow \neg Tr^{2}(\ulcorner \psi \urcorner ))$ follows from axiom 9 of $\text {KF}^{\prime }_{2}$. Thus, we have $\mathcal {M}^{2}\vDash W^{2}(\ulcorner \neg \psi \urcorner )\rightarrow (Tr^{2}(\ulcorner \neg \psi \urcorner )\leftrightarrow \neg \psi )$ □

Proof of lemma 4.3

By straightforward induction over formulas □

Proof of theorem 4.2 For each n≥0, the claim is proved by induction over formulas. If n=0, the claim follows from the first part of Theorem 4.3 on p. 93 in McGee [12]. Let n>0.

Direction 1

We show that $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$ implies $\kappa ^{\prime }_{\mathcal {M}^{n}}(E,A)=(E,A)$, where

(⋆):

A={c ⁿ⁺¹(φ):c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(¬φ)∈E} ∪

{c ⁿ⁺¹(φ):c ⁿ⁺¹(φ)∈L ⁿ and c ⁿ⁺¹(φ)∉E} ∪

{d∈D:d∉L ⁿ⁺¹}.

Recall that $\kappa ^{\prime }_{\mathcal {M}^{n}}(E,A):=(E^{\prime },A^{\prime })$ such that

$$\begin{array}{@{}rcl@{}}E^{\prime}=&&\{ c^{n+1}(\varphi)\in D: c^{n+1}(\varphi)\in L^{n+1}\backslash L^{n} \,\,\text{and}\,\, Val_{\mathcal{M}^{n}(E,A)}(\varphi)=t\}\\ &&\cup\\ &&\{ c^{n+1}(\varphi)\in D: c^{n+1}(\varphi)\in L^{n} \,\,\text{and}\,\, Val_{\mathcal{M}^{n}}(Tr^{n}(\ulcorner\varphi\urcorner))=t\}, \end{array} $$

and

$$\begin{array}{@{}rcl@{}} A^{\prime}=&&\{c^{n+1}(\varphi)\in D: c^{n+1}(\varphi)\in L^{n+1}\backslash L^{n} \,\,\text{and}\,\, Val_{\mathcal{M}^{n}(E,A)}(\varphi)=f\}\\ &&\cup \end{array} $$

$$\begin{array}{@{}rcl@{}} &&\{ c^{n+1}(\varphi)\in D: c^{n+1}(\varphi)\in L^{n} \,\,\text{and}\,\, Val_{\mathcal{M}^{n}}(Tr^{n}(\ulcorner\varphi\urcorner))\neq t\}\\ &&\cup\\ &&\{d\in D: d\notin L^{n+1}\}. \end{array} $$

We will now prove the following three propositions. For all sentences $\varphi \in \mathcal {L}^{n+1}$:

• 1. If c ⁿ⁺¹(φ)∈L ⁿ, then $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi \urcorner ))= t$ iff c ⁿ⁺¹(φ)∈E.

• 2. If c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ, then $Val_{\mathcal {M}^{n}(E,A)}(\varphi )=t$ iff c ⁿ⁺¹(φ)∈E.

• 3. If c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ, then $Val_{\mathcal {M}^{n}(E,A)}(\varphi )=f$ iff $c^{n+1}(\neg \varphi \urcorner )\in E$.

Note that if d is no metalanguage code of a sentence, then d∈A ^′ and d∈A. It can easily be checked that 1. and 3. imply A=A ^′, and 2. and 3. imply E=E ^′. Therefore by 1., 2. and 3, we obtain $\kappa ^{\prime }_{\mathcal {M}^{n}}(E,A)=(E,A)$.

We start with 1.

• ad 1. Let $\varphi \in \mathcal {L}^{n}$. Then $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi \urcorner ))=t$ iff $Val_{\mathcal {M}^{n}(E)}(Tr^{n}(\ulcorner \varphi \urcorner ))=t$. Furthermore, by $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, we obtain $Val_{\mathcal {M}^{n}(E)}(Tr^{n}(\ulcorner \varphi \urcorner ))=t$ iff $Val_{\mathcal {M}^{n}(E)}(Tr^{n+1}(\ulcorner \varphi \urcorner ))=t$. Finally, $Val_{\mathcal {M}^{n}(E)}(Tr^{n+1}(\ulcorner \varphi \urcorner ))=t$ iff c ⁿ⁺¹(φ)∈E, and thus $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi \urcorner ))=t$ iff c ⁿ⁺¹(φ)∈E.

We show 2. and 3. by simultaneous induction over formulas.

Case 1

Let φ be an atomic formula in $\mathcal {L}^{n+1}\backslash \mathcal {L}^{n}$, i.e. $\varphi =Tr^{n+1}(\ulcorner \psi \urcorner )$ for some ψ. Then

• ad 2. $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \psi \urcorner ))=t$ iff $\mathcal {M}^{n}(E,A)\vDash Tr^{n+1}(\ulcorner \psi \urcorner )$, and $\mathcal {M}^{n}(E,A)\vDash Tr^{n+1}(\ulcorner \psi \urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi \urcorner )$. Since $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi \urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner Tr^{n+1}(\ulcorner \psi \urcorner )\urcorner )$. Furthermore, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner Tr^{n+1}(\ulcorner \psi \urcorner )\urcorner )$ iff $c^{n+1}(Tr^{n+1}(\ulcorner \psi \urcorner ))\in E$. Therefore, $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \psi \urcorner ))=t$ iff $c^{n+1}(Tr^{n+1}(\ulcorner \psi \urcorner ))\in E$.

• ad 3. $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \psi \urcorner ))=f$ iff c ⁿ⁺¹(ψ)∈A, and c ⁿ⁺¹(ψ)∈A. By (⋆), either c ⁿ⁺¹(ψ)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(¬ψ)∈E, or c ⁿ⁺¹(ψ)∈L ⁿ and c ⁿ⁺¹(ψ)∉E.

  If c ⁿ⁺¹(ψ)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(¬ψ)∈E, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\neg \psi )$. By $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, we obtain $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\neg \psi )\leftrightarrow \linebreak Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\ulcorner \psi \urcorner )\urcorner )$. Moreover, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\ulcorner \psi \urcorner )\urcorner )$ iff $c^{n+1}(\neg Tr^{n+1}(\ulcorner \psi \urcorner ))\in E$. Thus, if c ⁿ⁺¹(ψ)∈L ⁿ⁺¹∖L ⁿ, we obtain $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \psi \urcorner ))=f$ iff $c^{n+1}(\neg Tr^{n+1}(\ulcorner \psi \urcorner ))\in E$.

  If c ⁿ⁺¹(ψ)∈L ⁿ and c ⁿ⁺¹(ψ)∉E, then $\mathcal {M}^{n}(E)\vDash \neg Tr^{n+1}(\ulcorner \psi \urcorner )$. Since $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$ and c ⁿ⁺¹(ψ)∈L ⁿ, $\mathcal {M}^{n}(E)\vDash \neg Tr^{n+1}(\ulcorner \psi \urcorner )$ iff $\mathcal {M}^{n}(E)\vDash \neg Tr^{n}(\ulcorner \psi \urcorner )$. Furthermore, by $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, $\mathcal {M}^{n}(E)\vDash \neg Tr^{n}(\ulcorner \psi \urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\ulcorner \psi \urcorner )\urcorner )$, and therefore, we obtain $c^{n+1}(\neg Tr^{n+1}(\ulcorner \psi \urcorner ))\in E$. Thus, if c ⁿ⁺¹(ψ)∈L ⁿ, we obtain $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \psi \urcorner ))=f$ iff $c^{n+1}(\neg Tr^{n+1}(\ulcorner \psi \urcorner ))\in E$.

Case 2

The case where φ is a negated atomic formula in $\mathcal {L}^{n+1}\backslash \mathcal {L}^{n}$, i.e. $\varphi =\neg Tr^{n+1}(\ulcorner \psi \urcorner )$, is proved analogously to Case 1 (using the strong Kleene scheme for ‘ ¬’).

Case 3

Let φ=ψ ₁∨ψ ₂ for some formulas ψ ₁ and ψ ₂ of $\mathcal {L}^{n+1}$, and let our induction hypothesis be that ψ ₁ and ψ ₂ meet Propositions 2 and 3. Then

• ad 2. By the strong Kleene scheme for ‘ ∨’, $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1}\vee \psi _{2})=t$ iff $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1})=t$ or $Val_{\mathcal {M}^{n}(E,A)}(\psi _{2})=t$. By the induction hypothesis, $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1})=t$ or $Val_{\mathcal {M}^{n}(E,A)}(\psi _{2})=t$ iff c ⁿ⁺¹(ψ ₁)∈E or c ⁿ⁺¹(ψ ₂)∈E. Furthermore, c ⁿ⁺¹(ψ ₁)∈E or c ⁿ⁺¹(ψ ₂)∈E iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{1}\urcorner )$ or $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{2}\urcorner )$. In addition, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{1}\urcorner )$ or $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{2}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{1}\urcorner )\vee Tr^{n+1}(\ulcorner \psi _{2}\urcorner )$. By $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, it follows that $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{1}\urcorner )\vee Tr^{n+1}(\ulcorner \psi _{2}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{1}\vee \psi _{2}\urcorner )$. Moreover, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \psi _{1}\vee \psi _{2}\urcorner )$ iff c ⁿ⁺¹(ψ ₁∨ψ ₂)∈E, from which we obtain $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1}\vee \psi _{2})=t$ iff c ⁿ⁺¹(ψ ₁∨ψ ₂)∈E.

• ad 3. By the strong Kleene scheme for ‘ ∨’, $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1}\vee \psi _{2})=f$ iff $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1})=f$ and $Val_{\mathcal {M}^{n}(E,A)}(\psi _{2})=f$. By the induction hypothesis, we obtain $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1})=f$ and $Val_{\mathcal {M}^{n}(E,A)}(\psi _{2})=f$ iff c ⁿ⁺¹(¬ψ ₁)∈E and c ⁿ⁺¹(¬ψ ₂)∈E. Moreover, we have c ⁿ⁺¹(¬ψ ₁)∈E and c ⁿ⁺¹(¬ψ ₂)∈E iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \psi _{1}\urcorner )$ and $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \psi _{2}\urcorner )$. Furthermore, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \psi _{1}\urcorner )$ and $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \psi _{2}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \psi _{1}\urcorner )\wedge Tr^{n+1}(\ulcorner \neg \psi _{2}\urcorner )$. Since $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, we have $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \psi _{1}\urcorner ) \wedge Tr^{n+1}(\ulcorner \neg \psi _{2}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg (\psi _{1}\vee \psi _{2})\urcorner )$. Finally, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg (\psi _{1}\vee \psi _{2})\urcorner )$ iff c ⁿ⁺¹(¬(ψ ₁∨ψ ₂))∈E, from which we obtain $Val_{\mathcal {M}^{n}(E,A)}(\psi _{1}\vee \psi _{2})=f$ iff c ⁿ⁺¹(¬(ψ ₁∨ψ ₂))∈E.

Case 4

The case where φ=¬(ψ ₁∨ψ ₂) for some formulas ψ ₁ and ψ ₂ in $\mathcal {L}^{n+1}$, is proved analogously to Case 3.

Case 5

Let φ=∀x ψ where ψ is a formula of $\mathcal {L}^{n+1}$. For simplicity, let us assume that for each object d, there is a closed term $\bar {d}$ which denotes d, i.e. $I(\bar {d})=d$. Thus, we will assume a substitutional interpretation of universal quantifiers: $\mathcal {M}^{n}(E)\vDash \forall x\varphi$ iff $\mathcal {M}^{n}(E)\vDash [\varphi ]_{x}^{\bar {d}}$ for each d∈D. To make the formulas more legible we shall abbreviate ‘$sub(\ulcorner \varphi \urcorner ,x,y)$’ by ‘${\ulcorner [\varphi ]_{x}^{y}}\urcorner$’, for each sentence φ and for each variables x and y. Let our induction hypothesis be that for each d∈D, $[\psi ]_{x}^{\bar {d}}$ meets Propositions 2. and 3. Then

• ad 2. $Val_{\mathcal {M}^{n}(E,A)}(\forall x\psi )=t$ iff for all d∈D, $Val_{\mathcal {M}^{n}(E,A)}([\psi ]_{x}^{\bar {d}})=t$. By the induction hypothesis, for all d∈D, $Val_{\mathcal {M}^{n}(E,A)}([\psi ]_{x}^{\bar {d}})=t$ iff for all $d\in D: c^{n+1}([\psi ]_{x}^{\bar {d}})\in E$. Furthermore, for all $d\in D: c^{n+1}([\psi ]_{x}^{\bar {d}})\in E$ iff for all $d\in D, \mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner [\psi ]_{x}^{\bar {d}}\urcorner )$, and for all $d\in D, \mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner [\psi ]_{x}^{\bar {d}}\urcorner )$ iff ($\mathcal {M}^{n}(E)\vDash \forall x Tr^{n+1}(\ulcorner \psi \urcorner )$ iff) $\mathcal {M}^{n}(E)\vDash \forall z Tr^{n+1}(\ulcorner [\psi ]_{x}^{num(z)}\urcorner )$. By $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, $\mathcal {M}^{n}(E)\vDash \forall z Tr^{n+1}(\ulcorner [\psi ]_{x}^{num(z)}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}\left (\ulcorner \forall x\psi \urcorner \right )$. Finally, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \forall x\psi \urcorner )$ iff c ⁿ⁺¹(∀x ψ)∈E.

• ad 3. $Val_{\mathcal {M}^{n}(E,A)}(\forall x\psi )=f$ iff there is a d∈D: $Val_{\mathcal {M}^{n}(E,A)}([\psi ]_{x}^{\bar {d}})=f$. By the induction hypothesis, there is a d∈D: $Val_{\mathcal {M}^{n}(E,A)}([\psi ]_{x}^{\bar {d}})=f$ iff there is a $d\in D: c^{n+1}([\neg \psi ]_{x}^{\bar {d}})\in E$. Furthermore, there is a $d\in D: c^{n+1}([\neg \psi ]_{x}^{\bar {d}})\in E$ iff there is a $d\in D, \mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner [\neg \psi ]_{x}^{\bar {d}}\urcorner )$. In addition, there is a $d\in D, \mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner [\neg \psi ]_{x}^{\bar {d}}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash \exists z Tr^{n+1}(\ulcorner [\neg \psi ]_{x}^{num(z)}\urcorner )$. By $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$, we obtain $\mathcal {M}^{n}(E)\vDash \exists z Tr^{n+1}(\ulcorner [\neg \psi ]_{x}^{num(z)}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \forall x\psi \urcorner )$. Finally, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \forall x\psi \urcorner )$ iff c ⁿ⁺¹(¬∀x ψ)∈E.

Case 6

The case where φ = ¬∀x ψ and ψ is a formula of $\mathcal {L}^{n+1}$ is proved analogously to Case 5.

Direction 2

We show that $\kappa ^{\prime }_{\mathcal {M}^{n}}(E,A)=(E,A)$ implies $\mathcal {M}^{n}(E)\vDash \text {KF}^{\prime }_{n+1}$ by showing the following ten items:

• 1. $\mathcal {M}^{n}(E)\vDash \forall x(Sent_{\mathcal {L}^{n}}(x)\rightarrow (Tr^{n+1}(x)\leftrightarrow Tr^{n}(x)))$;

• 2. $\mathcal {M}^{n}(E)\vDash \forall x(Sent_{\mathcal {L}^{n+1}}(x)\rightarrow (Tr^{n+1}(\ulcorner Tr^{n+1}(\dot {x})\urcorner )\leftrightarrow Tr^{n+1}(x)))$;

• 3a. $\mathcal {M}^{n}(E)\vDash \forall x(Sent_{\mathcal {L}^{n}}(x)\rightarrow (Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\dot {x})\urcorner )\leftrightarrow \neg Tr^{n}(x)))$;

• 3b. $\mathcal {M}^{n}(E)\vDash \forall x((Sent_{\mathcal {L}^{n+1}}(x)\wedge \neg Sent_{\mathcal {L}^{n}}(x))\rightarrow$

  $(Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\dot {x})\urcorner )\leftrightarrow Tr^{n+1}($ ¬̣ x)));

• 4. $\mathcal {M}^{n}(E)\vDash \forall x\forall y(Sent_{\mathcal {L}^{n+1}}(x$ ∨̣ y)→

  (T r ⁿ⁺¹(x ∨̣ y)⇔(T r ⁿ⁺¹(x)∨T r ⁿ⁺¹(y))));

• 5. $\mathcal {M}^{n}(E)\vDash \forall x\forall y\forall z(Sent_{\mathcal {L}^{n+1}}($ ¬̣ (x ∨̣ y))→

  (T r ⁿ⁺¹(¬̣ (x ∨̣ y))⇔(T r ⁿ⁺¹(¬̣ x)∧T r ⁿ⁺¹(¬̣ y))));

• 6. $\mathcal {M}^{n}(E)\vDash \forall x\forall y((Var_{\mathcal {L}^{n+1}}(x)\wedge Frm_{\mathcal {L}^{n+1}}(y))\rightarrow$

  (T r ⁿ⁺¹(∃̣ x y)⇔∃z T r ⁿ⁺¹(s u b(y,x,n u m(z)))));

• 7. $\mathcal {M}^{n}(E)\vDash \forall x\forall y((Var_{\mathcal {L}^{n+1}}(x)\wedge Frm_{\mathcal {L}^{n+1}}(y))\rightarrow$

  (T r ⁿ⁺¹(¬̣ ∃̣ x y)⇔∀z T r ⁿ⁺¹(¬̣ s u b(y,x,n u m(z)))));

• 8. $\mathcal {M}^{n}(E)\vDash \forall x\forall y((Sent_{\mathcal {L}^{n+1}}(x)\wedge \hspace {2pt} x\equiv \hspace {2pt}$ ¬̣ ¬̣ y)→

  (T r ⁿ⁺¹(x)⇔T r ⁿ⁺¹(y)));

• 9. $\mathcal {M}^{n}(E)\vDash \forall x (Sent_{\mathcal {L}^{n+1}}(x)\rightarrow \neg (Tr^{n+1}(x)\wedge Tr^{n+1}($ ¬̣ x))).

ad 1 and ad 2. Straightforward.

For any d∈D, assume $\mathcal {M}^{n}(E)\vDash Sent_{\mathcal {L}^{n}}(\bar {d})$. Then there is a φ such that c ⁿ⁺¹(φ)=d and c ⁿ⁺¹(φ)∈L ⁿ. By

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\neg Tr^{n+1}(\ulcorner \varphi \urcorner ))$ iff

• $c^{n+1}(\neg Tr^{n+1}(\ulcorner \varphi \urcorner ))\in E$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg Tr^{n+1}(\ulcorner \varphi \urcorner ))=t$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \varphi \urcorner ))=f$ iff

• c ⁿ⁺¹(φ)∈A iff (since c ⁿ⁺¹(φ)∈L ⁿ) iff

• $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi \urcorner ))\neq t$ iff

• $Val_{\mathcal {M}^{n}}(\neg Tr^{n}(\ulcorner \varphi \urcorner ))=t$ iff

• $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \varphi \urcorner )$ iff

• $\mathcal {M}^{n}(E)\vDash \neg Tr^{n}(\ulcorner \varphi \urcorner )$,

we obtain $\mathcal {M}^{n}(E)\vDash \forall x(Sent_{\mathcal {L}^{n}}(x)\rightarrow (Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\dot {x})\urcorner )\leftrightarrow \neg Tr^{n}(x)))$.

For any d∈D, assume $\mathcal {M}^{n}(E)\vDash Sent_{\mathcal {L}^{n+1}}(\bar {d})\wedge \neg Sent_{\mathcal {L}^{n}}(\bar {d})$. Then there is a φ such that c ⁿ⁺¹(φ)=d and c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ. By

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}($ ¬̣$\bar {d})$ iff

• c ⁿ⁺¹(¬φ)∈E iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi )=t$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\varphi )=f$ iff (since c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ)

• $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \varphi \urcorner ))=f$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg Tr^{n+1}(\ulcorner \varphi \urcorner ))=t$ iff

• $c^{n+1}(\neg Tr^{n+1}(\ulcorner \varphi \urcorner ))\in E$ iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\bar {d})\urcorner )$,

we obtain $\mathcal {M}^{n}(E)\vDash \forall x((Sent_{\mathcal {L}^{n+1}}(x)\wedge \neg Sent_{\mathcal {L}^{n}}(x))\rightarrow ((Tr^{n+1}($ ¬̣$x)\leftrightarrow Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\dot {x})\urcorner )))$.

Assume $\mathcal {M}^{n}(E)\vDash Sent_{\mathcal {L}^{n+1}}(\bar {d}_{1}$ ∨̣$\bar {d}_{2})$. Then there are two sentences of $\mathcal {L}^{n+1}$, such that c ⁿ⁺¹(φ ₁)=d ₁, c ⁿ⁺¹(φ ₂)=d ₂. $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner )$ iff c ⁿ⁺¹(φ ₁∨φ ₂)∈E. From c ⁿ⁺¹(φ ₁∨φ ₂)∈E, it follows either $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{1}\vee \varphi _{2})=t$ (in case φ ₁∨φ ₂ is no sentence of $\mathcal {L}^{n}$), or $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner ))=t$ (in case φ ₁∨φ ₂ is a sentence of $\mathcal {L}^{n}$). In the first case we have

• $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{1}\vee \varphi _{2})=t$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{1})=t$ or $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{2})=t$ iff

• c ⁿ⁺¹(φ ₁)∈E or c ⁿ⁺¹(φ ₂)∈E (and φ ₁ or φ ₂ is no sentence of $\mathcal {L}^{n}$)) iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\urcorner )$ or $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{2}\urcorner )$ iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\urcorner )\vee Tr^{n+1}(\ulcorner \varphi _{2}\urcorner )$.

In the second case φ ₁ and φ ₂ are both sentences of $\mathcal {L}^{n}$, and we have:

• $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner ))=t$ iff (since $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$)

• $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi _{1}\urcorner )\vee Tr^{n}(\ulcorner \varphi _{2}\urcorner ))=t$ iff

• $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi _{1}\urcorner ))=t$ or $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \varphi _{2}\urcorner ))=t$ iff (by the definition of E)

• c ⁿ⁺¹(φ ₁)∈E or c ⁿ⁺¹(φ ₂)∈E iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\urcorner )$ or $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{2}\urcorner )$ iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\urcorner )\vee Tr^{n+1}(\ulcorner \varphi _{2}\urcorner )$.

Therefore, we have shown that $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \varphi _{1}\urcorner )\vee Tr^{n+1}(\ulcorner \varphi _{2}\urcorner )$, i.e. $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\bar {d}_{1}$ ∨̣$\bar {d}_{2})$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\bar {d}_{1})\vee Tr^{n+1}(\bar {d}_{2})$.

Assume $\mathcal {M}^{n}(E)\vDash Sent_{\mathcal {L}^{n+1}}($ ¬̣$(\bar {d}_{1}$ ∨̣$\bar {d}_{2}))$.

Then there are two sentences φ ₁ and φ ₂ of $\mathcal {L}^{n+1}$, such that c ⁿ⁺¹(φ ₁)=d ₁, and c ⁿ⁺¹(φ ₂)=d ₂. Either c ⁿ⁺¹(φ ₁)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ⁺¹∖L ⁿ, or c ⁿ⁺¹(φ ₁)∈L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ, or (without loss of generality) c ⁿ⁺¹(φ ₁)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ.

In case that c ⁿ⁺¹(φ ₁)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ⁺¹∖L ⁿ:

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \varphi _{1}\urcorner )\wedge Tr^{n+1}(\ulcorner \neg \varphi _{2}\urcorner )$ iff

• c ⁿ⁺¹(¬φ ₁)∈E and c ⁿ⁺¹(¬φ ₂)∈E iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{1})=t$ and $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{2})=t$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{1}\wedge \neg \varphi _{2})=t$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg (\varphi _{1}\vee \varphi _{2}))=t$ iff

• c ⁿ⁺¹(¬(φ ₁∨φ ₂))∈E iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg (\varphi _{1}\vee \varphi _{2})\urcorner )$.

In case that c ⁿ⁺¹(φ ₁)∈L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ:

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \varphi _{1}\urcorner )\wedge Tr^{n+1}(\ulcorner \neg \varphi _{2}\urcorner )$ iff

• c ⁿ⁺¹(¬φ ₁)∈E and c ⁿ⁺¹(¬φ ₂)∈E iff

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg \varphi _{1}\urcorner )$ and $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg \varphi _{2}\urcorner )$ iff

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg \varphi _{1}\urcorner )\wedge Tr^{n}(\ulcorner \neg \varphi _{2}\urcorner )$ iff (since $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$)

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg (\varphi _{1}\vee \varphi _{2})\urcorner )$ iff (by the definition of E)

• c ⁿ⁺¹(¬(φ ₁∨φ ₂))∈E iff

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\neg (\varphi _{1}\vee \varphi _{2})\urcorner )$.

In case that c ⁿ⁺¹(φ ₁)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ:

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg (\varphi _{1}\vee \varphi _{2})\urcorner )$ iff (by axiom 3a, which was proved in ‘ad 3a’, and c ⁿ⁺¹(φ ₁)∈L ⁿ⁺¹∖L ⁿ)

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg Tr^{n+1}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner )\urcorner )$ iff

• $c^{n+1}(\neg Tr^{n+1}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner ))\in E$ iff

• $Val_{\mathcal {M}^{n}(E,A)}(\neg Tr^{n+1}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner ))=t$ iff (by strong Kleene logic)

• $Val_{\mathcal {M}^{n}(E,A)}(Tr^{n+1}(\ulcorner \varphi _{1}\vee \varphi _{2}\urcorner ))=f$ iff

• c ⁿ⁺¹(φ ₁∨φ ₂)∈A iff (by the definition of A)

• $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{1}\vee \varphi _{2})=f$ iff (by strong Kleene logic)

• $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{1})=f$ and $Val_{\mathcal {M}^{n}(E,A)}(\varphi _{2})=f$ iff (by strong Kleene logic)

• $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{1})=t$ and $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{2})=t$.

We continue this case as follows: concerning φ ₁, $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{1})=t$ iff c ⁿ⁺¹(¬φ ₁)∈E iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \varphi _{1}\urcorner )$. Concerning φ ₂, either c ⁿ⁺¹(φ ₂)∈L ⁰ or there is a k, 0<k≤n, such that c ⁿ⁺¹(φ ₂)∈L ^k∖L ^k−1. In case that c ⁿ⁺¹(φ ₂)∈L ⁰:

• $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{2})=t$ iff (by $\mathcal {M}^{1}\vDash \text {KF}^{\prime }_{1}$ and Theorem 4.1)

• $Val_{\mathcal {M}^{1}(E,A)}(\neg \varphi _{2})=t$ iff

• c ¹(¬φ ₂)∈I ¹(T r ¹) iff

• $\mathcal {M}^{1}\vDash Tr^{1}(\ulcorner \neg \varphi _{2}\urcorner )$ iff (since $\mathcal {M}^{2}\vDash \text {KF}^{\prime }_{2}$, $\mathcal {M}^{3}\vDash \text {KF}^{\prime }_{3}$, …, $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$, and by axiom 1, which was proved in ‘ad 1’)

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \varphi _{2}\urcorner )$.

In case that c ⁿ⁺¹(φ ₂)∈L ^k∖L ^k−1:

• $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi _{2})=t$ iff

• $Val_{\mathcal {M}^{k}(E,A)}(\neg \varphi _{2})=t$ iff

• $I^{k}(\ulcorner \neg \varphi _{2}\urcorner )\in I^{k}(Tr^{k})$ iff

• $\mathcal {M}^{k}\vDash Tr^{k}(\ulcorner \neg \varphi _{2}\urcorner )$ iff (since $\mathcal {M}^{k+1}\vDash \text {KF}^{\prime }_{k+1}$, $\mathcal {M}^{k+2}\vDash \text {KF}^{\prime }_{k+2}$, …, $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$, and by axiom 1, which was proved in ‘ad 1’)

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \varphi _{2}\urcorner )$.

Thus, in case that c ⁿ⁺¹(φ ₁)∈L ⁿ⁺¹∖L ⁿ and c ⁿ⁺¹(φ ₂)∈L ⁿ, $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg (\varphi _{1}\vee \varphi _{2})\urcorner )$ iff $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \neg \varphi _{1}\urcorner )\wedge Tr^{n+1}(\ulcorner \neg \varphi _{2}\urcorner )$. Therefore, $\mathcal {M}^{n}(E)\vDash Sent_{\mathcal {L}^{n+1}}($ ¬̣$(\bar {d}_{1}$ ∨̣$\bar {d}_{2}))\rightarrow (Tr^{n+1}($ ¬̣$(\bar {d}_{1}$ ∨̣$\bar {d}_{2}))\leftrightarrow (Tr^{n+1}($ ¬̣$\bar {d}_{1})\wedge Tr^{n+1}($ ¬̣$\bar {d}_{1})))$.

Assume $\mathcal {M}^{n}(E)\vDash Var_{\mathcal {L}^{n+1}}(\bar {d_{1}})\wedge Frm_{\mathcal {L}^{n+1}}(\bar {d_{2}})$, and let c ⁿ⁺¹(x)=d ₁ and c ⁿ⁺¹(φ)=d ₂.

Then either $\mathcal {M}^{n}(E)\vDash Frm_{\mathcal {L}^{n+1}}(\ulcorner \varphi \urcorner )\wedge \neg Frm_{\mathcal {L}^{n}}(\ulcorner \varphi \urcorner )$ or $\mathcal {M}^{n}(E)\vDash Frm_{\mathcal {L}^{n}}(\ulcorner \varphi \urcorner )$. In case that $\mathcal {M}^{n}(E)\vDash Frm_{\mathcal {L}^{n+1}}(\ulcorner \varphi \urcorner )\wedge \neg Frm_{\mathcal {L}^{n}}(\ulcorner \varphi \urcorner )$:

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \exists x\varphi \urcorner )$ iff

• c ⁿ⁺¹(∃x φ)∈E iff

• $Val_{\mathcal {M}^{n}(E,A)}(\exists x\varphi )=t$ iff

• there is a d∈D, such that $Val_{\mathcal {M}^{n}(E,A)}([\varphi ]_{x}^{\bar {d}})=t$ iff

• there is a d∈D, such that $c^{n+1}([\varphi ]_{x}^{\bar {d}})\in E$ iff

• there is a d∈D, such that $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner [\varphi ]_{x}^{\bar {d}}\urcorner )$ iff

• $\mathcal {M}^{n}(E)\vDash \exists z Tr^{n+1}(sub(\ulcorner \varphi \urcorner ,x,num(z)))$.

In case that $\mathcal {M}^{n}(E)\vDash Frm_{\mathcal {L}^{n}}(\ulcorner \varphi \urcorner )$:

• $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \exists x\varphi \urcorner )$ iff

• c ⁿ⁺¹(∃x φ)∈E iff (since c ⁿ⁺¹(∃x φ)∈L ⁿ)

• $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner \exists x\varphi \urcorner ))=t$ iff (by $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$)

• $Val_{\mathcal {M}^{n}}(\exists z Tr^{n}(sub(\ulcorner \varphi \urcorner ,x,num(z))))=t$ iff

• there is a d∈D, such that $Val_{\mathcal {M}^{n}}(Tr^{n}(\ulcorner [\varphi ]_{x}^{\bar {d}}\urcorner ))=t$ iff (by axiom 1, which was proved in ‘ad 1’)

• there is a d∈D, such that $Val_{\mathcal {M}^{n}(E)}(Tr^{n+1}(\ulcorner [\varphi ]_{x}^{\bar {d}}\urcorner ))=t$ iff

• $\mathcal {M}^{n}(E)\vDash \exists z Tr^{n+1}(sub(\ulcorner \varphi \urcorner ,x,num(z)))$.

Thus, in both cases it holds that $\mathcal {M}^{n}(E)\vDash Tr^{n+1}(\ulcorner \exists x\varphi \urcorner )\leftrightarrow \linebreak \exists z Tr^{n+1}(sub(\ulcorner \varphi \urcorner ,x,num(z)))$, in other words $\mathcal {M}^{n}(E)\vDash Tr^{n+1}$(∃̣$\bar {d_{1}} \bar {d_{2}})\leftrightarrow \exists z Tr^{n+1}(sub(\bar {d_{2}},\bar {d_{1}},num(z)))$.

Analogously to ‘ad 6’.

Analogously distinguishing the cases c ⁿ⁺¹(φ)∈L ⁿ and c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ.

Assume $\mathcal {M}^{n}(E)\vDash Sent_{\mathcal {L}^{n+1}}\left (\bar {d}\right )$. It follows that there is a sentence φ such that $\mathcal {M}^{n}(E)\vDash \bar {d}\equiv \ulcorner \varphi \urcorner$, and either c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ or c ⁿ⁺¹(φ)∈L ⁿ.

Assume c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ. Since $Val_{\mathcal {M}^{n}(E)}(\varphi )\neq Val_{\mathcal {M}^{n}(E)}(\neg \varphi )$, $Val_{\mathcal {M}^{n}(E)}(\varphi )=t$ and $Val_{\mathcal {M}^{n}(E)}(\neg \varphi )=t$ cannot both hold. Therefore, $Val_{\mathcal {M}^{n}(E,A)}(\varphi )=t$ and $Val_{\mathcal {M}^{n}(E,A)}(\neg \varphi )=t$ cannot both be the case. Since c ⁿ⁺¹(φ)∈L ⁿ⁺¹∖L ⁿ, we thus obtain either c ⁿ⁺¹(φ)∉E or c ⁿ⁺¹(¬φ)∉E. Hence, either $\mathcal {M}^{n}(E)\vDash \neg Tr^{n+1}(\ulcorner \varphi \urcorner ))$ or $\mathcal {M}^{n}(E)\vDash \neg Tr^{n+1}(\ulcorner \neg \varphi \urcorner ))$, and so $\mathcal {M}^{n}(E)\vDash \neg Tr^{n+1}(\ulcorner \varphi \urcorner ))\vee \neg Tr^{n+1}(\ulcorner \neg \varphi \urcorner ))$. Therefore, $\mathcal {M}^{n}(E)\vDash \neg (Tr^{n+1}(\ulcorner \varphi \urcorner )\wedge Tr^{n+1}(\ulcorner \neg \varphi \urcorner ))$.

In case that c ⁿ⁺¹(φ)∈L ⁿ, we obtain $\mathcal {M}^{n}\vDash \neg (Tr^{n}(\ulcorner \varphi \urcorner )\wedge Tr^{n}(\ulcorner \neg \varphi \urcorner ))$ by $\mathcal {M}^{n}\vDash \text {KF}^{\prime }_{n}$ and by axiom 9 of $\text {KF}^{\prime }_{n}$. Therefore, $\mathcal {M}^{n}(E)\vDash \neg (Tr^{n}(\ulcorner \varphi \urcorner )\wedge Tr^{n}(\ulcorner \neg \varphi \urcorner ))$, and by axiom 1, which was proved in ‘ad 1’, we obtain $\mathcal {M}^{n}(E)\vDash \neg (Tr^{n+1}(\ulcorner \varphi \urcorner )\wedge Tr^{n+1}(\ulcorner \neg \varphi \urcorner ))$ □

Proof of corollary 4.1

• 1. The first claim is a generalisation of Lemma 4.1 and is demonstrated analogously.

• 2. The second claim is an immediate consequence of the first axioms of $\text {KF}^{\prime }_{n}$, $\text {KF}^{\prime }_{n+1}$, …, $\text {KF}^{\prime }_{m}$.

• 3. The third claim follows from claim 2 of this lemma and the second axioms of $\text {KF}^{\prime }_{n}$, $\text {KF}^{\prime }_{n+1}$, …, $\text {KF}^{\prime }_{m}$.

• 4. The fourth claim is demonstrated by induction over the depth i of a truth-diagnosis about φ of $\mathcal {L}^{k}$.

Let i = 1. We obtain the claim by the following steps:

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \varphi \urcorner )$ iff (since $\mathcal {M}^{n+1}$ is a {T r ⁿ⁺¹}-expansion of $\mathcal {M}^{n}$)

• $\mathcal {M}^{n+1}\vDash Tr^{n}(\ulcorner \varphi \urcorner )$ iff (by axiom 1 of $\text {KF}^{\prime }_{n+1}$ and φ is a sentence of $\mathcal {L}^{k}$)

• $\mathcal {M}^{n+1}\vDash Tr^{n+1}(\ulcorner \varphi \urcorner )$ iff (by analogous reasoning)

• $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner \varphi \urcorner )$

Therefore, $\mathcal {M}^{m}\vDash Tr^{n}(\ulcorner \varphi \urcorner )\leftrightarrow Tr^{m}(\ulcorner \varphi \urcorner )$ and $\mathcal {M}^{m}\vDash \neg Tr^{n}(\ulcorner \varphi \urcorner )\leftrightarrow \linebreak \neg Tr^{m}(\ulcorner \varphi \urcorner )$.

Let i=2. There are four possible types of iterated T r ⁿ-diagnoses $S^{n}(\ulcorner \varphi \urcorner )$ about φ of depth 2: ‘(0,0)’, ‘(0,1)’, ‘(1,0)’ or ‘(1,1)’. We start with assuming that the type of $S^{n}(\ulcorner \varphi \urcorner )$ is ‘(1,0)’, i.e. $S^{n}(\ulcorner \varphi \urcorner )= Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner \varphi \urcorner )\urcorner )$. Then we derive $\mathcal {M}^{m}\vDash S^{n}(\ulcorner \varphi \urcorner )\leftrightarrow S^{m}(\ulcorner \varphi \urcorner )$ by the following steps:

• $\mathcal {M}^{m}\vDash S^{n}(\ulcorner \varphi \urcorner )$ iff

• $\mathcal {M}^{m}\vDash Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner \varphi \urcorner )\urcorner )$ iff (since $\mathcal {M}^{m}$ is a {T r ⁿ⁺¹,T r ⁿ⁺²,…,T r ^m}-expansion of $\mathcal {M}^{n}$)

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner \varphi \urcorner )\urcorner )$ iff (by axiom 3a of $\text {KF}^{\prime }_{n}$ and since φ is a sentence of $\mathcal {L}^{k}$ and thus of $\mathcal {L}^{n-1}$)

• $\mathcal {M}^{n}\vDash \neg Tr^{n-1}(\ulcorner \varphi \urcorner )$ iff (by the first axiom of $\text {KF}^{\prime }_{n}$ and since φ is a sentence of $\mathcal {L}^{k}$ and thus of $\mathcal {L}^{n-1}$)

• $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \varphi \urcorner )$ iff (since $\mathcal {M}^{n+1}$ is a {T r ⁿ⁺¹}-expansion of $\mathcal {M}^{n}$)

• $\mathcal {M}^{n+1}\vDash \neg Tr^{n}(\ulcorner \varphi \urcorner )$ iff (by the first axiom of $\text {KF}^{\prime }_{n+1}$ and since φ is a sentence of $\mathcal {L}^{k}$ and thus of $\mathcal {L}^{n}$)

• $\mathcal {M}^{n+1}\vDash \neg Tr^{n+1}(\ulcorner \varphi \urcorner )$ iff (by analogous reasoning)

• $\mathcal {M}^{m-1}\vDash \neg Tr^{m-1}(\ulcorner \varphi \urcorner )$ iff (since $\mathcal {M}^{m}$ is a {T r ^m}-expansion of $\mathcal {M}^{m-1}$)

• $\mathcal {M}^{m}\vDash \neg Tr^{m-1}(\ulcorner \varphi \urcorner )$ iff (by axiom 3a of $\text {KF}^{\prime }_{m}$ and since φ is a sentence of $\mathcal {L}^{k}$ and thus of $\mathcal {L}^{m-1}$)

• $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner \neg Tr^{m}(\ulcorner \varphi \urcorner )\urcorner )$ iff

• $\mathcal {M}^{m}\vDash S^{m}(\ulcorner \varphi \urcorner )$

We obtain $\mathcal {M}^{m}\vDash S^{n}(\ulcorner \varphi \urcorner )\leftrightarrow S^{m}(\ulcorner \varphi \urcorner )$ for the three other possible depth-2 types of $S^{n}(\ulcorner \varphi \urcorner )$ by similar reasoning.

We now show “ i→i+1”, where i≥2. Assume that for each type τ of depth i, $\mathcal {M}^{m}\vDash S^{n}(\ulcorner \varphi \urcorner )\leftrightarrow S^{m}(\ulcorner \varphi \urcorner )$, where $S^{n}(\ulcorner \varphi \urcorner )$ is the iterated T r ⁿ-diagnosis about φ of type τ and $S^{m}(\ulcorner \varphi \urcorner )$ is the iterated T r ^m-diagnosis about φ of type τ. Let $U^{n}(\ulcorner \varphi \urcorner )$ be any iterated T r ⁿ-diagnosis about φ of depth i+1, and let $U^{m}(\ulcorner \varphi \urcorner )$ be the respective iterated T r ^m-diagnosis about φ of depth i+1 and of the same type as $U^{n}(\ulcorner \varphi \urcorner )$.

The type of $U^{n}(\ulcorner \varphi \urcorner )$ and $U^{m}(\ulcorner \varphi \urcorner )$ begins with either one of the following pairs:‘(0,0)’, ‘(0,1)’, ‘(1,0)’ or ‘(1,1)’. We start with assuming that the type of $U^{n}(\ulcorner \varphi \urcorner )$ begins with ‘(1,0)’, i.e. $U^{n}(\ulcorner \varphi \urcorner )=Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner V^{n}(\ulcorner \varphi \urcorner )\urcorner )\urcorner )$ where $V^{n}(\ulcorner \varphi \urcorner )$ is a T r ⁿ-diagnosis about φ of depth i−1. Since we have assumed that i≥2, i−1≥1, and so $V^{n}(\ulcorner \varphi \urcorner )$ is a “proper” T r ⁿ-diagnosis. Then we derive $\mathcal {M}^{m}\vDash U^{n}(\ulcorner \varphi \urcorner )\leftrightarrow U^{m}(\ulcorner \varphi \urcorner )$ by the following steps:

• $\mathcal {M}^{m}\vDash U^{n}(\ulcorner \varphi \urcorner )$ iff

• $\mathcal {M}^{m}\vDash Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner V^{n}(\ulcorner \varphi \urcorner )\urcorner )\urcorner )$ iff (since $\mathcal {M}^{m}$ is a {T r ⁿ⁺¹,T r ⁿ⁺²,…,T r ^m}-expansion of $\mathcal {M}^{n}$)

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner V^{n}(\ulcorner \varphi \urcorner )\urcorner )\urcorner )$ iff (by axiom 3b of $\text {KF}^{\prime }_{n}$ and $V^{n}(\ulcorner \varphi \urcorner )$ is a sentence of $\mathcal {L}^{n}\backslash \mathcal {L}^{n-1}$)

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg V^{n}(\ulcorner \varphi \urcorner )\urcorner )$ iff (since $\mathcal {M}^{m}$ is a {T r ⁿ⁺¹,T r ⁿ⁺²,…,T r ^m}-expansion of $\mathcal {M}^{n}$)

• $\mathcal {M}^{m}\vDash Tr^{n}(\ulcorner \neg V^{n}(\ulcorner \varphi \urcorner )\urcorner )$ iff (by the induction hypothesis and $Tr^{n}(\ulcorner \neg V^{n}(\ulcorner \varphi \urcorner )\urcorner )$ is an iterated T r ⁿ-diagnosis about φ of depth i)

• $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner \neg V^{m}(\ulcorner \varphi \urcorner )\urcorner )$ (where $V^{m}(\ulcorner \varphi \urcorner )$ is the T r ^m-diagnosis about φ with the same type as $V^{n}(\ulcorner \varphi \urcorner )$) iff (by axiom 3b of KF _m and $V^{m}(\ulcorner \varphi \urcorner )$ is a sentence of $\mathcal {L}^{m}\backslash \mathcal {L}^{m-1}$)

• $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner \neg Tr^{m}(\ulcorner V^{m}(\ulcorner \varphi \urcorner )\urcorner )\urcorner )$ iff

• $\mathcal {M}^{m}\vDash U^{m}(\ulcorner \varphi \urcorner )$

We obtain $\mathcal {M}^{m}\vDash U^{n}(\ulcorner \varphi \urcorner )\leftrightarrow U^{m}(\ulcorner \varphi \urcorner )$ in case of the three other possible types by similar reasoning.

5. The fifth claim is demonstrated by induction over the depth i of the iterated T r ⁿ-diagnosis of $S(\ulcorner \lambda ^{n}\urcorner )$ about λ ⁿ. Let i=1. We obtain the induction basis by $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )$ and $\mathcal {M}^{n}\nvDash Tr^{n}(\ulcorner \lambda ^{n}\urcorner )$ (which are immediate consequences of the first claim of this Lemma). Thus there is no T r ⁿ-diagnosis about λ ⁿ of depth 1 that begins with ‘1’ and that is true in $\mathcal {M}^{n}$.

Let i=2. We have $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )$. By Lemma 3.3 and $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \lambda ^{n}\urcorner )\leftrightarrow Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )\urcorner )$, we obtain $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )\urcorner )$. By $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )$ and axiom 2 of $\text {KF}^{\prime }_{n}$, we obtain $\mathcal {M}^{n}\vDash \linebreak \neg Tr^{n}(\ulcorner Tr^{n}(\ulcorner \lambda ^{n}\urcorner )\urcorner )$. Thus there is no T r ⁿ-diagnosis about λ ⁿ of depth 2 that begins with ‘1’ and that is true in $\mathcal {M}^{n}$.

We show “ i→i+1”, where i≥2. Assume that the type of each iterated T r ⁿ-diagnosis about λ ⁿ of depth i and that is true in $\mathcal {M}^{n}$, begins with ‘0’. Furthermore, assume for reductio that there is an iterated T r ⁿ-diagnosis about λ ⁿ of depth i+1 that begins with ‘1’ and that is true in $\mathcal {M}^{n}$. Then there is a T r ⁿ-diagnosis $S(\ulcorner \lambda ^{n}\urcorner )$ about λ ⁿ of depth i such that $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner S(\ulcorner \lambda ^{n}\urcorner )\urcorner )$.

Assume that the type of $S(\ulcorner \lambda ^{n}\urcorner )$ begins with ‘0’, i.e. $S(\ulcorner \lambda ^{n}\urcorner )=\linebreak \neg Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner )$ where $S^{\prime }(\ulcorner \lambda ^{n}\urcorner )$ is a T r ⁿ-diagnosis about λ ⁿ of depth i−1≥1 (by i≥2). Then we derive a contradiction by the following steps:

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner S(\ulcorner \lambda ^{n}\urcorner )\urcorner )$ iff (by $S(\ulcorner \lambda ^{n}\urcorner )=\neg Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner ))$

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner )\urcorner )$ iff (by axiom 3b of $\text {KF}^{\prime }_{n}$ and since $S^{\prime }(\ulcorner \lambda ^{n}\urcorner )$ is a sentence of $\mathcal {L}^{n}\backslash \mathcal {L}^{n-1}$)

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner \neg S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner )$

Thus, there would an iterated T r ⁿ-diagnosis about λ ⁿ of depth i that does not begin with ‘0’ and that is true in $\mathcal {M}^{n}$, which contradicts the induction hypothesis.

If the type of $S(\ulcorner \lambda ^{n}\urcorner )$ begins with ‘1’, i.e. $S(\ulcorner \lambda ^{n}\urcorner )=Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner )$ where $S^{\prime }(\ulcorner \lambda ^{n}\urcorner )$ is a T r ⁿ-diagnosis about λ ⁿ of depth i−1, then we derive a contradiction by the following steps:

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner S(\ulcorner \lambda ^{n}\urcorner )\urcorner )$ iff (by $S(\ulcorner \lambda ^{n}\urcorner )=Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner ))$

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner )\urcorner )$ iff (by axiom 2 of $\text {KF}^{\prime }_{n}$)

• $\mathcal {M}^{n}\vDash Tr^{n}(\ulcorner S^{\prime }(\ulcorner \lambda ^{n}\urcorner )\urcorner )$

Thus, there would be an iterated T r ⁿ-diagnosis about λ ⁿ of depth i that does not begin with ‘0’ and that is true in $\mathcal {M}^{n}$, which contradicts the induction hypothesis as well. In consequence, there can be no T r ⁿ-diagnosis about λ ⁿ of depth i+1 that begins with ‘1’ and that is true in $\mathcal {M}^{n}$.

6. By $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )$ and the first axioms of $\text {KF}^{\prime }_{n+1}$, …, $\text {KF}^{\prime }_{m-1}$, we obtain $\mathcal {M}^{m-1}\vDash \neg Tr^{m-1}(\ulcorner \lambda ^{n}\urcorner )$. Moreover, by axiom 3a of $\text {KF}^{\prime }_{m}$ we obtain $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner \neg Tr^{m}(\ulcorner \lambda ^{n}\urcorner )\urcorner )$. By iterated application of the second axiom of $\text {KF}^{\prime }_{m}$, we derive $\mathcal {M}^{m}\vDash Tr^{m}(\ulcorner Tr^{m}(\ulcorner {\ldots } Tr^{m}(\ulcorner \neg Tr^{m}(\ulcorner \lambda ^{n}\urcorner )\urcorner )\ldots \urcorner )\urcorner )$. On the other hand, we have $\mathcal {M}^{n}\vDash \neg Tr^{n}(\ulcorner Tr^{n}(\ulcorner {\ldots } Tr^{n}(\ulcorner \neg Tr^{n}(\ulcorner \lambda ^{n}\urcorner )\urcorner )\ldots \urcorner )\urcorner )$ (in consequence of claim 5 of this Lemma) □

Proof of corollary 4.2

• 1. The claim is derived analogously to the first claim of Lemma 4.2.

• 2. The claim is derived analogously to the second claim of Lemma 4.2.

• 3. The claim is an immediate consequence of the first claim of Corollary 4.1.

□