# Is the formular "x is red" written in the first order language?

I watched a video lecture on the set theory by the lecturer whom I respect the most. He provided an example of a property in the axiom schema of separation. He stated that in $$S=\{x\in \{3,4\} |$$x is red$$\}$$ the property "x is red" is good enough for the set to be defined. He said it could be any property, Russel Paradox is gone since we have $$x\in\{3,4\}$$. I understand why. The lecturer stated that this set is a null set, since the letters $$3$$ and $$4$$ were written in white color. But I also googled that the property should be built in the first-order logic language with only non-logical quantifier $$\in$$. My first question is: does this property really built in the first-order logic language with only non-logical quantifier $$\in$$? Can we really make some extra definitions for what is red and construct this set? Second question, does the axiom in this variant (when a property is just any property like he said) always allow to avoid paradoxes? Or set theory language is a must for the construction of the property?

• Can sets of oranges be defined using ZFC and the first-order logic language with only non-logical quantifier $\in$? I am asking since in ZFC we build sets starting from a null set. Using ZFC and some definitions we can build natural and real numbers, but not oranges? Or sets of oranges too can be built in ZFC (just some extra definitions for oranges)? Oct 29, 2020 at 16:32
• No; oranges cannot be defined using ZFC. Oranges are not mathematical objects. Oct 29, 2020 at 17:24
• "X is red" is written in the 1st order language. We can now create axioms: every object on earth equals to a single number (all these numbers should be different). So the set of oranges is defined? Where did i make a mistake? Oct 30, 2020 at 6:56
• If i can not create new axioms I can call it hypotheses in the 1st order language? Oct 30, 2020 at 6:59
• No; as said above, we cannot "define" oranges and their properties in ZFC. We can build a dedicated FO theory for oranges with specific primitive predicates and axioms. Oct 30, 2020 at 8:38