3
$\begingroup$

It's relatively standard to add a sort of sets over some base theory and supplement the axioms with comprehension principles as in second order arithmetic.

Is there a nice way to do this if your initial theory has multiple sorts? For instance, if you started with a theory with a sort for natural numbers and a sort for reals?

Of course, one could introduce comprehension axioms that require a formula for each sort but that seems kinda ugly and I don't see how to extend that to infinitely many sorts. Alternatively, one could define sorts for each finite (or more) product of sorts whose elements are members of that product but I wonder if but you lose some degree of power w/o sets containing both kinds of elements?

Thats a little vague but if I knew how to state it formally I wouldn't be asking.

Is there some elegant approach I'm unaware of for this kind of thing?

$\endgroup$
1
  • 1
    $\begingroup$ The initial motivation behind the question was wondering if how you might formulate reasoning inductively defined objects like finite trees using a non-type theory approach that has the full strength of second order logic without using godel codes (in other words you have a bunch of sorts each of which comes with some construction operations and axioms allowing for induction with respect to the induced ordering). But I'm now just curious about this generally. $\endgroup$ Nov 21, 2022 at 18:08

1 Answer 1

6
$\begingroup$

Let me argue that some care is needed, since one approach that might naively seem reasonable at first is definitely less powerful than we might desire.

Namely, what I claim is that it is strictly less powerful to allow second-order resources only over each sort separately, without any second-order relations spanning the sorts.

Let me prove this by illustrating with an example that my PhD student Nuno Maia and I had made a few years ago. Namely, consider the two-sorted model consisting of two copies of the standard model of arithmetic $$\langle\newcommand\N{\mathbb{N}}\N_0,+_0,\cdot_0,<_0,\N_1,+_1,\cdot_1,<_1\rangle$$ That is, each $\N_i$ is the standard model $\N$, with the usual addition and multiplication structure. Let us assume that each sort has its own separate quantifiers and variable symbols, which is one of the standard ways to treat sorts.

We can prove that every first-order assertion $\varphi(\vec x,\vec y)$ in this two-sorted langauge, where the variables in $\vec x$ have sort $0$ and those in $\vec y$ have sort $1$, is equivalent to a Boolean combination of assertions $\varphi_0(\vec x)$ about the sort $0$ part only and assertions $\varphi_1(\vec y)$ solely about the sort $1$ part. This is true for atomic assertions and is preserved by Boolean combinations, and by quantifiers, precisely because the quantifiers are themselves sorted.

In particular, one cannot define the isomorphism of $\N_0$ with $\N_1$ in the two-sorted structure, since the isomorphism cannot be pulled apart this way into separate statements about the domain and range.

Now, the interesting further observation is that if one adds the second-order resources, but only to each sort separately, then you still can't define the isomorphism. That is, let's add sorted second-order quantifiers, with sort $0$ quantifiers quantifying over subsets and relations on $\N_0$ only, and others for second-order subsets and relations on $\N_1$. The point is that the induction argument still goes through.

In particular, and this was our main focus, one cannot prove the Dedekind categoricity proof in sorted second-order logic. That is, we can have a two-sorted model $$\langle\N_0,+_0,\cdot_0,<_0,\N_1,+_1,\cdot_1,<_1\rangle$$ where each sort $\N_i$ satisfies the second-order Peano axioms, but there is no second-order definable isomorphism between them, if the second-order resources are contained in each sort separately.

This example is just the sort of recursive-definition situation that you describe in your question and comment, since the full categoricity argument of Dedekind is an induction in second-order logic.

That is, for the full categoricity result, which shows that there is only one model of second-order PA up to isomorphism, one uses the second-order resource spanning the sorts. Namely, one refers to the various partial isomorphisms that match the initial segments of one model with the other, and then prove (by second-order induction) that these cohere and that one can extend the to the first-point missed on either side, so collectively they define an isomorphism.

$\endgroup$
2
  • 1
    $\begingroup$ Thanks so much! But suppose I introduce one sort of sets and two membership relations (one for each sort) so my comprehension axioms all take two formula. Is that going to be as powerful as introducing a sort of pairs and then sets of those pairs? Also any thoughts on the most elegant way to do this that gives the maximal power (like if u want to do automated reasoning Godel numbers get kinda clunky). $\endgroup$ Nov 21, 2022 at 22:55
  • $\begingroup$ A set of pairs seems to be the interpretatively the same as a single binary relation Rab, where a is from one sort and b from another. This is exactly the kind of cross-sort relation that I am speaking of in my answer. My preference would be to use the binary cross-sort relation, since no new objects are introduced. And it does make plain the difference between monadic second-order and binary cross-sort relations. I would similarly find it elegant simply to allow cross-sort relations of any arity (with subarities in each sort separately). This is less than full coding of finite sequences. $\endgroup$ Nov 21, 2022 at 23:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.