# Would it also be useful to include an ordered pair function in first order logic?

Typically, first-order logic is assumed to include an equality relation $=$, even though this is "non-logical," together with some postulates about equality.

Would it also be useful to include an ordered pair function $(*,*)?$ One could assume that $(x,y)=(x',y')$ precisely when $x=x$ and $y=y'$. Or perhaps it would be best to add denumerably many such functions, $(*)$, $(*,*)$, $(*,*,*)$, etc.

The upshot of doing (either) of these is that relations can now all be unary. This would prettify a lot of notation. For instance, the axiom schema of replacement would look much neater.

Thoughts, anyone?

EDIT: Replacement would read as follows.

$$\forall w \forall A[(\forall x \in A \exists ! y \phi(x,y,w,A)) \Rightarrow \exists B\forall y(y \in B \Leftrightarrow \exists x \in A \phi(x,y,w,A))]$$

-
I am very confused about how the Axiom Schema of Replacement would "look much neater" with the introduction of pairing/tripling/$n$-tupling operations in the syntax itself. Please express this Schema in your new syntax so I/we can judge. – arjafi Feb 4 '13 at 12:14
So now every function has to be defined on tuples of every arity? Not to mention on tuples whose elements are themselves tuples? This doesn't sound very neat to me. – Chris Eagle Feb 4 '13 at 12:31
@ArthurFischer Done. – goblin Feb 4 '13 at 20:48

The main issue with this that I can see would be that it wouldn't allow for any finite models, because if a model has $n$ distinct elements $a_i$, then it also has to have $n^2$ distinct elements of the form $(a_i, a_j)$. I think this on its own is reason enough to avoid it for first order logic in general.

Having said that, there are several individual theories where it is convenient to have a pairing operator. Set theory and number theory both have conservative extensions with pairing operators (that is, there are already "implicit" pairing operators in the theory). Because of this, in these theories someone will often use brackets $(,)$ in their formulas as if there is a pairing operator. Like you said, this does make the notation much nicer.

-

The fact that you mention Replacement leads me to believe that you're especially interested in first-order theories which are meant to capture some sort of set theory. In a set theory, we have a way of identifying ordered pairs with elements of the universe - the standard choice in ZFC is to code $(a,b)$ by the element $\{\{a\},\{a,b\}\}$.

Now we have a definable predicate Pair($x$) which determines whether some set $x$ codes a pair (it says "This set has two elements. One of these has one element, $a$. The other has at most two elements, one of which is $a$.") and definable functions First($x$) and Second($x$) which return $a$ and $b$. The theory then proves $\forall a \forall b \exists x\, \text{Pair}(x) \land (\text{First}(x) = a) \land (\text{Second}(x) = b)$.

By adding the ordered pair function, you're adding a Skolem function for the sentence above. This eliminates the existential quantifier, so you now have $\forall a \forall b \text{Pair}((a,b)) \land (\text{First}((a,b)) = a) \land (\text{Second}((a,b)) = b)$. This is a totally standard thing to do in first-order logic - it simplifies syntax without changing the strength of the theory or its class of models (this is what the user aws means by saying that set theory has a "conservative" extension with a pairing operator). It's analogous to adding the inverse symbol ($^{-1}$) to the theory of groups. You can read more details on the wikipedia link.

But set theory is somehow special in that there is a canonical way to code a pair of elements as a single element. That is, there is a definable injection $M^2 \rightarrow M$ for any model $M$. In general first-order logic, you don't have this kind of structure, and adding a pairing function to a general theory could really change the theory.

However, there is a "safe" way to add pairing (and n-tuple) functions to an arbitrary first-order theory, which I'll describe now. We move from single-sorted logic to many-sorted logic, with one sort for each natural number. The $n^{th}$ sort represents the cartesian power $M^n$. Now for each $n$, we can also add an $n$-ary function $f_n$ which takes the $n$ elements $x_1,\dots,x_n$ to the element in the $n^{th}$ sort representing the $n$-tuple ($x_1,\dots,x_n$). We also add axioms stating that $f_n$ is a bijection for each $n$. One can check that this is construction gives a "conservative extension" in some sense.

The advantage of this situation is that we can now view all definable functions and relations as unary, as you wanted. The expense is that we're in a many-sorted context, which you have to get used to. Model theorists often go further, adding new sorts not just for all $M^n$, but for all quotients of $M^n$ by definable equivalence relations - the resulting theory is called $T^{eq}$, and it is a nice place to work for a variety of reasons.

-
In fact, there are lots of pairing functions in set theory – one benefit of using an explicit pairing function is to get rid of the "theorems" that depend on the precise implementation of pairing. – Zhen Lin Feb 4 '13 at 19:14
@ZhenLin Yes, that's a good point - there's another approach, which I didn't talk about, where you add a pairing function to the language and an axiom saying that it's injective, but you don't specify the form of output. This is attractive in that you don't get "meaningless theorems" like $\{a,b\} \in (a,b)$. On the other hand, it might be unattractive to people who want set theory to be "as close to complete as possible" - it makes lots of very simple sentences independent! Of course, this might support the point of view that this desire for completeness is misguided... – Alex Kruckman Feb 4 '13 at 19:38

A comment on an incidental (but interesting) feature of the question, rather than a direct answer. According to the OP:

Typically, first-order logic is assumed to include an equality relation =, even though this is "non-logical", ...

But why suppose identity is non-logical? We need a demarcation criterion for distinguishing logical from non-logical operators. Let's consider two:

A. There's the idea going back to Gentzen that a logical operator is one that is fully defined by introduction rules and (harmonious) elimination rules. This idea is explored in e.g. a famous paper by Ian Hacking 'What is Logic?' (1979) reprinted in e.g. Dov Gabbay (ed) What is a Logical System?.

B. There's the idea going back to Tarski that a logical operator is one that exhibits a certain invariance under arbitrary permutations of the domain of objects. This idea is explored in e.g. Tarski's 'What are Logical Notions?' History and Philosophy of Logic (1986). (Transcript of a 1966 talk.)

Both ideas A and B, for a start, make identity a logical operator.

-
I was implicitly defining non-logical as follows: A logical symbol can be viewed as acting on formulae and returning a formula, whereas a non-logical symbol can be viewed as acting on acting on expressions and returning a formula. However, the possible definitions of "logical operator" you mention are probably better definitions than what I had in mind. – goblin Feb 4 '13 at 20:58

Pairing does exist in first-order logic.

It is implicit in untyped logic, as pairing is managed through the way we organize formulae. e.g. in the theory of real closed fields (arithmetic of real numbers), we can't have a variable $P$ that represents a point of the Euclidean plane $\mathbb{R}^2$, but we can systematically use two variables $x$ and $y$ always quantified in pairs and used together in relations and functions.

In untyped logic, we can introduce pairing at a purely syntactic level as well. We can define a new language that allows variables that range over tuples of objects, and provide a purely syntactic translation from this new language into the old language where all variables are merely objects.

There is also typed logic, which generally have explicit product types. e.g. taking again the theory of real closed fields, we can let $R$ denote the type comprising numbers, and there are product types such as $R \times R$ comprising pairs of numbers.

-