Convention 2.1. Subindices will be used mainly for disambiguation and will be dropped when this does not lead to confusion. Thus if $\mathfrak X$ is a dynamic topological system, we may write, e.g., f instead of $f_{\mathfrak {X}}$ . We may also on occasion introduce alternative notation for the components of a given structure $:$ if we write, e.g., $\mathfrak X = (X, \mathcal T, f)$ , this means that $|\mathfrak X| = X$ , $\mathcal T_{\mathfrak {X}}=\mathcal T$ , and $f_{\mathfrak {X}} = f$ . Nevertheless, such usage will be preceded with due warning. A similar convention applies for topological spaces and other classes of structures.

Proof. Let $\Phi $ be a prime $\mathcal L$ -type. Observe that $\Phi $ is already saturated by definition, so it remains to check that it satisfies all conditions of Definition 4.1. Conditions 1 and 2 follow from the consistency of $\Phi $ . The proofs of the other conditions are all similar to each other. For example, for 7, suppose that $\varphi \to \psi \in \Phi ^+$ and $\varphi \not \in \Phi ^-$ . Since $\Phi $ is saturated, it follows that $\varphi \in \Phi ^+$ . But $\big (\varphi \wedge (\varphi \to \psi )\big ) \to \psi $ is an intuitionistic tautology, so using the fact that $\Phi $ is consistent we see that $\psi \not \in \Psi ^-$ , which using the assumption that $\Phi $ is saturated gives us $\psi \in \Phi ^+$ . For condition 9 we use (E1): if $\Diamond \varphi \in \Phi ^-$ and $\varphi \in \Phi ^+$ we would have that $\Phi $ is inconsistent; hence $\varphi \in \Phi ^-$ . The rest of the conditions are left to the reader.⊣

Proof. The proof is standard, but we provide a sketch. Let $\varphi \in \mathcal L $ . Note that either $\Gamma ,\varphi \not \vdash \Delta $ or $\Gamma \not \vdash \Delta ,\varphi $ , for otherwise by a cut rule (which is intuitionistically derivable) we would have $\Gamma \vdash \Delta $ . Thus we can add $\varphi $ to $\Gamma \cup \Delta $ , and by repeating this process for each element of $\mathcal L $ (or using Zorn’s lemma) we can find suitable $\Phi $ .⊣

Proof. We know that $\preccurlyeq _{T}$ is a partial order and restrictions of partial orders are partial orders, so $\preccurlyeq _\Lambda $ is a partial order. Moreover, $\ell _\Lambda $ is the identity, so $\Phi \preccurlyeq _\Lambda \Psi $ implies that $\ell _\Lambda (\Phi ) \preccurlyeq _{T} \ell _\Lambda (\Psi )$ .

Now let $\Phi \in |{\mathfrak M}_\Lambda |$ and assume that $\varphi \to \psi \in \Phi ^-$ . Note that $ \Phi ^+,\varphi \not \vdash \psi $ , for otherwise by intuitionistic reasoning we would have $\Phi ^+\vdash \varphi \to \psi $ ; hence $ \Phi ^+,\varphi \not \vdash \psi $ , contrary to our assumption. By Lemma 5.3, there is a prime type $\Psi $ with $\Phi ^+ \cup \{\varphi \} \subseteq \Psi ^+$ and $\psi \in \Psi ^-$ . It follows that $\Phi \preccurlyeq _\Lambda \Psi $ , $\varphi \in \Psi ^+$ , and $\psi \in \Psi ^-$ , as needed.⊣

Proof. For a set $\Gamma \subseteq \mathcal L $ , recall that we had defined $\circ \Gamma = \{\circ \varphi : \varphi \in \Gamma \}$ . Define also $\ominus \Gamma = \{\varphi : \circ \varphi \in \Gamma \}$ . With this, we show that $S_\Lambda $ is functional and forward-confluent.

Functionality. Let $\Phi \in |{\mathfrak M}_\Lambda |$ and define $\Psi = (\ominus \Phi ^+,\ominus \Phi ^-)$ . We claim that $\Phi \mathrel S_T\Psi $ and that if $\Phi \mathrel S_T\Theta $ , it follows that $\Theta =\Psi $ . Recall that $\Phi \mathrel S_T\Theta $ means that the pair $(\Phi ,\Theta )$ is sensible (in the sense of Definition 4.6).

First we must check that $\Psi \in |{\mathfrak M}_\Lambda |$ . To see that $\Psi $ is saturated, let $\varphi \in \mathcal L_\Diamond $ be so that $\varphi \not \in \Psi ^-$ . It follows that $\circ \varphi \not \in \Phi ^-$ , but $\Phi $ is saturated, so $\circ \varphi \in \Phi ^+$ and thus $\varphi \in \Psi ^+$ . Since $\varphi $ was arbitrary, $\Psi ^-\cup \Psi ^+ = \mathcal L_\Diamond $ . Next we check that $\Psi $ is consistent. If not, let $\Gamma \subseteq \Psi ^+$ and $\Delta \subseteq \Psi ^-$ be finite such that $\bigwedge \Gamma \to \bigvee \Delta $ is derivable. Using (NR2) and (N4) we see that $\circ \bigwedge \Gamma \to \circ \bigvee \Delta $ is derivable, which in view of Lemma 3.5 implies that $ \bigwedge \circ \Gamma \to \bigvee \circ \Delta $ is derivable as well. But $\circ \Gamma \subseteq \Phi ^+$ and $\circ \Delta \subseteq \Phi ^-$ , contradicting the fact that $\Phi $ is consistent. We conclude that $\Psi \in |{\mathfrak M}_\Lambda |$ .

We must now check that $\Phi \mathrel S_T \Psi $ . It is clear that clauses (1) and (2) of Definition 4.6 hold. If $\Diamond \varphi \in \Phi ^+$ (so that $\Diamond $ is allowed in $\mathcal L$ ) and $\varphi \not \in \Phi ^+$ , it follows that $\varphi \in \Phi ^-$ . By Lemma 3.6 $\Diamond \varphi \to \varphi \vee \circ \Diamond \varphi $ is derivable, so we cannot have that $\circ \Diamond \varphi \in \Phi ^-$ and hence $\circ \Diamond \varphi \in \Phi ^+$ , so that $\Diamond \varphi \in \Psi ^+$ . Similarly, if $\Diamond \varphi \in \Phi ^-$ we have that $\circ \Diamond \varphi \in \Phi ^-$ , for otherwise we obtain a contradiction from (E1). Therefore, $\Diamond \varphi \in \Psi ^-$ as well. The clauses for $\forall \varphi $ follow a similar line of reasoning using (UA6).

To check that $\Psi $ is unique, suppose that $\Theta \in |{\mathfrak M}_\Lambda |$ is such that $\Phi \mathrel S_\Lambda \Theta $ . Then, if $\varphi \in \Psi ^+$ it follows from the definition of $\mathrel S_T$ that $\circ \varphi \in \Phi ^+$ and hence $\varphi \in \Theta ^+$ ; by the same argument, if $\varphi \in \Psi ^-$ it follows that $\varphi \in \Theta ^-$ , and hence $\Theta = \Psi $ .

Continuity: Now that we have shown that $S_\Lambda $ is a function, we may treat it as such. Suppose that $\Phi \preccurlyeq _\Lambda \Psi $ ; we must check that $S_\Lambda (\Phi ) \preccurlyeq _\Lambda S_\Lambda (\Psi )$ . Let $\varphi \in S^+_\Lambda (\Phi )$ . Using the definition of $\mathrel S_T$ , we have that $\circ \varphi \in \Phi ^+$ ; hence $\circ \varphi \in \Psi ^+ $ and thus $\varphi \in S_\Lambda ^+(\Psi )$ . By a similar argument, if $\varphi \in S_\Lambda ^-(\Psi )$ , it follows that $ \varphi \in S_\Lambda ^-(\Phi )$ . Since $\varphi \in S_\Lambda (\Phi )$ was arbitrary we obtain $S^+_\Lambda (\Phi ) \preccurlyeq _\Lambda S^+_\Lambda (\Psi )$ , as needed.

Openness: Suppose that (N5) is an axiom of $\Lambda $ and $\Psi \succcurlyeq _\Lambda S_\Lambda (\Phi )$ . We claim that $\Theta ' : = ( \circ \Psi ^+ \cup \Phi ^+, \circ \Psi ^-)$ is consistent. If not, there are finite $\Xi \subseteq \Psi ^+ $ , $\Gamma \subseteq \Phi ^+$ , and $ \Delta \subseteq \Psi ^-$ such that $\vdash \bigwedge \circ \Xi \wedge \bigwedge \Gamma \to \bigvee \circ \Delta $ . Since $\Gamma \subseteq \Phi ^+$ , this yields $ \bigwedge \circ \Xi \to \bigvee \circ \Delta \in \Phi ^+$ . Using Lemma 3.5, (N5), and propositional reasoning, this gives us $\circ \left ( \bigwedge \Xi \to \bigvee \Delta \right ) \in \Phi ^+$ ; hence $\bigwedge \Xi \to \bigvee \Delta \in \Psi ^+$ . But then $\bigwedge \Xi \wedge \left ( \bigwedge \Xi \to \bigvee \Delta \right ) \to \bigvee \Delta $ would be an intuitionistic tautology witnessing that $\Psi $ is inconsistent, contrary to our assumption. We conclude that $\Theta ' $ is consistent; hence it can be extended to a prime type $\Theta $ using the Lindenbaum lemma, and clearly $\Phi \preccurlyeq _\Lambda \Theta \mathrel S_\Lambda \Psi $ , as required.⊣

Proof. We need for the following three properties to hold: 1. $(|{\mathfrak M}_\Lambda |,{\preccurlyeq }_\Lambda ,\ell _\Lambda )$ is a labelled poset; 2. $S_\Lambda $ is a sensible forward-confluent function; and3. $\ell _\Lambda $ has $T_{ \mathcal L }$ as its codomain. The first item is Lemma 5.4. That $S_\Lambda $ is a forward-confluent function is Lemma 5.5, and it is sensible since $\Phi \mathrel S_\Lambda \Psi $ precisely when $\Phi \mathrel S_T \Psi $ . Finally, if $\Phi \in |{\mathfrak M}_\Lambda |$ then $\ell _\Lambda (\Phi ) = \Phi $ , which is an element of $T_{ \mathcal L }$ by Lemma 5.2.⊣

Proof. Let $\Lambda $ be either ${\sf ITL}_{{\circ } }$ or ${\sf ITL}^{+}_{{\circ } }$ . By Lemma 5.3, if $\Lambda \not \vdash \varphi $ then there is $\Phi \in |{\mathfrak M}_\Lambda |$ such that $\varphi \in \Phi ^-$ . By Proposition 5.6 ${\mathfrak M}_\Lambda $ is a deterministic, weak quasimodel falsifying $\varphi $ , and moreover it is trivially $\omega $ -sensible as $\Diamond $ is not in our language. By Lemma 4.8, $\varphi $ is not valid in the class of expanding posets, as required. In the case that $\Lambda = {\sf ITL}^{+}_{{\circ } }$ , we additionally use the fact that $S_\Lambda $ is open, so that ${\mathfrak M}_\Lambda $ is persistent.⊣

Proof. Each claim is proved by backward induction on $\preccurlyeq $ .

(1) Let us first consider the base case, when there is no $v \succ w$ . Assume that ${\textrm{Sim}}({w}) \in \ell ^-(x)$ . From the definition of labelled poset $\bigwedge \ell _{\mathfrak {A}}^+(w) \in \ell _{\mathfrak {X}}^+(y)$ and $\bigvee \ell _{\mathfrak {A}}^-(w) \in \ell _{\mathfrak {X}}^-(y)$ for some $y \succcurlyeq x$ . From the definition of type it follows that $\ell _{\mathfrak {A}}^+(w) \subseteq \ell _{\mathfrak {X}}^+(y)$ and $\ell _{\mathfrak {A}}^-(w) \subseteq \ell _{\mathfrak {X}}^-(y)$ , so that $\ell _{\mathfrak {A}}(w) \subseteq _{T} \ell _{\mathfrak {X}}(y)$ . It follows that ${\mathrel E} \stackrel {\textrm {def}}{=} \lbrace (w, y)\rbrace $ is a simulation, so $(\mathfrak A, w) \rightharpoonup ({\mathfrak X}, y )$ .

For the inductive step, let us assume that the lemma holds for all $v \succ w$ . Assume that ${\textrm{Sim}}({w}) \in \ell _{\mathfrak {X}}^-(x)$ . From the definition of labelled poset, it follows that $\bigwedge \ell _{\mathfrak {A}}^+(w) \in \ell _{\mathfrak {X}}^+(y)$ , $\bigvee \ell _{\mathfrak {A}}^-(w) \in \ell _{\mathfrak {X}}^-(y)$ , and $\bigvee _{v \prec w} {\textrm{Sim}}({v}) \in \ell _{\mathfrak {X}}^-(y)$ for some $y \succcurlyeq x$ . Following similar reasoning as in the base case we can conclude that $\ell _{\mathfrak {A}}(w) \subseteq \ell _{\mathfrak {X}}(y)$ , and moreover, that ${\textrm{Sim}}({v}) \in \ell _{\mathfrak {X}}^-(y)$ for all $v \succ w$ . By induction hypothesis we conclude that for all $v \succ w$ , there exists a simulation $\mathrel E_{v}$ such that $v \mathrel E_{v} z_{v}$ for some $z_{v} \succcurlyeq y$ . Let ${\mathrel E} \stackrel {\textrm {def}}{=} \lbrace (w, y) \rbrace \cup \bigcup \limits _{v \succ w} \mathrel E_{v}$ . The reader may check that $\mathrel E$ is a simulation and that $w \mathrel E y \succcurlyeq x$ , so that $(\mathfrak A,w) \rightharpoonup ({\mathfrak X}, y)$ , as needed.

(2) For the base case, assume that $(\mathfrak A,w) \rightharpoonup (\mathfrak X, y)$ for some $y \succcurlyeq x$ , so there exists a simulation $\mathrel E$ such that $w \mathrel E y $ . It follows that $\ell _{\mathfrak {A}}^+(w) \subseteq \ell _{\mathfrak {X}}^+(y)$ and $\ell _{\mathfrak {A}}^-(w) \subseteq \ell _{\mathfrak {X}}^-(y)$ . From conditions 3 and 5 of the definition of type (Definition 4.1), it follows that $\bigwedge \ell _{\mathfrak {A}}^+(w) \not \in \ell _{\mathfrak {X}}^-(y)$ and $\bigvee \ell _{\mathfrak {A}}^-(w) \not \in \ell _{\mathfrak {X}}^+(y)$ . But then, condition 7 gives us ${\textrm{Sim}}({w}) \not \in \ell _{\mathfrak {X}}^+(y)$ , so ${\textrm{Sim}}({w}) \not \in \ell _{\mathfrak {X}}^+(x)$ .

For the inductive step, by the same reasoning as in the base case it follows that $\bigwedge \ell _{\mathfrak {A}}^+(w) \not \in \ell _{\mathfrak {X}}^-(y)$ and $\bigvee \ell _{\mathfrak {A}}^-(w) \not \in \ell _{\mathfrak {X}}^+(y)$ . Now, let v be such that $v \succ w$ . Since $\mathrel E$ is forward confluent then $v \mathrel E z_{v}$ for some $z_{v} \succcurlyeq y$ . By induction hypothesis, ${\textrm{Sim}}({v}) \not \in \ell ^+(z_{v})$ , so ${\textrm{Sim}}({v}) \not \in \ell ^+(y)$ . Since v was arbitrary we conclude that $\bigvee _{v \succ w} {\textrm{Sim}}({v}) \not \in \ell ^+(y)$ . Finally, from condition 7 of Definition 4.1 and the fact that $y \preccurlyeq x$ we get that ${\textrm{Sim}}({w}) \not \in \ell ^+(x)$ .⊣

Proof. (1) First assume that $\psi \in \ell ^- ({w})$ , and toward a contradiction that $\nvdash \psi \to {\textrm{Sim}}({{w}})$ . Recall that ${\mathfrak M}_\Lambda $ denotes the canonical model for $\Lambda $ . By the Lindenbaum lemma there is $\Gamma \in | {\mathfrak M}_\Lambda | $ such that $\psi \to {\textrm{Sim}}({{w}}) \in \Gamma ^-$ . Thus for some $\Theta \succcurlyeq _\Lambda \Gamma $ we have that $\psi \in \Theta ^+$ and ${\textrm{Sim}}({{w}}) \in \Theta ^-$ . But then by Proposition 6.4 we have that $(\mathfrak I,{w}) \rightharpoonup ({\mathfrak M}_\Lambda ,\Delta )$ for some $\Delta \succcurlyeq _\Lambda \Theta $ , so that $\psi \in \Delta ^-$ , and by monotonicity $\psi \in \Theta ^-$ , contradicting the consistency of $\Theta $ .

(2) If $\psi \in \ell ^+ ({w})$ , we proceed similarly. Assume toward a contradiction that $\nvdash \big ( \psi \to {\textrm{Sim}}({{w}}) \big ) \to {\textrm{Sim}}({w})$ . Then, reasoning as above there is $\Theta \in |{\mathfrak M}_\Lambda |$ such that $\psi \to {\textrm{Sim}}({{w}}) \in \Theta ^+$ and ${\textrm{Sim}}({w}) \in \Theta ^-$ . From Proposition 6.4 we see that there is $\Delta \succcurlyeq _c \Theta $ such that $(\mathfrak I,w) \rightharpoonup ({\mathfrak M}_\Lambda ,\Delta )$ , so that $\psi \in \Delta ^+$ and, once again by Proposition 6.4, ${\textrm{Sim}}({w}) \in \Delta ^-$ . It follows that $\psi \to {\textrm{Sim}}({w}) \not \in \Delta ^+$ ; but in view of upward persistence, this contradicts that $\psi \to {\textrm{Sim}}({{w}}) \in \Theta ^+$ .

(3) Suppose that ${v}\succcurlyeq {w}$ . Reasoning as above, it suffices to show that if $\Gamma \in |{\mathfrak M}_\Lambda |$ is such that ${\textrm{Sim}}({{w}}) \in \Gamma ^-$ , then also ${\textrm{Sim}}({{v}}) \in \Gamma ^-$ . But if ${\textrm{Sim}}({{w}}) \in \Gamma ^-$ , there is $\Theta \succcurlyeq _\Lambda \Gamma $ such that $(\mathfrak I_{ },w) \rightharpoonup ({\mathfrak M}_\Lambda , \Theta )$ . By forward confluence $(\mathfrak I_{ },v) \rightharpoonup ({\mathfrak M}_\Lambda , \Delta )$ for some $\Delta \succcurlyeq _\Lambda \Theta $ . Thus by Proposition 6.4, ${\textrm{Sim}}({v}) \in \Delta ^-$ and by upwards persistence ${\textrm{Sim}}({v}) \in \Gamma ^-$ . Since $\Gamma \in |{\mathfrak M}_\Lambda | $ was arbitrary, the claim follows.

(4) We prove that if $\Gamma \in |{\mathfrak M}_\Lambda |$ is such that

(1) $$ \begin{align} \bigwedge _{\psi\in \ell^- ({{w}})} \textrm{Sim}({{w}}) \in \Gamma ^+, \end{align} $$

then $\psi \in \Gamma ^+$ . If (1) holds then by Theorem 7.1, there is ${w} \in |\mathfrak I_{ }|$ with $(\mathfrak I_{ }, w) \rightharpoonup ({\mathfrak M}_\Lambda ,\Gamma )$ . By Proposition 6.4, ${\textrm{Sim}}({w}) \in \Gamma ^-$ , and hence it follows from (1) that $\psi \not \in \ell ^- ({{w}})$ , but $\mathfrak I_{ }$ is saturated and $\psi \in \Sigma $ , so $\psi \in \ell ^+ ({{w}})$ and thus $\psi \in \Gamma ^+$ , as required.

(5) Suppose that $\Gamma \in |{\mathfrak M}_\Lambda |$ is such that

(2) $$ \begin{align} \circ\bigwedge _{{{w}} \mathrel S_{\mathfrak I_{ }} {{{v}}} }{\textrm{Sim}}({{{v}}}) \in \Gamma^+ , \end{align} $$

and assume toward a contradiction that ${\textrm{Sim}}({{w}}) \in \Gamma ^-$ . By Proposition 6.4 $(\mathfrak I_{ }, w) \rightharpoonup ({\mathfrak M}_\Lambda ,\Delta )$ for some $\Delta \succcurlyeq _\Lambda \Gamma $ . Since $\rightharpoonup $ is a dynamic simulation, it follows that there is $v \in |\mathfrak I_{ }|$ with ${w} \mathrel S_{\mathfrak I_{ }} v$ and $(\mathfrak I_{ }, v) \rightharpoonup \big ( {\mathfrak M}_\Lambda , S_\Lambda (\Delta ) \big ) $ , so that $\textrm{Sim}(v) \in \big ( S_\Lambda (\Delta ) \big ) ^-$ . It follows that $\circ \textrm{Sim}(v) \in \Gamma ^-$ , since $S_\Lambda $ is sensible and $\Gamma $ is saturated. But $\Delta \succcurlyeq _\Lambda \Gamma $ , so that $\circ {\textrm{Sim}}({v}) \in S^-_\Lambda (\Gamma )$ as well, contradicting (2).⊣

Proof. To check that $|{\mathfrak I}^\blacklozenge _{ }|$ is upward closed, let ${{w}}\in |{\mathfrak I}^\blacklozenge _{ }|$ and suppose ${{{v}}}\succcurlyeq {{w}}$ . Now, by Proposition 7.3 (3), we have that $\vdash \textrm{Sim}({{{v}}})\to \textrm{Sim}({{w}})$ ; hence if ${{w}}$ is possible, so is ${{{v}}}$ . To see that $S_{{\mathfrak I}^\blacklozenge _{ } }$ is serial, observe that by Proposition 7.3 (5), if ${{w}}\in |{\mathfrak I}^\blacklozenge _{ }| \subseteq |\mathfrak I_{ }|$ , $\vdash \circ \bigwedge _{{{w}}\mathrel S_{\mathfrak I_{ }} {{{v}}} }\textrm{Sim}({{{v}}}) \to \textrm{Sim}({{w}})$ . Since ${{w}}$ is possible, it follows that for some ${{{v}}}$ with ${{w}} \mathrel S_{\mathfrak I_{ }} {{{v}}}$ , ${{{v}}}$ is possible as well, for otherwise $\circ \bigwedge _{{{w}}\mathrel S_{\mathfrak I_{ }} {{{v}}} }\textrm{Sim}({{{v}}})$ would be equivalent to $\circ \top $ , allowing us to deduce $\textrm{Sim}({{w}})$ . But then ${{{v}}}\in |{\mathfrak I}^\blacklozenge _{ }|$ , as needed.⊣

Proof. Let $\mathfrak I_{ } = \mathfrak I_{ \Sigma }$ . By Proposition 7.3 (5) we have that, for all ${{{v}}}\in {R}({{w}})$ ,

$$ \begin{align*}\vdash \circ\bigwedge\limits_{{{{v}}} \mathrel S_{\mathfrak I_{ }} u }\mathrm{Sim}(u) \to \mathrm{Sim}({{{v}}}).\end{align*} $$

Now, if $u\not \in |{\mathfrak I}^\blacklozenge _{ \Sigma }|$ , then $\vdash \mathrm{Sim}(u)$ ; hence by (NR2) we have $\vdash \circ \mathrm{Sim}(u)$ , and we can remove ${\mathrm{Sim}}({u})$ from the conjunction using Lemma 3.5 and propositional reasoning. Since ${{{v}}} \in R(w)$ was arbitrary, this shows that

$$ \begin{align*}\vdash \circ \bigwedge\limits_{w \mathrel R v}\mathrm{Sim}({{{v}}})\to \bigwedge \limits_{w \mathrel R v}\mathrm{Sim}({{{v}}}).\\[-38pt] \end{align*} $$

⊣

Proof. Towards a contradiction, assume that ${{w}}\in {\textrm {Poss}}_{\Sigma }$ and $\Diamond \psi \in \ell ^+ ({{w}})$ but, for all ${{{v}}}\in {R}({{w}})$ , $\psi \in \ell ^-({{w}})$ . By Lemma 8.1, $\vdash \circ \bigwedge \limits _{w \mathrel R v} \mathrm{Sim}({{{v}}})\to \bigwedge \limits _{w \mathrel R v} \mathrm{Sim}({{{v}}})$ . By the $\Diamond $ -induction Rule (ER2), $\vdash \Diamond \bigwedge \limits _{w\mathrel Rv}\mathrm{Sim}({{{v}}})\to \bigwedge \limits _{w\mathrel Rv}\mathrm{Sim}({{{v}}})$ ; in particular,

(3) $$ \begin{align} \vdash \Diamond \bigwedge _{w\mathrel Rv}\mathrm{Sim}({{{v}}})\to \mathrm{Sim}({{w}}). \end{align} $$

Now let ${{{v}}}\in {R}({{w}})$ . By Proposition 7.3 (1) and the assumption that $\psi \in \ell ^-({{{v}}})$ we have that $\vdash \psi \to \mathrm{Sim}({{{v}}}) $ , and since ${{{v}}}$ was arbitrary, $\vdash \psi \to \bigwedge _{w\mathrel Rv}\mathrm{Sim}({{{v}}}) $ . Using distributivity (ER1) we further have that $\vdash \Diamond \psi \rightarrow \Diamond \bigwedge _{w\mathrel Rv}\mathrm{Sim}({{{v}}})$ . This, along with (3), shows that $\vdash \Diamond \psi \to \mathrm{Sim}({{w}})$ ; however, by Proposition 7.3 (2) and our assumption that $\Diamond \psi \in \ell ^+ ({{w}})$ we have that $\vdash \big ( \Diamond \psi \to \mathrm{Sim}({{w}}) \big ) \to {\mathrm{Sim}}({w})$ ; hence by modus ponens we obtain $\vdash \mathrm{Sim}({{w}}),$ which contradicts the assumption that ${{w}}\in {\textrm {Poss}}_{\Sigma }$ . We conclude that there can be no such ${{w}}$ .⊣

Proof. Let ${\mathfrak I}^\blacklozenge _{ } = {\mathfrak I}^\blacklozenge _{ \Sigma }$ . By Lemma 7.8, $|{\mathfrak I}^\blacklozenge _{ }|$ is upwards closed in $|\mathfrak I_{ \Sigma }|$ and $S_{{\mathfrak I}^\blacklozenge _{ }}$ is serial, while by Proposition 8.2, $S_{{\mathfrak I}^\blacklozenge _{ }}$ is $\omega $ -sensible. It follows from Lemma 4.11 that ${\mathfrak I}^\blacklozenge _{ }$ is a quasimodel.⊣

Proof. We prove the contrapositive. Suppose $\varphi $ is an unprovable formula and let

$$ \begin{align*}W=\left \{ {{w}}\in\mathfrak I_{ {\textrm{sub}}(\varphi) }:\varphi\in \ell^- ({{w}})\right \}.\end{align*} $$

Then, by Proposition 7.3 (4) we have that $\vdash \bigwedge _{{w} \in W} \mathrm{Sim}({{w}}) \rightarrow \varphi $ ; since $\varphi $ is unprovable, it follows that some ${{w}}^\ast \in W$ is possible and hence ${{w}}^\ast \in {\textrm {Poss}}_{{\textrm {sub}}(\varphi )}$ . By Corollary 8.3, ${\mathfrak I}^\blacklozenge _{ {\textrm {sub}}(\varphi ) }$ is a quasimodel, so that by Theorem 4.9, $\varphi $ is falsifiable in some dynamical system.⊣

Proof. It can be checked using universal excluded middle (UA1) that $|{\mathfrak M}_\Lambda [\Pi ]|$ is open and using (UA6) that it is $S_\Lambda $ -invariant. In view of Lemma 10.9, we may moreover conclude that ${\mathfrak M}_\Lambda [\Pi ]$ is a weak quasimodel.

It remains to show that ${\mathfrak M}_\Lambda [\Pi ]$ is honest. That $\forall \varphi \in \Phi ^+ \cap \Sigma $ implies that $\varphi \in \Psi ^+$ for all $\Phi ,\Psi \in |{\mathfrak M}_\Lambda [\Pi ]|$ follows readily from the truth Axiom (UA4). For the remaining condition, let us take $ \Phi \in |{\mathfrak M}_\Lambda [\Pi ]|$ and let $\forall \varphi \in \Sigma $ be such that $\forall \varphi \in \Phi ^- $ . Let $\Psi ' = ( \Pi ^+ , \lbrace \varphi \rbrace \cup \Pi ^-)$ . Assume towards a contradiction that $\Psi '$ is not consistent, so that $\vdash \bigwedge \Pi ^+ \rightarrow \varphi \vee \bigvee \Pi ^- $ . By Rule (UR1), $\vdash \forall \left (\bigwedge \Pi ^+ \rightarrow \varphi \vee \bigvee \Pi ^- \right )$ . By Axiom (UA2), $\vdash \forall \bigwedge \Pi ^+ \rightarrow \forall \left ( \varphi \vee \bigvee \Pi ^- \right )$ . From $\Phi _\forall = \Pi $ , Axioms (UA5) and (UA2), and propositional reasoning we conclude that $\vdash \bigwedge \Pi ^+ \to \forall \bigwedge \Pi ^+ $ ; hence $\vdash \bigwedge \Pi ^+ \to \forall \left (\varphi \vee \bigvee \Pi ^- \right ) $ . By several applications of Axiom (UA3), $\vdash \forall \left ( \varphi \vee \bigvee \Pi ^-\right ) \to \forall \varphi \vee \bigvee \Pi ^-$ ; hence $\vdash \bigwedge \Pi ^+ \to \forall \varphi \vee \bigvee \Pi ^-$ , which since $\forall \varphi \in \Pi ^- \subseteq \Phi ^- $ implies that $\Phi $ is inconsistent, a contradiction.

Hence $\Psi '$ is consistent. By Lemma 5.3, $\Psi '$ can be extended to a prime type $ \Psi $ . Since, by construction, $\Pi \subseteq _T \Psi $ , we have that $\Psi \in |{\mathfrak M}_\Lambda [\Pi ]|$ and, moreover, $\varphi \in \Psi ^-$ , as required.⊣

Proof. Let ${\mathfrak I}^\blacklozenge _{ } = {\mathfrak I}^\blacklozenge _{ \Sigma }$ . If $ w \in |{\mathfrak I}^\blacklozenge _{ }[\Pi ]|$ , by Lemma 7.5 there is $\Gamma \in |{\mathfrak M}_\Lambda |$ with $ w \rightharpoonup \Gamma $ , and by label-preservation $\Pi \subseteq _T \Gamma $ , so that $\Gamma \in |{\mathfrak M}_\Lambda [\Pi ]|$ . Hence $\rightharpoonup $ is total. Conversely, if $\Gamma \in | {\mathfrak M}_\Lambda [\Pi ]|$ , then by Theorem 7.1 there is $w\in |\mathfrak I_{ \Sigma }|$ such that $ w \rightharpoonup \Gamma $ , and once again by label-preservation $w \in |{\mathfrak I}^\blacklozenge _{ } [\Pi ]|$ .

To see that ${\mathfrak I}^\blacklozenge _{ } [\Pi ]$ is a quasimodel, in view of Lemma 4.11, it suffices to show that $|{\mathfrak I}^\blacklozenge _{ }[\Pi ]|$ is open and $S_{{\mathfrak I}^\blacklozenge _{ }}$ -invariant. However, if $ w \in |{\mathfrak I}^\blacklozenge _{ }[\Pi ]|$ , then since $ \rightharpoonup $ is total we have that there is $\Gamma \in |{\mathfrak M}_\Lambda [\Pi ]|$ with $ w \rightharpoonup \Gamma $ . By Lemma 9.3 $|{\mathfrak M}_\Lambda [\Pi ]|$ is open; hence by continuity there is $\Delta \in |{\mathfrak M}_\Lambda [\Pi ]|$ such that $ v \rightharpoonup \Delta $ , and once again by label-preservation this shows that $\Pi \subseteq _T \ell (v) $ , so that $v\in |{\mathfrak I}^\blacklozenge _{ }[\Pi ]|$ . That $|{\mathfrak I}^\blacklozenge _{ }[\Pi ]|$ is $S_{{\mathfrak I}^\blacklozenge _{ }}$ -invariant is immediate from conditions (5) and (6) of Definition 4.6 and the fact that $S_{{\mathfrak I}^\blacklozenge _{ }}$ is sensible.⊣

Proof. If $\varphi $ is unprovable, then $\varphi \in \Phi ^-$ for some $\Phi \in |{\mathfrak M}_\Lambda |$ , and by Theorem 7.1, there is some $w\in |{\mathfrak I}^\blacklozenge _{ \Sigma }|$ such that $({\mathfrak I}^\blacklozenge _{ \Sigma }, w) \rightharpoonup ({\mathfrak M}_\Lambda , \Phi )$ . Let $\Pi = (\ell (w))_\forall $ . Then, ${\mathfrak M}_\Lambda [\Pi ]$ is an honest weak quasimodel, so that by Lemmas 9.5 and 9.6, so is ${\mathfrak I}^\blacklozenge _{ \Sigma }[\Pi ]$ . It follows by Theorem 4.9 that $\varphi $ is falsifiable on some dynamic topological model.⊣

Proof. To prove item 1, it is sufficient to check that the conditions of Definition 4.1 hold. Conditions 1 and 2 of Definition 4.1 are straightforward. Since , conditions 4 and 6 clearly hold. For condition 7, suppose that . Since $\Sigma $ is closed under subformulas, $\varphi , \psi \in \Sigma $ and, since $\Psi $ is a type it follows that either $\varphi \in \Psi ^-$ or $\psi \in \Psi ^+$ . By definition either $\varphi \in \Psi ^-$ or $\psi \in \Psi ^+ \cap \Sigma $ . The proofs for conditions 3 and 5 of Definition 4.1 are similar and left to the reader.

For item 2 of the lemma, it suffices to observe that $ \sqsubseteq _T $ is a refinement of $ \preccurlyeq _{T} $ , and that $\preccurlyeq _{T}$ is already transitive.

For item 3, note that $\Gamma ^-=\Phi ^-$ and $\Gamma ^+=\Phi ^+\cap \Delta $ for some $\Delta $ closed under subformulas. We must check that each condition of Definition 4.6 holds. As an example, we work out (3). If $\Diamond \psi \in \Gamma ^+$ , since ${\textrm {sub}}(\Gamma ^+) \subseteq \Sigma $ then $\Diamond \psi , \psi \in \Sigma $ . From $\Gamma \sqsubseteq _T \Phi \mathrel S_T\Psi $ we conclude that $\Diamond \psi \in \Phi ^+$ , and either $\psi \in \Phi ^+$ or $\Diamond \psi \in \Psi ^+$ . In the first case, we note that $\Diamond \psi \in \Gamma ^+$ yields $\psi \in \Delta $ ; hence $\psi \in \Phi ^+\cap \Delta = \Gamma ^+$ . In the second, $\Diamond \psi \in \Psi ^+ \cap \Sigma $ , which means that . Other conditions follow similar reasoning and are left to the reader.