2
$\begingroup$

In Kleene ''Introduction to Metamathematics'' 1971 on pp.420 he shows that if we have a formal system which for some formula $M(x)$ can prove the statement $\exists x M(x)$ then one can introduce a new formal system with one more sort of variables and corresponding new axioms and axiom schemata where the newly added sort intuitively corresponds to objects for which $M(x)$ is valid. Then one can show that this new sort is eliminable in a sense that new obtained formal system is equivalent to the previous one because there is an effective (computable) process of translation of formulas and certain provability conditions between formulas of different systems hold.

Now, I am interested in the reverse process. Assume we have some formal theory that has more than one sort of variables. Is it possible to reduce the number of sorts such that the resulting formal system is in some sense equivalent to the original one? I tried looking it up in books and on the internet, but could not find precise statements about this. For example, one idea that I found is that for each sort that wants to be removed I can just add a new predicate which intuitively represents the statement "this object is (was) from this sort". But I am not sure how to make it precise, especially what would be the precise definition of the new formal system being equivalent to the original one. I know that I want the new system to be intuitively not stronger and not weaker.

For example, in Kleene's book when he decides on the definition of equivalence he imposes one of the conditions to be that if $E$ is formula in the new system $S_2$ and $E'$ is the corresponding translation back to formal system $S_1$ then $E \iff E'$ is provable in $S_2$. But I do not see how that can work in the current situation because consider expression that contains the sort I want to eliminate. Then, it is a formula in $S_1$ but is not a formula in $S_2$ (because it does not contain that sort anymore). So, $E \iff E'$ cannot even be expressed in $S_2$. Similarly, if there is a formula that has a new predicate symbol that expresses that some variable is a member of some sort using newly defined predicate then this is expressible in $S_2$ but is not expressible in $S_1$, so $E \iff E'$ cannot be expressed in $S_1$ as well.

I hope I made my intentions clear and please let me know what you think about it. I would appreciate any kind of help, advice, references and so on.

$\endgroup$
  • $\begingroup$ Which multisortred systems interest you? Writing it down in generality would be tedious, but this can probably be clear with an example. $\endgroup$ – user210229 Feb 14 '19 at 12:17
  • $\begingroup$ @MattF. Thanks for the comment! Honestly, I was not thinking about specific multiple sort system, but, say, for example: going from two sorted category theory (where one sort represents objects and other sort represents arrows) to one sorted version. $\endgroup$ – Daniels Krimans Feb 15 '19 at 3:46
1
+250
$\begingroup$

Consider category theory as an example, and the informal sentence "every object has a morphism that goes from the object to itself".

In a two-sorted version of category theory ($S_2$), we use the language $(\mathcal{M},\mathcal{O},R,s,t)$. Here:

  • $\mathcal{M}$ and $\mathcal{O}$ are the sorts for morphisms and objects
  • $R$ is the ternary relation determining when one morphism is the composition of two others
  • $s$ and $t$ are the functions from morphisms to objects identifying their source and target.

So in $S_2$ we write the original sentence as $$(**) \ \ \forall x \in \mathcal{O}\ \exists y \in \mathcal{M}\ s(y)=x \mathbin\& t(y)=x$$

In a one-sorted version of category theory ($S_1$), we use the language $(\mathcal{C},M,O,R,S,T)$. Here

  • $\mathcal{C}$ is the whole category, with both morphisms and objects
  • $M$ and $O$ are unary relations identifying morphisms and objects
  • $R$ is the ternary relation determining when one morphism is the composition of two others
  • $S$ is a binary relation true when the first argument is a morphism and the second argument is its source
  • $T$ is a binary relation true when the first argument is a morphism and the second argument is its target

So in $S_1$ we write the original sentence as $$(*)\ \ \forall x(O(x) \implies \exists y\ M(y) \mathbin\& S(y,x) \mathbin\& T(y,x))$$

Since $(*)$ and $(**)$ are sentences in different formal systems, we never prove them directly equivalent.

Instead, we show that we have a mapping $'$ taking formulas in $S_1$ to formulas in $S_2$, and a mapping $^\wedge$ taking formulas in $S_2$ to formulas in $S_1$. With such mappings, $(*)'$ and $(**)$ are sentences in $S_2$ which are equivalent in $S_2$. Similarly, $(**)^\wedge$ and $(*)$ are sentences in $S_1$ which are equivalent in $S_1$.

In general, we can prove that for all formulas in the appropriate languages:

$$\vdash_1 E \iff (E')^\wedge$$ $$\vdash_2 \eta \iff (\eta^\wedge)'$$ $$E \vdash_1 F \text{ iff } E' \vdash_2 F'$$ $$\eta \vdash_2 \phi \text{ iff } \eta^\wedge \vdash_1 \phi^\wedge$$

These are statements of pure symbol-manipulation, where $'$ and $\wedge$ and $\vdash_1$ and $\vdash_2$ are all defined as manipulations of symbols or their arithmetical equivalents. So we can prove these claims in Peano arithmetic or any other convenient theory for metamathematics. And this establishes the equivalence of the two systems.

$\endgroup$
  • $\begingroup$ Thanks! That is a very interesting answer and sounds exactly what I wanted. Can you please give some intuition behind why we choose those 4 conditions to characterize when two formal theories are equivalent. For example, why instead of $(E')$^ requiring to be $E$ we require logical equivalence of these formulas. Also why for the third/fourth conditions we have if and only if instead of if the non-translated version is provable then translated version is provable because I do not see how can one prove the other direction if one doesn't know the backward translation. $\endgroup$ – Daniels Krimans Feb 17 '19 at 3:28
  • $\begingroup$ If you write down rules for $’$ and $\wedge$ in the above example you will see that they are not exact inverses, but only up to logical equivalence; that’s the usual situation and the definition reflects that. Meanwhile, I don’t understand your last comment. $\endgroup$ – user210229 Feb 17 '19 at 15:19
  • $\begingroup$ Nevermind, I think I got it. Thank you $\endgroup$ – Daniels Krimans Feb 17 '19 at 19:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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