How are properties like "definability" called (in which formulas are involved):

A set $X$ is definable when there is a formula $\phi(x)$ such that $X = \lbrace x : \phi(x)\rbrace$.

It is not a first-order property (not even equivalent to a first-order property!), and it is not a second-order property (but maybe equivalent to a second-order property?)

Is it called a "semantic property" or a "meta(-theoretical) property"?

What is the usual name?

A companion definition of the one above is

A formula $\phi$ is a set-builder when there is a set $X$ such that $X = \lbrace x : \phi(x)\rbrace$.

How are such properties (of formulas) called?

Caveat: I am aware of the fact that treating formulas as sets will lead to problems when definability, truth, or satisfaction comes into play. So I explicitly want to treat them as linguistic entities, different from the objects they are talking about, so no contradictions can arise.

  • $\begingroup$ See this question at MO: mathoverflow.net/questions/146307/… $\endgroup$ – Hans-Peter Stricker Oct 29 '13 at 22:44
  • $\begingroup$ In Computability Theory one usually talks about representability of a given set/predicate/function in a given theory (in that sense, for instance, computable functions can be represented in a formal theory containing enough arithmetic). Is that what you're interested on? $\endgroup$ – J Marcos Oct 30 '13 at 0:50

I'd call such properties "logical". In the precise sense, that they are defined by reference to the properties of a (formal) language in an arbitrary context.

As you observe, a property whose definition involves quantifying separately over formulae and subsets of the universe is neither first- or second-order. Classification into orders is not really helpful here. The property would find a home somewhere in the Russell-Whitehead ramified theory of types, but that doesn't really add much to your understanding of what it means or how it behaves.

Of course in a sufficiently rich context (a model of ZFC, for example) you can treat both the language, and sets of elements, as first-order concepts: this is more or less what Goedel does in the incompleteness theorems. So there's really no need to get hung up about order or type unless you're thinking philosophically about the foundations of mathematics.

For actual mathematical purposes calling "definability" a logical property of a set (in a way that "being a subset of the direct product of the set of all elephants and the set of all angels" isn't), and "being a set-builder" a logical property of a formula (unlike "rhyming"), is clear enough.

  • $\begingroup$ I don't think that logical is a complete answer. Question says that "it's neither first order logic, nor second order logic. Then what type of logic is this?" Of course it's logical, but I don't think that this is what's asked. $\endgroup$ – Zafer Sernikli Nov 5 '13 at 13:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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