3
$\begingroup$

Consider the axioms of Hilbert geometry: the undefined elements are points, lines and planes. We are not talking about points as coordinates, lines as sets, etc. This theory has no model at all: we are not sure if we can describe points, ..., as sets. However, in proofs we’ll be always using sets of points, sets of planes, etc, which $\mathbb{ZFC}$ does not explicitly describe as existent since its universe of discourse is limited to sets. Why can we create sets of points?

Since the original question was not totally clear, we can have an analogy with Peano’s naturals. If we use them, the naturals are not necessarily sets, but we can construct set of naturals. The same applies for the axiomatic construction of the reals. They are not necessarily sets and, from the universe of discourse of Zermelo’s theory, we can’t construct sets of reals unless reals are proven to be sets or we create new axioms that describe truths between real numbers (undefined elements) and sets.

The main focus of this question is the formality to describe the relation of the objects of different formal theories. How can we relate these objects, specifically sets and other structures?

$\endgroup$
12
  • 2
    $\begingroup$ Do you understand how, say, $\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, $\mathbb C$ and their arithmetic can be formalized in set theory? $\endgroup$ Aug 12, 2018 at 16:44
  • 3
    $\begingroup$ I don't understand. Construction of what? What do you mean 'on reals'? New axioms compared to what 'old' axioms? (If you mean by 'on reals' that your question could just as easily apply to the real numbers as to geometry, then it would probably be most efficient to stick to that example and clarify what you mean relative to that.) $\endgroup$ Aug 12, 2018 at 21:56
  • 1
    $\begingroup$ Still having a hard time understanding what you mean but I think a picture is forming. Is this an accurate rephrasing of your question? “A second order theory of, say, the real numbers requires we talk about both reals and sets of reals. Thus, in addition to the axioms for real numbers, we also need the axioms of ZFC to tell us how to reason about sets of reals. However the axioms of set theory only talk about sets of sets, not sets of real numbers, so they can’t actually accomplish this. How do we accomplish this?” $\endgroup$ Aug 13, 2018 at 15:43
  • 1
    $\begingroup$ When you talk about the reals being a (or in this case, the) model of some second order axioms you are talking about reals and sets of reals in the metatheory, not the aforementioned second order theory. So your metatheory needs to be able to talk about reals and sets of reals and verify that the axioms hold. Usually, the metatheory is just informal math (usually mathematicians have no trouble reasoning precisely about reals and sets of reals). If we want to formalize the metatheory, one way is, as in Noah’s answer, where we represent both reals and sets of reals as sets and reason with ZFC. $\endgroup$ Aug 13, 2018 at 16:20
  • 1
    $\begingroup$ There is no conflict between this and the fact that the 2nd order theory of reals just has variables and set variables that we take to quantify over reals and sets of reals. In particular there’s no need to develop any set theory here: what an arbitrary set of reals is is “given”. All the set theory that formalizes this is in the metatheory. $\endgroup$ Aug 13, 2018 at 16:26

1 Answer 1

5
$\begingroup$

It's analogous to how informal-but-precise algorithms can be performed by computer programs, or how (a la Godel's incompleteness theorem) statements about provability can be "expressed in arithmetic" in some sense even thought they're obviously not simply statements about natural numbers, or how computer games can "describe physics" even though the described objects aren't literally inside the computer: the point is implementation.

Basically, when we think of "doing geometry inside ZFC," we're not claiming (or at least, don't need to be claiming) that points, lines, etc. literally are "pure sets" - rather, we're claiming that there is a way to define within ZFC something that "behaves like" geometry in a precise sense. We're not even claiming that this implementation is unique, any more than one claimes that there is a unique computer program (or even a unique computer program in a given language) which performs a specific algorithm, or a unique method of Godel number, or similar.

I think a good example to work on understanding is the connection between natural numbers and finite ordinals. It's hard to argue that the natural number $17$ literally is the set it's represented by in ZFC (namely, the seventeenth finite ordinal), but on the other hand the finite ordinals together with the purely-set-theoretically-defined operations of ordinal addition and ordinal multiplication correspond to the "true" natural numbers in an obvious way (e.g. the ordinal sum of the first and second finite ordinals is the third finite ordinal, just like how $1+2=3$).

There is a lot to be said along these lines, but for now you should just think of the following analogy:

ZFC is to ordinary mathematics as your favorite programming language is to algorithms.

It's by no means the only way to implement mathematics in a unified way, nor are the "standard implementations" of various pieces of mathematics in ZFC (to the extent that they exist) the only such implementations, but that's not the point: we only need ZFC to do its job.

$\endgroup$
2
  • $\begingroup$ I know that ZFC is just a model. Despite that, we need formality when talking about the mathematical community. If we want set theory, we use a model. This model has rules. Since geometry uses set theory, we’ll have to use a model within its formalities: so how does one plug other undefined elements within those problematic formalities? $\endgroup$ Aug 12, 2018 at 21:36
  • $\begingroup$ Looking at our comments in my answer, could you formalize this in terms of metatheory? $\endgroup$ Aug 14, 2018 at 0:46

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