Let $\mathcal{C}$ be the class of all sets $S$ such that $S$ is downward closed ($x \in S \to x \subseteq S$) and $(S, \in)$ is a model of ZFC (where $\in$ is set membership). Define the Kripke relation $\succ$ on $\mathcal{C}$ by $$ S_1 \succ S_2 \quad \text{if} \quad S_2 \in S_1. $$ Also let $\nu$ be an arbitrary mapping from propositional variables $p, q, \ldots$ to formulas of set theory, and say that $p$ is true at $S$ if $(S, \in)$ satisfies $\nu(p)$.

Then I claim $(\mathcal{C}, \succ, \nu)$ is a Kripke model for Gödel-Löb provability logic (GL). This is trivially true because GL corresponds to the frame condition "no infinite descending chains", and $\succ$ has no such chains $S_1 \succ S_2 \succ S_3 \succ \ldots$ because sets are well-founded. What's more interesting is that the provability modal $\square$ seems to correspond to provability "at $S$" in some sense: $\square A$ holds in the world $S$ iff $A$ holds in all models of ZFC that are elements of $S$. which by completeness of first-order-logic is another way of saying $A$ is provable according to $S$. For example, inconsistency $\square \bot$ holds exactly in models $S$ which contain no models of ZFC.

But I'd like to show $\mathcal{C}$ is not just a Kripke model of GL, but satisfies exactly the formulas true in GL, i.e., it is a canonical Kripke model. Precisely:

Question: is $(\mathcal{C}, \succ, \nu)$ a canonical Kripke model of GL, for some choice of $\nu$?

Of course, ZFC is not enough to resolve this -- ZFC cannot even show that there is a single model in $\mathcal{C}$, as this is equivalent to Con(ZFC). So the question is if we assume Con(ZFC) or some other sufficiently strong cardinal axiom, whether we get a canonical Kripke model for GL.

Let $\mathcal{C}$ be the class of all transitive models of ZFC, i.e., sets $S$ such that $S$ is downward closed ($x \in S \to x \subseteq S$) and $(S, \in)$ is a model of ZFC (where $\in$ is set membership). Define the Kripke relation $\succ$ on $\mathcal{C}$ by $$ S_1 \succ S_2 \quad \text{if} \quad S_2 \in S_1. $$ Also let $\nu$ be an arbitrary mapping from propositional variables $p, q, \ldots$ to formulas of set theory, and say that $p$ is true at $S$ if $(S, \in) \vDash \nu(p)$.

Then I claim $(\mathcal{C}, \succ, \nu)$ is a Kripke model for Gödel-Löb provability logic (GL). This is trivially true because GL corresponds to the frame condition "no infinite descending chains", and $\succ$ has no such chains $S_1 \succ S_2 \succ S_3 \succ \ldots$ because sets are well-founded. What's more interesting is that the provability modal $\square$ seems to correspond to provability "at $S$" in some sense: $\square A$ holds in the world $S$ iff $A$ holds in all models of ZFC that are elements of $S$. which by completeness of first-order-logic is another way of saying $A$ is provable according to $S$. For example, inconsistency $\square \bot$ holds exactly in models $S$ which contain no models of ZFC.

But I'd like to show $\mathcal{C}$ is not just a Kripke model of GL, but satisfies exactly the formulas true in GL, i.e., it is a canonical Kripke model. Precisely:

Question: is $(\mathcal{C}, \succ, \nu)$ a canonical Kripke model of GL, for some choice of $\nu$?

Of course, ZFC is not enough to resolve this -- ZFC cannot even show that there is a single model in $\mathcal{C}$, as this is equivalent to Con(ZFC). So the question is if we assume Con(ZFC) or some other sufficiently strong cardinal axiom, whether we get a canonical Kripke model for GL.

Let $\mathcal{C}$ be the class of all sets $S$ such that $(S, \in)$ is a model of ZFC (where $\in$ is set membership), and define the Kripke relation $\succ$ on $\mathcal{C}$ by $$ S_1 \succ S_2 \quad \text{if} \quad S_2 \in S_1. $$ Also let $\nu$ be an arbitrary mapping from propositional variables $p, q, \ldots$ to formulas of set theory, and say that $p$ is true at $S$ if $(S, \in)$ satisfies $\nu(p)$.

Then I claim $(\mathcal{C}, \succ, \nu)$ is a Kripke model for Gödel-Löb provability logic (GL). This is trivially true because GL corresponds to the frame condition "no infinite descending chains", and $\succ$ has no such chains $S_1 \succ S_2 \succ S_3 \succ \ldots$ because sets are well-founded. What's more interesting is that the provability modal $\square$ seems to correspond to provability "at $S$" in some sense: $\square A$ holds in the world $S$ iff $A$ holds in all models of ZFC that are elements of $S$. which by completeness of first-order-logic is another way of saying $A$ is provable according to $S$. For example, inconsistency $\square \bot$ holds exactly in models $S$ which contain no models of ZFC.

But I'd like to show $\mathcal{C}$ is not just a Kripke model of GL, but satisfies exactly the formulas true in GL, i.e., it is a canonical Kripke model. Precisely:

Question: is $(\mathcal{C}, \succ, \nu)$ a canonical Kripke model of GL, for some choice of $\nu$?

Of course, ZFC is not enough to resolve this -- ZFC cannot even show that there is a single model in $\mathcal{C}$, as this is equivalent to Con(ZFC). So the question is if we assume Con(ZFC) or some other sufficiently strong cardinal axiom, whether we get a canonical Kripke model for GL.

Let $\mathcal{C}$ be the class of all sets $S$ such that $S$ is downward closed ($x \in S \to x \subseteq S$) and $(S, \in)$ is a model of ZFC (where $\in$ is set membership). Define the Kripke relation $\succ$ on $\mathcal{C}$ by $$ S_1 \succ S_2 \quad \text{if} \quad S_2 \in S_1. $$ Also let $\nu$ be an arbitrary mapping from propositional variables $p, q, \ldots$ to formulas of set theory, and say that $p$ is true at $S$ if $(S, \in)$ satisfies $\nu(p)$.

Then I claim $(\mathcal{C}, \succ, \nu)$ is a Kripke model for Gödel-Löb provability logic (GL). This is trivially true because GL corresponds to the frame condition "no infinite descending chains", and $\succ$ has no such chains $S_1 \succ S_2 \succ S_3 \succ \ldots$ because sets are well-founded. What's more interesting is that the provability modal $\square$ seems to correspond to provability "at $S$" in some sense: $\square A$ holds in the world $S$ iff $A$ holds in all models of ZFC that are elements of $S$. which by completeness of first-order-logic is another way of saying $A$ is provable according to $S$. For example, inconsistency $\square \bot$ holds exactly in models $S$ which contain no models of ZFC.

But I'd like to show $\mathcal{C}$ is not just a Kripke model of GL, but satisfies exactly the formulas true in GL, i.e., it is a canonical Kripke model. Precisely:

Question: is $(\mathcal{C}, \succ, \nu)$ a canonical Kripke model of GL, for some choice of $\nu$?

Of course, ZFC is not enough to resolve this -- ZFC cannot even show that there is a single model in $\mathcal{C}$, as this is equivalent to Con(ZFC). So the question is if we assume Con(ZFC) or some other sufficiently strong cardinal axiom, whether we get a canonical Kripke model for GL.

Let $\mathcal{C}$ be the class of all sets $S$ such that $(S, \in)$ is a model of ZFC (where $\in$ is set membership), and define the Kripke relation $\succ$ on $\mathcal{C}$ by $$ S_1 \succ S_2 \quad \text{if} \quad S_2 \in S_1. $$ Also let $\nu$ be an arbitrary mapping from propositional variables $p, q, \ldots$ to formulas of set theory, and say that $p$ is true at $S$ if $(S, \in)$ satisfies $\nu(p)$.

Then I claim $(\mathcal{C}, \succ, \nu)$ is a Kripke model for Gödel-Löb provability logic (GL). This is trivially true because GL corresponds to the frame condition "no infinite descending chains", and $\succ$ has no such chains $S_1 \succ S_2 \succ S_3 \succ \ldots$ because sets are well-founded. What's more interesting is that the provability modal $\square$ seems to correspond to provability "at $S$" in some sense: $\square A$ holds in the world $S$ iff $A$ holds in all models of ZFC that are elements of $S$, which by completeness of first-order-logic is another way of saying $A$ is provable according to $S$. For example, inconsistency $\square \bot$ holds exactly in models $S$ which contain no models of ZFC.

But I'd like to show $\mathcal{C}$ is not just a Kripke model of GL, but satisfies exactly the formulas true in GL, i.e., it is a canonical Kripke model. Precisely:

Question: is $(\mathcal{C}, \succ, \nu)$ a canonical Kripke model of GL, for some choice of $\nu$?

Of course, ZFC is not enough to resolve this -- ZFC cannot even show that there is a single model in $\mathcal{C}$, as this is equivalent to Con(ZFC). So the question is if we assume Con(ZFC) or some other sufficiently strong cardinal axiom, whether we get a canonical Kripke model for GL.

Let $\mathcal{C}$ be the class of all sets $S$ such that $(S, \in)$ is a model of ZFC (where $\in$ is set membership), and define the Kripke relation $\succ$ on $\mathcal{C}$ by $$ S_1 \succ S_2 \quad \text{if} \quad S_2 \in S_1. $$ Also let $\nu$ be an arbitrary mapping from propositional variables $p, q, \ldots$ to formulas of set theory, and say that $p$ is true at $S$ if $(S, \in)$ satisfies $\nu(p)$.

Then I claim $(\mathcal{C}, \succ, \nu)$ is a Kripke model for Gödel-Löb provability logic (GL). This is trivially true because GL corresponds to the frame condition "no infinite descending chains", and $\succ$ has no such chains $S_1 \succ S_2 \succ S_3 \succ \ldots$ because sets are well-founded. What's more interesting is that the provability modal $\square$ seems to correspond to provability "at $S$" in some sense: $\square A$ holds in the world $S$ iff $A$ holds in all models of ZFC that are elements of $S$. which by completeness of first-order-logic is another way of saying $A$ is provable according to $S$. For example, inconsistency $\square \bot$ holds exactly in models $S$ which contain no models of ZFC.

But I'd like to show $\mathcal{C}$ is not just a Kripke model of GL, but satisfies exactly the formulas true in GL, i.e., it is a canonical Kripke model. Precisely:

Question: is $(\mathcal{C}, \succ, \nu)$ a canonical Kripke model of GL, for some choice of $\nu$?

Of course, ZFC is not enough to resolve this -- ZFC cannot even show that there is a single model in $\mathcal{C}$, as this is equivalent to Con(ZFC). So the question is if we assume Con(ZFC) or some other sufficiently strong cardinal axiom, whether we get a canonical Kripke model for GL.