19
$\begingroup$

Zermelo-Fraenkel set theory (with choice) is commonly accepted as the standard foundation of mathematics. It is a material set theory. For every two objects/sets $a,b$ one can ask whether $a=b$ or not. Also, one can always ask whether $a\in b$ is true or not. So $\in$ is a global element relation.

As an alternative foundation for set theory, Shulman proposed SEAR. It is a structural set theory. That is, elements have no internal structure, i.e. are just "abstract dots". One has a type declaration $a\colon A$ for saying that $a$ is an element of $A$. But this can't be negated, so $\colon$ is no relation. But if $A$ is a set (should I say "abstract set" for emphasizing the point that I mean "set in a structural set theory"?), then one has a local element relation $\in_A$: for each element $a$ in $A$ and each subset $B$ of $A$ (= function $A\to 2:=\{0,1\}$), the statement $a\in_A B:\iff B(a)=1$ is either true or false.

On the SEAR-page I linked to above, there is a proof (due to Shulman I guess) showing that SEAR and ZF are basically equivalent: from a model of ZF one can construct a model of SEAR and vice versa. This is a meta theorem. But in which foundation does the proof of such a meta theorem take place? Is this meta foundation a structural or a material set theory?

Improve this question
$\endgroup$
4
  • 4
    $\begingroup$ I think the meta-theory for interpreting SEAR in ZF is nothing more than first-order logic: one just makes the necessary definitions directly in the theory. In the other direction, interpreting ZF in SEAR, we define ZF-sets as equivalence classes of certain well-founded graphs, as described in the nLab article on pure sets ncatlab.org/nlab/show/pure+set, so it looks like some set theory is being invoked there. But I'm supposing nothing more than that (compare the distinction between set and 'setoid': ncatlab.org/nlab/show/equivalence+relation). $\endgroup$
    – Todd Trimble
    Commented Jan 31, 2017 at 15:58
  • $\begingroup$ @ToddTrimble: Thanks. "so it looks like some set theory is being invoked there" Is this set theory a material or a structural set theory? $\endgroup$
    – user103598
    Commented Jan 31, 2017 at 16:06
  • 2
    $\begingroup$ A very weak form of structural set theory would be enough, if my reading is correct. A similarly weak form of material set theory would be enough too (but maybe overkill IMO). $\endgroup$
    – Todd Trimble
    Commented Jan 31, 2017 at 16:19
  • $\begingroup$ How are material set theory and structural set theory related from the point of view of category theory? Would the answer to this question help answer the OP's question? $\endgroup$
    – Thomas Benjamin
    Commented Feb 1, 2017 at 2:21

2 Answers 2

Reset to default
19
$\begingroup$

Your question is much more specific than your title suggests. As to the question itself, my answer is that it doesn't matter. The proof is given in mathematics, not in any formal system. A foundation for mathematics, in order to count as a foundation of mathematics, must be able to formalize most ordinary mathematical arguments. Thus, any foundation for mathematics could be used to formalize such a metatheorem.

With that said, some people care about whether metatheorems of this sort can be formalized in very weak theories. There's nothing wrong with that, but it's not something I spend my time thinking about, and in particular I didn't think about it when writing the proof you refer to. The closest I came was noting that instead of a "construction of a model" the proof can equivalently be regarded as giving a translation of first-order formulas. If you're interested in this sort of question, then Nik's answer seems reasonable to me, but I'm not familiar with the details of how this sort of thing goes.

Improve this answer
$\endgroup$
12
  • 7
    $\begingroup$ I think this is the usual view, but it bothered me as a student because it seems like you are implicitly relying on the consistency of the very systems about whose consistency you are reasoning. So I like the idea that you can regard these problems as number-theoretic questions about the relative consistency of two theories and then prove things about this in a purely number-theoretic system. $\endgroup$
    – Nik Weaver
    Commented Jan 31, 2017 at 18:17
  • 7
    $\begingroup$ @NikWeaver : The thing you say that bothered you as a student arises only if one states explicitly that something like ZFC is being used for the metatheory, not if one states that the metatheory is "mathematics, not any formal system." Maybe what you meant is something else that bothers some students, which is that if rigor is supposed to come from formalization, then doesn't the informality of meta-reasoning mean that the meta-reasoning isn't rigorous, and so everything breaks down? $\endgroup$
    – Timothy Chow
    Commented Jan 31, 2017 at 18:43
  • 6
    $\begingroup$ Still, I think it's a great victory of mathematical logic as a field to have this ability to "bootstrap", not in the Hilbert sense of proving consistency of strong systems from weak ones, but at least in the sense of being able to carry out the meta-theory (and indeed, most of all finitary mathematical reasoning) with very weak logical formalisms. $\endgroup$
    – cody
    Commented Jan 31, 2017 at 18:55
  • 4
    $\begingroup$ @NikWeaver I care more about not relative consistency but "interpretability": that you can directly construct a model of one theory from the other theory in a relatively straightforward way. This tells us how to actually relate (at least in principle) mathematics formalized in the two theories. If someone proves a theorem in ZFC, then I understand directly what it means in SEAR as a theorem about hereditarily well-founded relations, and vice versa: a theorem in SEAR is a theorem in ZFC about the category of sets. This seems to me of more practical importance, especially in this case. $\endgroup$
    – Mike Shulman
    Commented Feb 1, 2017 at 0:37
  • 3
    $\begingroup$ Put differently, consider the category of models of ZF and the category of models of SEAR. To say Con(ZF)$\iff$Con(SEAR) is to say that if one of these categories has an object, then so does the other. I would much rather know that these categories are related by an adjunction or an equivalence, even if I need a stronger metatheory. $\endgroup$
    – Mike Shulman
    Commented Feb 1, 2017 at 4:32
12
$\begingroup$

One direction could go like this. Let ${\rm ZFC}^+$ be the theory in the language of set theory augmented by a constant symbol ${\bf M}$ with the axioms

$\bullet$ every axiom of ${\rm ZFC}$

$\bullet$ "${\bf M}$ is countable and transitive"

$\bullet$ the relativization of every axiom of ${\rm ZFC}$ to ${\bf M}$.

Then one can prove ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm ZFC}^+)$ in Peano arithmetic, and based on the page you linked, it looks like one can straightforwardly prove the consistency of any finite fragment of ${\rm SEAR}$ in ${\rm ZFC}^+$. Thus one can prove ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm SEAR})$ in Peano arithmetic. (If ${\rm SEAR}$ were not consistent then some finite fragment ${\rm SEAR}_0$ would be inconsistent, and this fact would be verifiable in ${\rm ZFC}^+$, so that ${\rm ZFC}^+$ would prove both ${\rm Con}({\rm SEAR}_0)$ and $\neg{\rm Con}({\rm SEAR}_0)$ and hence be inconsistent.) For details see Chapter 7 of my book.

I imagine a similar argument would work in the reverse direction to prove ${\rm Con}({\rm SEAR}) \Rightarrow {\rm Con}({\rm ZFC})$ in Peano arithmetic, but I'm not familiar with ${\rm SEAR}$ so I can't say that for sure.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ Wait, what? Isn't the existence of a transitive model of ZFC strictly stronger than the existence of just any model? $\endgroup$
    – Johannes Hahn
    Commented Jan 31, 2017 at 18:12
  • 2
    $\begingroup$ @JohannesHahn: you can't prove in ZFC${}^+$ that ZFC has any model, transitive or not, assuming ZFC is consistent. You can only prove that any finite fragment of ZFC has a model (which can already be done in ZFC). (This is the idea of why ZFC and ZFC${}^+$ are equiconsistent.) $\endgroup$
    – Nik Weaver
    Commented Jan 31, 2017 at 18:23
  • 3
    $\begingroup$ If one can prove Con(SEAR) in ZFC${}^+$, then one cannot prove Con(SEAR)$\implies$Con(ZFC) in Peano arithmetic, because, by combining the two along with Con(ZFC)$\implies$Con(ZFC${}^+$), we'd get that ZFC${}^+$ proves its own consistency. $\endgroup$
    – Andreas Blass
    Commented Jan 31, 2017 at 19:25
  • 1
    $\begingroup$ @AndreasBlass: you're right, I was sloppy. I'll fix it. $\endgroup$
    – Nik Weaver
    Commented Jan 31, 2017 at 19:35

You must log in to answer this question.