I was looking into model theory where a first-order language can be interpreted with a structure and a variable assignment.
Here is an example of a FOL with interpretation:
We have terms:
Atomic Terms: are constants such as zero
Generative Terms: for each term t: suc(t) is a term
Variable terms: Variables are terms. They are free until captured and turned into bounded variables by a formula.
We have formulas:
Atomic formula: are relations such as isEven, isNotZero
Generative formula:
If $\phi$ and $\psi$ are formula, so is $\phi \wedge \psi$
If $\phi$ and $\psi$ are formula, so is $\phi \vee \psi$
If $\phi$ and $\psi$ are formula, so is $\phi \Rightarrow \psi$
If $\phi$ is a formula, so is $\neg \phi$
If $\phi$ is a formula, so is $\exists x. \phi$
If $\phi$ is a formula, so is $\forall x. \phi$
An intepretation gives meaning to the terms and relations. (And from there formulas can also be interpreted).
Universe: $\mathbb{Z}$
$I(zero) = 0 \in \mathbb{Z}$.
$I(Suc(t)) = I(t) + 1 \in \mathbb{Z}$
$isEven(t) = I(t) \equiv_2 0 \in \mathbb{Z}$
First, I was wondering, is the following property applied to interpretations studied anywhere:
$\forall u \in \text{Universe}. \exists t \in \text{Terms}_\text{without variables} . u = I(t)$
For example, -1 cannot be directly constructed without variable terms.
-1 can only be made accessible using the exists quantifier. $\exists m . suc(m) = zero$
And if you want uniqueness you can use this trick: $\wedge \forall m', m''. suc(m') = zero \wedge suc(m'') = zero \implies m' = m''$
Thus second, I was wondering if the following property is studied and if it has a name in the literature:
Structures for which each element in the universe can be determined uniquely using the existential quantifier trick.