How to define "is a structure" by a first-order formula of ZFC

Question

So, I've been trying to define a series of notions by first-order formulas in ZFC, and I'd like to know if I'm getting this right. In particular, I'd like to know if my formula for defining a first-order structure is correct. Generally, we understand, rather informally, a structure as, say, $\mathfrak{A} = \langle A, r_i, f_j, c_k \rangle_{i \in I, j \in J, k \in K}$, with each $r_i$, $f_j$, and $c_k$ being, respectively, a relation symbol, a function symbol, and a designated element, all indexed by the sets $I, J, K$. So in order to express this by a first-order, I came up with:

$\mathrm{Str}(\mathfrak{A}) = _{\text{def}} \exists A, I, J, K, R, F, C [(\forall r \in R (\mathrm{Rel}(r) \wedge \exists n \in \omega \mathrm{Dom}(r) = A^n \wedge \mathrm{Ran}(r) = A \wedge \exists \nu (\mathrm{Func}(\nu) \wedge \mathrm{Dom}(\nu)= I \wedge \mathrm{Ran}(\nu) = R \wedge \mathrm{Bij}(\nu))) \wedge (\forall f \in F (\mathrm{Func}(f) \wedge \exists n \mathrm{Dom}(f) = A^n \wedge \mathrm{Ran}(f) = A \wedge \exists \mu \mathrm{Dom}(\mu) = J \wedge \mathrm{Ran}(\mu) = F \wedge \mathrm{Bij}(\mu))) \wedge (\forall c \in C (c \in A \wedge \exists \xi \mathrm{Dom}(\xi) = K \wedge \mathrm{Ran}(\xi) = C \wedge \mathrm{Bij}(\xi)) \wedge (\mathfrak{A} = \langle A, R, F, C \rangle)]$

Assuming, of course, that the predicates "is a relation", "is a function", "is the domain of", "is the range of", "is a bijection", are already defined. Does that work? Is there an easier way of doing it?

Answer 1

The simplest way, I think, is to use the following approach.

We have the language, $\cal L$ which is an ordered tuple of pairwise disjoint sets, and a function $\sigma$. The sets are constants, relations, functions and variable symbols. And you have an arity function $\sigma$ which takes a relation and function symbol and returns a natural numbers for the arity of that symbol.

An interpretation for $\cal L$, a structure, is a pair $(M,\Sigma)$ where $M$ is a non-empty set and $\Sigma$ is the interpretation function. Namely:

1. For every constant symbol $c$ in $\cal L$, $\Sigma(c)$ is an element of $M$.
2. For every relation symbol $R$ in $\cal L$, $\Sigma(R)\subseteq M^{\sigma(R)}$.
3. For every function symbols $f$ in $\cal L$, $\Sigma(f)\colon M^{\sigma(f)}\to M$.

Your suggestion seems to be somewhat close to this. But there are issues. If $R$ is a binary relation symbol, it cannot be interpreted as a ternary relation symbol, but by saying $\exists n$ you in fact allow that. Additionally the domain or range of $R$ need not be everything.

If this is not what you meant, then it goes to show you that your suggestion is quite complex and unclear.

Finally, if you want a general notion of structure, then just state "There exists a language $\cal L$ such that $(M,\Sigma)$ is a $\cal L$-structure".