4
$\begingroup$

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.

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ Your interpretation of completeness is wrong. Suppose $M$ is a minimal transitive model of ZFC, for example. Then $M$ thinks ZFC is consistent, but $M$ does not contain any model of ZFC in the sense of your post. This is because you're restricting attention to well-founded models. (And if you broaden this to allow ill-founded models as worlds, i.e. $S$ "sees" $S'$ iff $S'$ is "coded in" $S$ in some appropriate sense, then your argument for no-descending-chains breaks down.) $\endgroup$
    – Noah Schweber
    Commented Mar 19, 2023 at 20:58
  • 1
    $\begingroup$ On this theme, although no longer directly relevant to your question, the following is worth keeping in mind: if ZFC is consistent then it has a ${\bf 0'}$-computable (or even low) model, but no $\omega$-model of ZFC can even be hyperarithmetic under any circumstances. Meanwhile, if ZFC has an $\omega$-model then it has a "low-for-hyperjump" $\omega$-model, but no such well-founded model under any circumstances. So the gap between general models (to which completeness applies) and well-founded models (as in your post) is extremely large. $\endgroup$
    – Noah Schweber
    Commented Mar 19, 2023 at 21:06
  • $\begingroup$ @NoahSchweber, thanks! re: interpretation of completeness, you are right -- I thought that part might be fishy. And not just well-founded models, but those whose interpretation of $\in$ agrees with set membership in the metatheory. $\endgroup$
    – Caleb Stanford
    Commented Mar 19, 2023 at 21:50
  • 1
    $\begingroup$ Surprisingly, that part's not too bad: via Mostowski collapse, you can conflate "true membership relation" with "well-founded and 'locally set-like,'" where the latter is the condition that for all $x$ the collection of $y$ such that $y\varepsilon x$ is a set. But the general/well-founded issue is serious (and fun! :P). $\endgroup$
    – Noah Schweber
    Commented Mar 19, 2023 at 21:52
  • $\begingroup$ Good to know. Anyway, so that means this Kripke model is not really about provability in ZFC according to $M$, but about a weaker semantic notion, namely "lack of a concrete (and well-founded) counterexample at $M$" $\endgroup$
    – Caleb Stanford
    Commented Mar 19, 2023 at 22:00

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .