Pairs, sets and sequences in first-order theories (Q943342)

The paper studies first-order theories (recursively axiomatizable, in a finite language) endowed with so-called containers, such as ordered and unordered pairs, sequences, sets. Formally, a theory possesses certain containers if it supports an unrelativized interpretation with absolute equality (a direct interpretation) of a suitable container theory. The author explores the idea that for certain types of containers, this is equivalent to the ostensibly much stricter condition that the theory is definitionally equivalent to an extension (in the same language) of the container theory. Thus, a theory \(U\) is called adaptive if whenever a theory \(V\) directly interprets \(U\) then \(V\) is definitionally equivalent to an extension of \(U\). The main results of the paper state that the theory of functional non-surjective ordered pairing, and a weak set theory WS (axiomatized by the existence of successors and of an empty set) are both adaptive. In particular, a theory is sequential if and only if it is definitionally equivalent to an extension of WS.