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)

Improve this question
$\endgroup$
4
  • $\begingroup$ See related question about introduction of terms in set theory: mathoverflow.net/a/12405/1946 $\endgroup$
    – Joel David Hamkins
    Commented 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$
    – Carlos Freites
    Commented 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$
    – Joel David Hamkins
    Commented 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$
    – Carlos Freites
    Commented May 26, 2014 at 5:18

1 Answer 1

Reset to default
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.

Improve this answer
$\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$
    – Carlos Freites
    Commented 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$
    – Andreas Blass
    Commented 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$
    – Carlos Freites
    Commented May 25, 2014 at 19:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .