The Löwenheim–Skolem theorem implies that if ZFC is consistent then its countable model M exists.

  1. What theory is used to say that M is countable?
  2. Is there an uncountable model if ZFC is consistent?
New contributor
Elmar Guseinov is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.

put on hold as off-topic by Emil Jeřábek, Wojowu, Andreas Blass, Andrés E. Caicedo, RP_ 2 days ago

This question appears to be off-topic. The users who voted to close gave these specific reasons:

  • "This question does not appear to be about research level mathematics within the scope defined in the help center." – Andrés E. Caicedo, RP_
  • "MathOverflow is for mathematicians to ask each other questions about their research. See Math.StackExchange to ask general questions in mathematics." – Emil Jeřábek, Andreas Blass
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ Question 1 is unclear, and in any case this would be a better fit for Math Stack Exchange, as it's not research-level. $\endgroup$ – Kevin Carlson Aug 14 at 19:47
  • 2
    $\begingroup$ (1) Like most of mathematics, this result is ordinarily proved in ZFC. Considerably weaker theories suffice, though, for example Zermelo set theory (i.e., you don't need replacement or choice), and you can probably get by without power set. (2) Yes, by the upward Löwenheim-Skolem-Tarski theorem (but now you do need power set and probably a weak version of choice). $\endgroup$ – Andreas Blass Aug 14 at 19:49
  • 1
    $\begingroup$ @KevinCarlson I don't think it's unclear since a theorem is often defined as a sentence of a language, thus this sentence may be obtained in some theory. $\endgroup$ – Elmar Guseinov Aug 14 at 20:04
  • 3
    $\begingroup$ Part 1 isn't Lowenheim-Skolem, it's (a form of) the model existence theorem, which is provable in PA. $\endgroup$ – Nik Weaver Aug 14 at 20:22
  • 1
    $\begingroup$ For 1, the usual Henkin proof (if acceptable in your system) comes with an explicit enumeration of the terms of the model. You then need to mod out by provable equality (if you care about that). In any case the "countability" aspect of the proof is immediate (so long as your "countability" notion is closed under quotients, if you care about modding out). $\endgroup$ – François G. Dorais 2 days ago