2.1 Preliminaries from provability logic

Let $\mathbb {P}$ be a set of propositional variables. The syntax of modal logic is obtained by adding the modal operator $\Box $ to propositional logic. So if $\varphi $ is a formula, then $\Box \varphi $ is a formula. As usual, $\lozenge $ is used as a shorthand for $\neg \Box \neg $ and $\bot $ for the logical constant “false.”

The system $\mathbf {GL}$ is defined by the following axioms schemata and rules:

• • propositional tautologies,

• • K. $\Box (\varphi \rightarrow \psi ) \rightarrow (\Box \varphi \rightarrow \Box \psi )$ ,

• • Löb. $\Box (\Box \varphi \rightarrow \varphi ) \rightarrow \Box \varphi $ ,

• • MP. $\vdash \varphi ,\ \vdash \varphi \rightarrow \psi \Rightarrow \vdash \psi $ ,

• • Nec. $\vdash \varphi \Rightarrow \Box \varphi $ .

A Kripke frame is a pair $\mathfrak {F}=(W,R)$ where W is a non-empty set and $R\subseteq W\times W$ is an accessibility relation. A Kripke model is a triple $\mathfrak {M}=(W,R,\nu )$ where $\nu $ is a valuation function which assigns to each $p\in \mathbb {P}$ a subset of W. The valuation function $\nu $ is extended to all formulas as follows:

$$ \begin{align*} \nu(\neg\varphi)&= W - \nu(\varphi),\\ \nu(\varphi \wedge \psi) &= \nu(\varphi)\cap \nu(\psi),\\ \nu(\Box\varphi)&= \{w\in W\ |\ (\forall v\in W)\ wRv\rightarrow v\in \nu(\varphi)\}. \end{align*} $$

A formula $\varphi $ is valid in $\mathfrak {M}$ if $\nu (\varphi )=W$ ; also, it is valid in $\mathfrak {F}$ if it is valid in every model based on $\mathfrak {F}$ .

The Kripke completeness of $\mathbf {GL}$ can facilitate the method of proving the other completeness results. To be more precise, for a given class of structures, instead of proving the completeness directly, one can find a way to transform the validity from this class to the class of Kripke frames. This idea is also used by Blass to give a sufficient condition for the completeness of $\mathbf {GL}$ with respect to any family of filters. To this end, a particular class of trees named $\mathbf {K}_n$ is considered in [Reference Blass10] as a crossing point between these two classes.

For each fixed natural number n, the nodes of $\mathbf {K}_n$ consist of all finite sequences of pairs $\langle (i_1,j_1), \dots ,(i_k,j_k)\rangle $ where $n>i_1>\dots > i_k\geq 0$ and $j_1,\dots ,j_k\in \omega $ are arbitrary. The order of $\mathbf {K}_n$ , denoted by $\lhd $ , is the end extension order; thus, t extends s iff $s \lhd t$ . So the root of $\mathbf {K}_n$ is the empty sequence $\langle \rangle $ , and the height of the tree is n. Also, each node with height $0<i \leq n$ has infinitely many immediate successors of height j for each $j<i$ .

It is easy to see that each finite transitive tree $(W,R)$ with height n is a bounded morphic image of $\mathbf {K}_n$ . That is, there is an onto function f from the nodes of $\mathbf {K}_n$ to W such that for any $s,t\in \mathbf {K}_n$ and $w\in W$ we have:

• • $s \lhd t$ implies $f(s)R f(t)$ .

• • If $f(s)R w$ , then there is $t\in \mathbf {K}_n$ such that $s \lhd t$ and $f(t)=w$ .

It is easy to see that the validity of formulas is preserved under bounded morphic images. So, by Proposition 2.1, we have:

• • If $\mathbf {GL}\vdash \varphi $ , then $\varphi $ is valid in $\mathbf {K}_n$ for every n.

Suppose that $\vec {\mathcal {F}}=\langle \mathcal {F}_{\alpha }: \alpha \in On \rangle $ is a family of filters where $\mathcal {F}_{\alpha }$ is a filter on $\alpha $ , for each $\alpha \in On$ . A valuation $\nu $ on this family is a function which assigns a class of ordinals to each $p\in \mathbb {P}$ . Then the valuation function $\nu $ is extended to all formulas by the standard rules for Boolean connectives and the following for $\Box $ operator:

$$ \begin{align*} \nu(\Box\varphi)&= \{\alpha\ |\ \nu(\varphi)\in \mathcal{F}_{\alpha}\}. \end{align*} $$

Then for the dual operator $\lozenge $ we have

$$ \begin{align*} \nu(\lozenge\varphi)=\{\alpha\ |\ \nu(\varphi) \text{ has positive measure w.r.t } \mathcal{F}_{\alpha}\}. \end{align*} $$

A formula $\varphi $ is $\vec {\mathcal {F}}$ -valid if for every valuation $\nu $ on $\vec {\mathcal {F}}$ we have $\nu (\varphi )=On$ .

In this paper, we are interested in the filter sequence of normal measures $\vec {\mathcal {M}}=\langle \mathcal {M}_{\alpha }: \alpha \in On \rangle ,$ where for each $\alpha $ , $\mathcal {M}_{\alpha }$ is the intersection of all normal measures on $\alpha $ .

Note that in $\vec {\mathcal {M}}$ , the formula $\lozenge \top $ determines the class of all measurable cardinals; reciprocally, $\Box \bot $ defines the class of all non-measurable ordinals. Furthermore, $\lozenge ^n \top $ is true at an ordinal $\alpha $ if and only if $\alpha $ is a measurable cardinal with Mitchell order $\geq n$ (see Definition 2.7).

By showing that for any $\alpha $ and A if $A\in \mathcal {M}_{\alpha }$ , then $\{\beta <\alpha : A\cap \beta \in \mathcal {M}_{\beta }\}\in \mathcal {M}_{\alpha }$ ; Blass proved the following soundness theorem.

From the soundness result, one can indicate some properties of measurable cardinals. For example, Blass showed that the validity of the Löb formula implies that any measurable cardinal $\kappa $ has a normal measure containing $\{\alpha <\kappa : \alpha \text { is not measurable}\}$ . Also, if A has a positive measure with respect to $\mathcal {M}_{\kappa }$ , then so does the set $\{\alpha \in A : \alpha \text { has no normal filter containing } A\}$ . More generally, one can see that the validity of $\lozenge ^{n+1}\top \rightarrow \lozenge (\lozenge ^m\top \wedge \Box ^{m+1}\bot )$ for each $m<n$ implies that any measurable cardinal $\kappa $ with $o(\kappa )\geq n$ has a normal measure containing $\{\alpha <\kappa : o(\alpha )=m\}$ , where $o(\alpha )$ is the Mitchell order of $\alpha $ (see Definition 2.7).

The following lemma gives a sufficient condition to convert a Kripke interpretation of a given formula into a filter interpretation (see the proof of Theorem 3 in [Reference Blass10] for information on how this conversion is defined). So, the main part of the proof of Theorem 1.1 is to show that the following lemma holds for a family of normal filter sequences; the proof is given in Section 3. Then the completeness of $\mathbf {GL}$ with respect to these filters is obtained by Proposition 2.1.

2.2 Preliminaries from set theory

In this subsection we recall some definitions and facts about measurable cardinals and their Mitchell order structure.

One can show that any measurable cardinal $\kappa $ carries a normal measure, i.e., a $\kappa $ -complete non-principal ultrafilter $\mathcal {U}$ on $\kappa $ which is normal:

$$\begin{align*}\forall \xi < \kappa, A_{\xi} \in \mathcal{U} \Rightarrow \bigtriangleup_{\xi<\kappa}A_{\xi}=\{\alpha < \kappa: \forall\xi<\alpha,~\alpha \in A_{\xi} \}\in \mathcal{U}. \end{align*}$$

Given a normal measure $\mathcal {U}$ on $\kappa $ we can perform the ultrapower $\text {Ult}(V, \mathcal {U})$ and the ultrapower embedding $j: V \to \text {Ult}(V, \mathcal {U})$ which is defined by $j(x) = [c_x]_{\mathcal {U}}$ , where $c_x: \kappa \to V$ is the constant function x. By Łoś theorem, j is easily seen to be an elementary embedding. On the other hand, $\text {Ult}(V, \mathcal {U})$ is well-founded, and hence it is isomorphic to a unique transitive inner model $M_{\mathcal {U}}$ via a unique isomorphism $\pi : \text {Ult}(V, \mathcal {U}) \simeq M_{\mathcal {U}}$ . Then $j_{\mathcal {U}}: V \to M_{\mathcal {U}}$ , defined by $j_{\mathcal {U}}=\pi \circ j$ defines an elementary embedding from the universe V into an inner model $M_{\mathcal {U}}$ with critical point $\kappa $ (i.e., $j_{\mathcal {U}} \restriction \kappa =\text {id}\restriction \kappa $ and $j_{\mathcal {U}}(\kappa )> \kappa $ ).

Conversely, given a non-trivial elementary embedding $j: V \to M$ from V into an inner model M with critical point $\kappa ,$ one can form the normal measure

$$\begin{align*}\mathcal{U}=\{ X \subseteq \kappa: \kappa \in j(X) \} \end{align*}$$

on $\kappa $ and then j factors through $j_{\mathcal {U}}$ in the sense that $j=k \circ j_{\mathcal {U}}$ , where $k: M_{\mathcal U} \to M$ is defined as $k([f]_{\mathcal U})=j(f)(\kappa )$ .

We now define an order on normal measures introduced by Mitchell.

In [Reference Mitchell15], Mitchell proved that $\lhd $ is a well-founded order now known as the Mitchell ordering. Thus, given any normal measure $\mathcal {U}$ on $\kappa ,$ we can define its Mitchell order as

$$\begin{align*}o(\mathcal{U})=\sup\{o(\mathcal{W})+1: \mathcal{W} \lhd \mathcal{U} \}. \end{align*}$$

The Mitchell order of $\kappa $ is also defined as

$$\begin{align*}o(\kappa)=\sup\{o(\mathcal{U})+1: \mathcal{U} \text{~is a normal measure on~}\kappa \}. \end{align*}$$

Definition 2.7. Suppose $\kappa $ is a measurable cardinal. Then

$$\begin{align*}\lhd(\kappa)= (\{ \mathcal{U}: \mathcal{U} \text{~is a normal measure on~}\kappa \}, \lhd). \end{align*}$$

The structure of $\lhd (\kappa )$ is widely studied in set theory, we refer to [Reference Ben-Neria8, Reference Ben-Neria9] for most recent results. We will need the following, which plays an essential role in the proof of Theorem 1.1.

Let us recall that a forcing notion $(\mathbb {Q}, \leq , \leq ^*)$ satisfies the Prikry property if $\leq ^* \subseteq \leq $ and for each $p \in \mathbb {Q}$ and each sentence $\sigma $ in the forcing language of $(\mathbb {Q}, \leq )$ , there exists $q \leq ^* p$ such that q decides $\sigma $ . The key point is that in general $(\mathbb {Q}, \leq )$ lacks to be even $\aleph _1$ -distributive, but if $(\mathbb {Q}, \leq , \leq ^*)$ satisfies the Prikry property and $(\mathbb {Q}, \leq ^*)$ is $\kappa $ -closed, then forcing with $(\mathbb {Q}, \leq )$ does not add new bounded subsets to $\kappa .$ We may note that Ben-Neria’s forcing of the above theorem can be considered as a Prikry type forcing notion $(\mathbb {Q}, \leq , \leq ^*)$ , and furthermore, given any $\theta < \kappa $ , we can manage the forcing so that $(\mathbb {Q}, \leq ^*)$ is $\theta $ -closed, in particular it does not add any new bounded subsets to $\theta $ .

The following is an immediate corollary of the above theorem, whose proof requires familiarity with Prikry type forcing notions and their iterations (see [Reference Gitik12] for more information).Footnote ¹

It is worth mentioning that the usual iteration of Prikry type forcing notions, say, for example, finite support iteration, fails to preserve cardinals. To give a motivation of why this happens, let $\langle \kappa _n: n<\omega \rangle $ be an increasing sequence of measurable cardinals and let $\kappa =\sup _{n<\omega }\kappa _n$ . For each $n< \omega $ , let $\mathcal U_n$ be a normal measure on $\kappa _n$ and let $\mathbb {P}_n$ be the corresponding Prikry forcing. Thus a condition in $\mathbb {P}_n$ is a pair $(s, A),$ where $s \in [\kappa _n]^{<\omega }, A \in \mathcal U_n$ , and $\max (s) < \min (A)$ . Given another condition $(t, B)$ , we say $(t, B) \leq (s, A)$ iff $s \unlhd t, B \subseteq A$ , and $t \setminus s \subseteq A.$ The direct extension order is defined as $(t, B) \leq ^* (s, A)$ iff $(t, B) \leq (s, A)$ and $s=t$ . Forcing with $\mathbb {P}_n$ adds an $\omega $ -sequence $C_n \subseteq \kappa _n$ , which is cofinal in $\kappa _n$ , called the Prikry sequence. Now let $\mathbb {P}$ be the finite support product of $\mathbb {P}_n$ ’s.Footnote ² Thus a condition in $\mathbb {P}$ is a sequence $p= \langle p_n: n<\omega \rangle $ , where each $p_n \in \mathbb {P}_n$ , and for all but finitely many $n, p_n=(\emptyset , \kappa _n)=1_{\mathbb {P}_n}$ . We claim that forcing with $\mathbb {P}$ collapses $\kappa $ into $\omega $ . To see this, let G be $\mathbb {P}$ -generic over V, and for each n, let $C_n$ be the Prikry sequence added by it thorough $\kappa _n.$ Define $f: \omega \rightarrow \kappa $ by $f(n)=\min (C_n)$ . Given any $\alpha < \kappa ,$ it is easy to see that the set

$$ \begin{align*} D_{\alpha}=\{p= \langle p_n: n<\omega\rangle \in \mathbb{P}: \exists n \big( \kappa_n> \alpha,~ p_n=(\{\alpha\}, \kappa_n \setminus (\alpha+1)) \big) \} \end{align*} $$

is dense in $\mathbb {P}$ . But if $p \in D_{\alpha }$ is as above, then $p \Vdash _{\mathbb {P}}$ “ .” It follows that $\text {range}(f)=\kappa $ , and thus $\kappa $ is collapsed.

However, there are other ways to iterate Prikry type forcing notions that avoid the above problem; the most known methods are the Magidor iteration (full support iteration) and Gitik iteration (Easton support iteration). Such kinds of iterations satisfy the Prikry property, and by using this fact, one can show that the resulting forcing behaves nicely.

Proof Recall from the above that Ben-Neria’s forcing of Theorem 2.8 is a Prikry type forcing notion $(\mathbb {Q}, \leq , \leq ^*)$ . Now let $\langle \kappa _n: n<\omega \rangle $ and $\langle (\mathbf {S}_n, <_n): n<\omega \rangle $ be as above. For each $n<\omega $ , let $\langle \lambda ^n_i: i \leq \omega \rangle $ be the first $\omega +1$ measurable cardinals above $\kappa _n$ .Footnote ⁴ Then, for each n, $\lambda ^n_{\omega } < \kappa _{n+1}$ . Let

be the Magidor iteration of Prikry type forcing notions, where for each $n<\omega $ ,

is defined in $V^{\mathbb {P}_n}$ such that:

1. (1) $|\mathbb {Q}_n| < \kappa _{n+1}$ .

2. (2) $(\mathbb {Q}_n, \leq ^*_{\mathbb {Q}_n})$ is $\lambda ^{n-1}_{\omega }$ -closed, in particular it adds no new bounded subsets to $\lambda ^{n-1}_{\omega }$ .

3. (3) $\lhd (\kappa _n)^{V^{\mathbb {P}_{n+1}}} \simeq (\mathbf {S}_n, <_n)$ .

This is possible by Theorem 2.8 (and its proof) and the fact that by (1), all cardinals $\kappa _m,$ for $m>n$ , remain strong in the extension by $\mathbb {P}_{n+1}$ . Then $V^*=V^{\mathbb {P}_{\omega }}$ is the required model.