8
$\begingroup$

Kunen's inconsistency theorem is an important theorem in set theory on upper bounds for large cardinals.

It has long been thought to be able to be encoded on ZFC, but the full implementation has never appeared on Proof Assistant.

  • Lean has enough power to prove it. Because Lean's ground model is $pCIC + Choice$, which is sufficient to encode the Morse-Kelley set theory.
  • "There is no nontrivial $Σ_1$-elementary embedding $j : V \to V$" can be proved by $ZFC(j)$, But it cannot be proved axiom-free on $ZFC$.
  • The strength of "Metamath's ZFC + Metamath's class theory" is in the middle of $ZFC$ and $ZFC(j)$.

So can we prove Kunen's inconsistency theorem in Metamath without axioms?

Improve this question
$\endgroup$
1
  • $\begingroup$ @GuyCoder Whether a property can be proved axiom-free or not I think there can be a yes/no type answer. I do think we should have an [axiom-free] tag, but I don't have enough permissions... $\endgroup$
    – Ember Edison
    Commented Apr 15, 2022 at 10:19

1 Answer 1

Reset to default
8
$\begingroup$

The answer to this question is a tentative "yes", but it depends on how you interpret the resulting statement. From my understanding, there isn't anything about "elementary embedding" that would be a technical issue to express, so the only reason I can imagine that you say that it can't be proved in ZFC is because the statement involves a class quantification over $j$.

For a simple universal (or negated existential in this case) quantification over classes, Metamath (or more precisely set.mm) is perfectly capable of expressing these theorems. A simple example of a theorem over classes in set.mm is unass, $(\color{magenta}A\cup \color{magenta}B) \cup \color{magenta}C=\color{magenta}A\cup (\color{magenta}B \cup \color{magenta}C)$ which is true for all class terms $\color{magenta}A,\color{magenta}B,\color{magenta}C$.

In this case, the theorem would basically have the form:

$$\vdash(\color{magenta}J:V\longrightarrow V)\wedge \Sigma_1\mbox{-ElemEmbed}(\color{magenta}J)\to \color{magenta}J=\mbox{Id}\tag{*}$$

which has a free class variable $\color{magenta}J$. Although I have not attempted the proof, from what I can tell there should not be any technical limitations to proving this in set.mm with no additional axioms.

There are two competing semantics for these kinds of second order statements, and depending on which reading you take this may or may not be considered the "real" Kunen's theorem. The first reading takes all implicitly universally quantified class variables here as second order quantifiers over the universe. In that case, we are really talking about all subclasses of the universe, in which case this is really Kunen's theorem.

The second reading is that the quantifiers only range over definable classes. This is the reading we prefer when arguing that set.mm's axiom system is a conservative extension of ZFC: classes are really just a notational convenience for formulas with one free variable. In this case it's not really Kunen's theorem, because the desired elementary embedding is not necessarily definable. However, the existence of this theorem as stated means that if we did introduce an axiom like

$$\vdash(\mbox{Kunen}:V\longrightarrow V)\wedge \Sigma_1\mbox{-ElemEmbed}(\mbox{Kunen})\wedge \mbox{Kunen}\ne\mbox{Id}\tag{ax-Kunen}$$

then the elementary embedding would become definable (it is just $\mbox{Kunen}$) and we would be able to prove a contradiction using (*), so $\textsf{ZFC+ax-Kunen}\vdash \bot$ and (*) is the nearest equivalent to $\neg\textsf{ax-Kunen}$ that we can state and prove in $\textsf{ZFC}$.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ In order to express "elementary embedding", you have to be able to state $$ \color{blue}\varphi(\color{red}{x_1}, ... \color{red}{x_n}) \longleftrightarrow \color{blue}\psi(\color{magenta}J(\color{red}{x_1}), ... \color{magenta}J(\color{red}{x_n})) $$ I see how to do it for a fixed number of variables, but not for any number $n$ of variables. $\endgroup$
    – Thierry Arnoux
    Commented Apr 19, 2022 at 3:36
  • 1
    $\begingroup$ @ThierryArnoux It would be something like: for all set sequences $x:=(x_1,\dots,x_n)$ and for all formulas $P$, $\mbox{eval}(P,x)\leftrightarrow\mbox{eval}(P,J\circ x)$, where $\mbox{eval}$ evaluates a formula (a code for a wff expression) at a sequence of set values similar to df-sat. (Yes, you need an explicit definition of formula and satisfaction to define elementary equivalence.) $\endgroup$
    – Mario Carneiro
    Commented Apr 19, 2022 at 3:45
  • $\begingroup$ I see, thank you! $\endgroup$
    – Thierry Arnoux
    Commented Apr 20, 2022 at 3:01

Not the answer you're looking for? Browse other questions tagged or ask your own question.