The Löwenheim–Skolem theorem implies, among other things, that any first-order theory whose symbols are countable, and which has an infinite model, has a countably infinite model. This means that, in attempting to refer to uncountably infinite structures (such as in set theory), one "may as well" be referring to an only countably infinite structure, as far as proofs are concerned.

The main limitation I see with this theorem is that it preserves arbitrarily deep quantifier nesting. In Peano arithmetic, it is possible to form statements that correspond (under the standard interpretation) to arbitrary statements in the arithmetic hierarchy (by which I mean, the union of _Sigma^0_n_ and _Pi^0_n_ for arbitrary n). Not all of these statements are computable. In general, the question of whether a given statement is provable is a [...]

---

Outline:

(02:01) Propositional theories and provability-preserving translations

(05:45) Recap of consistent guessing oracles

(07:11) Applying consistent guessing oracles to dequantification

(13:33) Conclusion

---

First published:

Source:

Linkpost URL:
https://unstableontology.com/2024/04/23/dequantifying-first-order-theories/

Narrated by TYPE III AUDIO.