Can you use constants from the domain in a First Order Formula?

52 Views Asked by At

Say I have a First Order Signature defined like so:

$N = (\{1,2,3\dots\},T)$

Where T is a binary relation symbol. Can I use values from the domain to define functions over this signature? For example, could I have the function:

$\phi(x) = \forall y(T(x,y) \implies (y = 1))$

Or perhaps:

$\psi(x) = \forall y(T(1,y) \implies (T(x,y))$

(If you're interested, the reason why I'm asking this question is because I've been asked to define a prime number based on the signature $N = (\{1,2,3\dots\},T,A)$ where A and T are ternary operators for multiplication and addition respectively.)

1

There are 1 best solutions below

0
On BEST ANSWER

Are you sure your not mixing together a signature and a structure? A signature doesn't specify the domain. The whole point of a mathematical theory is that you can interpret it in any domain that can provide the structures and satisfy the constraints specified in the signature. As such, no, you can't use elements of the "domain", because you don't know what the domain is! If you need special elements to exist in the domain with special properties, you need to add nullary function symbols to the signature as Henno Brandsma states. Note, you only need to add function symbols for the elements you actually need, e.g. you might add $0$ and $1$, but you don't need a symbol for every natural number.

To illustrate, let's say you did have a signature with $0$, $1$, $A$, and $T$ and equations to make $A$ and $T$ behave like (functional relations for) addition and multiplication in a commutative ring. (Actually, a commutative semiring would probably be more appropriate.) Motivated by the example of natural numbers, you could make a definition of "prime" and prove some theorems. However, when you were done, your definition of prime and results would apply to anything which could support the signature, i.e. to any commutative (semi)ring. For example, to complex numbers or functions over an arbitrary commutative (semi)ring or arbitrary fields.