What kind of Properties are Allowed in the Schema of Comprehension?

Studying an introduction to set theory, we were presented with several axioms as the Axiom Schema of Comprehension and the Axiom of Infinity. This last aximom allows the definition of the inductive set.

The Schema of Comprehension states that every property defines a subset. If Pᵢ(x) is a property of x which can be true or false and Aᵢ is any defined set:

Provided Q(x) ≡ Pᵢ(x) ∧ x∈Aᵢ then, ∃Bᵢ { x ∈Bᵢ | Q(x) }

I have no complete comprehension of what can a property be. Can we define a property for each natural number (#(ϕ)) depending on whether the Gödel coded logical sentence (ϕ) it represents is provable or true? Awareness of the undecidability of this property implies there will be some elements within the subset of natural numbers this property defines that we are just not allowed to know if they belong or not to this new subset. Is this correct and/or allowed?

The main issue I'm trying to settle with this question is to achieve some clarification of which are the rules of logic appliying for the definition of this properties in the Axiom Schema of Comprehension. Can this properties be undecidable? Are there any types of definitions depending on the order of logic? Can someone recomend some reading on this?

I hope I can make the question more clear this time.

UPDATE: Interpretation that Confuses

I’ll write here the main conflict I think is produced between Axiom of Infinity and Axiom of Comprehension. I think this reasoning must not be correct, but I’m having a hard time understanding which are the allowances of the underlying logic that defines properties. Please excuse the untidiness as I’m no mathematician, I’m trying the best I can:

With Axioms of Infinity and the Schema of Comprehension, if we use some type of Gödel encoding for all logical symbols and also include a free variable, g. I will use these expressions:

• The #’(Ф) is the Gödel coding of logical symbols plus a free pointer variable g
• True(#’(Ф)) is a logical sentence that holds if Ф is true (we may not be able to decide if it does)
• Prov(#’(Ф)) is a logical sentence that holds if there exists a logical poof for Ф (we may not be able to decide if it does)

Every natural number encodes to some enumerable phrase in this logical language (that includes g). Some are undecidable, some are ill posed, some have g as a free variable. There is one that states “¬Prov(g)”.

Please consider some group of properties Pᵢ(x), as those which are true only in the case that: While g=i, if True(x) holds, then Pᵢ(x). For example: Pᵢ(x) ↔ g=i → True(x). We have a property for every natural number i. These properties can be undecidable.

For the very specific property in this group, in which i=#’(¬Prov(g)) there will be a member of the inductive set which can’t either belong, neither not belong, to the subset of naturals defined by Pᵢ(x). That member is #(¬Prov(g)).

If ¬True(g), then Prov(g). But if we can prove g, and also, we know that for this particular set i=g, we have that Prov(¬Prov(g)). This means either our logic is faulty or ¬Prov(g) holds.

If True(g), ¬Prov(g), but we also know that Prov(g) because we just prooved ¬True(g) is inconsistent.

So, granted any set Aᵢ, and Q(x) ≡ Pᵢ(x) ∧ x∈Aᵢ then {∃ i∈N | ∄Bᵢ { x∈Bᵢ | Q(x) }}

I think this reasoning is not allowed, or at least not in FOL, it mixes levels. Please if you could point out the flaws.

Original Question Titled: Presentation of the Inductive Set and the Allowed Logical Properties of the Schema of Comprehension

I was studying an introduction to set theory where the axioms are presented, I believe, according to some systemic expression need. So I reached a point where we need to define the group of natural numbers, and with the axioms so far introduced, we cannot postulate the sure existence of an infinite set. The Axiom of Infinity is then introduced for the production of the inductive set.

Previously we studied that if we have a set, a property always defines a subset within it (due to the Axiom Schema of Comprehension). So following this, it would seem possible to state a property that is not able to define a subset of naturals. Would this contradict the Axiom Schema of Comprehension?

Using some Gödel coding, enumerating properties that discriminate upon provability, and holding every time a different static pointer, until it matches the index of a Gödel sentence, is it possible to produce this property?

Please if someone could bring some light into this confusion pointing out how and why it is or isn’t well conceived, or under what order of logic could that property be defined. I’ve been very confused after we reached this axiom because I’m not familiar with the logic rules underlying the definition of a property, and just know some of the conventions as presented in the introduction to sets.

Strictly, what can and what cannot be a property? Under which conditions is this? Maybe you can refer me to some related reading for this. I found this thread that addresses self membership, but does not consider the fact that naturals can code enumerable logical sentences. Please help.

• It might be helpful if you could try to state the comprehension scheme in your own words (as this has the potential to highlight the specific issues/missunderstandings/... you are having with it). Besides that: I have no idea what you're asking in your second paragraph. – Stefan Mesken Mar 30 '16 at 1:32
• Hi @Stefan, thanks for your answer. What we know so far is that the Schema of Comprehension says that if Pᵢ(x) is a property of x which can be true or false, and Aᵢ any defined set, then: ∃Bᵢ { x ∈Bᵢ | Pᵢ(x) ⋀ x∈Aᵢ } Please correct me if im wrong in this. If we have the Axiom of Infinity and Schema of Comprehension, it seems we can map enumerable logical truths to the naturals in the set of natural numbers. Is it possible to define a property that decides truth for every natural, upon the provability or truth of the logic sentence coded by it? Something like Pᵢ(#(ϕ))↔ϕ – C.Dhio Mar 30 '16 at 13:08
• These questions are somewhat unrelated. First of all: What you name a "property" is a first-order formula in the language of set theory and "$x \in A$" is such a formula - so there is no need to distinguish between your $P(x)$ and $x \in A$ - they can be combined to the formula $Q(x) \equiv P(x) \wedge x \in A$. Regarding the second questions: There is no formula $P(x)$ such that for every sentence $\phi$, we have $P(\#\phi) \leftrightarrow \phi$. This is Tarski's undefinability theorem. – Stefan Mesken Mar 30 '16 at 13:23
• @Stefan, you are most clarifying. Please comment if the following conclusions are correct: 1. Properties must be defined in FOL using the theory's language. 2. Tarski's Theorem implies that you can't define a property that assigns truth to an element based on the theory's semantics. Regarding point 2, please if could you help me clarify: Is it correct that defining is not the same as deciding in Tarski's Theorem? Could you define a property based on provability? Can you please point some reading to understand Undefinability Theo. in this context? I read wiki but need more introd. Thanks!! – C.Dhio Mar 30 '16 at 13:47
• Technically, properties don't have to be FOL formulae, but in the given context they are. You can allow more complicated properties, but this isn't what you want to worry about right now. The second point is a bit more complicated. Tarski's Theorem says that there is no single formula that decides truth for all sentences. However, in $ZF$, for every finite number of sentences (and in fact for any level of the Lévy hierarchy such a formula can be explicitly written down - this isn't entirely obvious and requires some work. – Stefan Mesken Mar 30 '16 at 14:24