0
$\begingroup$

The idea is to build in ZFC using replacement, a set REPLACEMENT(x ∈ A: TERM(x)) from a set and a term in the same way the set {x ∈ A: FORMULA(x)} is built using specification from a set and a formula.

Given a set A and a TERM(x) with a free variable x, can be proved, using the axiom scheme of replacement, the existence of a set named

REPLACEMENT(x ∈ A:TERM(x)) with the following property

For all set z, z ∈ REPLACEMENT(x ∈ A:TERM(x)) <==> There is one x ∈ A such that z = TERM(x)

$\endgroup$
4
  • $\begingroup$ See related question about introduction of terms in set theory: mathoverflow.net/a/12405/1946 $\endgroup$ May 25, 2014 at 7:11
  • $\begingroup$ Exactly, Joel. The third paragraph of the answer 4, state "One might try to make all of the axioms of ZFC into term-forming operators, so that instead of saying "there exists a set with no elements" there would be a specified term ∅ and an axiom saying "∅ has no elements," and likewise for pairings, unions, replacement, etc... " and it is exactly what I have done in my ZFC formulation, do I have terms in it. $\endgroup$ May 25, 2014 at 14:43
  • $\begingroup$ Yes, and so the point is that you can introduce any such kind of terms, over any theory that proves that there are such sets realizing the terms definitions, and the new theory will be conservative over the original theory. In a sense, mathematicians and set theorist already do this instinctively, since one almost never sees assertions written out in the fundamental language of set theory (and nobody wants to see such assertions). Rather, we all pepper our mathematical reasoning with defined terms and expressions. And this is perfectly safe, for the reasons in the answer to which I linked. $\endgroup$ May 25, 2014 at 14:48
  • $\begingroup$ However I go further, my "NUCLEUS" develop the minimum to arrive to the Complete Field definition, then I take the Real numbers (and 0,+,1,*, etc) as a constant that is a Complete Field. This may be not standard, but works very well. $\endgroup$ May 26, 2014 at 5:18

1 Answer 1

2
$\begingroup$

If you're just asking whether this can be proved, the answer is yes (assuming that "For all SET(z)" means "For all sets z"). More importantly, this can be proved also for extensions by definitions of ZFC. That's important, because the official vocabulary of ZFC has no function symbols, so the only terms are variables; you need to pass to extensions by definitions to get non-trivial terms.

I don't like your notation though; it would be less confusing if the elements of the resulting set were to the left of the colon, as in the usual set-builder notation.

A more general notation, $\{t(x):x\in A:\phi(x)\}$, where $t(x)$ is a term and $\phi(x)$ is a formula, has been used. I don't remember where I first saw it; Yuri Gurevich, Saharon Shelah, and I used it in our paper "Choiceless polynomial time", but it had already been used earlier by others.

$\endgroup$
3
  • $\begingroup$ Thank you. Your assumption is right "For all SET(z)" means "For all set". About the lack of function symbol in ZFC, is just because that, I used the theorem in a language I built based in ZFC. On the other hand, in the notation you cited {t(x):x∈A:ϕ(x)} I can not see where the formula ϕ(x) come from, would not be enough {t(x):x∈A} because what is given are the set A and the term t(x). Thanks again, your answer is a relief to me. $\endgroup$ May 24, 2014 at 21:08
  • $\begingroup$ By including $\phi$, we get a construction that directly incorporates both replacement (by taking $\phi(x)$ to be some formula that is true for all $x$, like for example $x=x$) and separation (by taking $t(x)$ to be simply $x$), without going through the (easy but somewhat unnatural) process of getting separation as a special case of replacement. Whether one can get by without $\phi$ altogether depends on how rich a supply of terms one has; you indicated that you add some terms by extending the language of ZFC, but it may matter how widely you extend the language. $\endgroup$ May 25, 2014 at 1:43
  • $\begingroup$ By taking the Real numbers as a Complete Field constant, I have made optional construct it. Thank you. $\endgroup$ May 25, 2014 at 19:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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