1
$\begingroup$

Suppose $T$ is a set theory, i.e. doesn't have proper classes. And $T$ can interpret $\sf PA$, and $T$ is an effectively generated consistent first order set theory. Now, let $T^+$ be a class theory that extends $T$. More specifically $T^+$ is bi-sorted with first sort (in lower case) ranging over sets of $T$ and second sort (in upper case) ranging over all classes. Now we add all axioms of $T$ in lower case, axiomatize $\forall x \exists Y: x=Y$ and also axiomatize $\forall Y: Y \in X \to \exists z: z=Y$. The class axioms are just Extensionality for classes and Comprehension asserting that every formula $\phi$ that doesn't mention "$X$" there is a class $X=\{y \mid \phi(y)\}$

Now, assume that $T$ can prove pairing and $T^+$ proves induction over the naturals. Notice, that $T^+$ may just be a conservative extension of $T$. Also suppose that $T$ is finitely axiomatizable.

Would that be enough to ensure that $T^+$ must not be finitely axiomatizable?

Improve this question
$\endgroup$
7
  • $\begingroup$ Why only those second-order axioms? This doesn't even cover the main cases of GBC and KM, which have the replacement axioms, not to mention global choice. Further, the critical difference between GBC and KM is whether you have class comprehension only for first-order assertions (with class parameters) or fully for second-order assertions. You are ambiguous on whether $\phi$ is first or second order, but I think you mean second-order because of your other questions. But this is highly relevant for finite axiomatizability, since GBC is finitely axiomatizable, but KM is not. $\endgroup$
    – Joel David Hamkins
    Commented Jul 2 at 18:04
  • $\begingroup$ @JoelDavidHamkins, yes, correct, I meant second order actually any formula first or second. There is an induction axiom scheme over naturals, this is a second order schema. Does that matter as regards non-finite axiomatizability, because I saw that with KM but not with GBC. $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 2 at 18:11
  • 2
    $\begingroup$ I would have to think about it, since your theory is both weirdly weak, lacking replacement, and also weirdly strong, with second-order comprehension. I don't find it a natural theory. I would guess it likely isn't finitely axiomatizable, since it is closer to the KM case, but in lacking those other powers, the question is whether this would still be true. $\endgroup$
    – Joel David Hamkins
    Commented Jul 2 at 18:14
  • 3
    $\begingroup$ If by “$T^+$ proves induction” you mean that it proves the induction schema for all formulas in its language, then $T^+$ is (uniformly essentially) reflexive (see mathoverflow.net/a/87249; note that any reasonable theory of classes is sequential), hence not finitely axiomatizable unless inconsistent. $\endgroup$
    – Emil Jeřábek
    Commented Jul 2 at 18:24
  • $\begingroup$ @EmilJeřábek, so full induction is vital! So, the answer is to the positive. I think this needs to be put as answer to this question. $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 2 at 19:36

1 Answer 1

Reset to default
5
$\begingroup$

As explained with more details in https://mathoverflow.net/a/87249, every sequential theory that proves the induction schema for all formulas in its languages is reflexive (even uniformly essentially reflexive), and as such it cannot be finitely axiomatizable unless it is inconsistent, by Gödel’s theorem.

Any reasonable class theory is sequential (this means, roughly, that we can code finite sequences of objects of the theory in such a way that an empty sequence exists, and any sequence can be extended by any object as a new element). E.g., we can code finite sequences of classes such that a class $X$ encodes a sequence whose $i$th element is $\{x:\langle i,x\rangle\in X\}$. A weak fragment of comprehension ensures that this works.

Your postulates for $T^+$ ensure that it proves induction for all formulas. Thus, it is indeed reflexive, and not finitely axiomatizable unless inconsistent.

Note also that contrary to the assertion in the question, $T^+$ is not a conservative extension of $T$ (unless $T$ is inconsistent), as it proves the consistency of $T$, for much the same reason.

Improve this answer
$\endgroup$
2
  • $\begingroup$ When you say $T^+$ proves $\sf Con(T)$, then this $\sf Con(T)$ is written in which language? Why can't it be in the language of $T^+$ but not in the language of $T$? $\endgroup$
    – Zuhair Al-Johar
    Commented Jul 3 at 20:26
  • $\begingroup$ Con(T) is formulated in the usual way in the language of arithmetic, which is already included in $T$. $\endgroup$
    – Emil Jeřábek
    Commented Jul 3 at 21:17

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