I have read in John Corcoran's "Mutual Interpretability is not Definitional Equivalence" (meeting abstract, 1979, p. 430) that the following two "second-order" axiomatizations of Peano arithmetic (I will call them $T$ and $T'$) are mutually interpretable, but not definitionally equivalent. I don't see why. Here are the two formulations ('s' is the successor functor). See also Corcoran's note concerning definitional equivalence.


$s(x)\neq 0$;

$s(x) = s(y) \rightarrow x=y$;

$(P0 \land \forall x (Px \rightarrow Ps(x)) \rightarrow \forall yPy $


$x+1 \neq 0$;

$x+1 = y+1 \rightarrow x=y$;

$(P0 \land \forall x (Px \rightarrow Px+1) \rightarrow \forall yPy$

Recall that mutual interpretability is just like definitional equivalence except that the two definitional extensions $T^+$ and $T'^+$ need not be logically equivalent. The only requirement is that $T^+ \vdash T'$ and $T'^+ \vdash T$.

  • $\begingroup$ This is all a bit unclear. (1) What is [Corcoran 1981]? The reference is not very useful without a title. (2) Corcoran is using a non-standard definition of "mutual interpretability" here, which makes the question a bit confusing. (3) What are the languages of $T$ and $T'$? It seems $T$ has a unary function symbol $s$ and a constant symbol $0$. Does $T'$ have a binary function symbol $+$ and two constant symbols $0$ and $1$? Is $P$ a second-order variable that is implicitly universally quantified? When we talk about "definitional extensions", are we allowed to use second-order definitions? $\endgroup$ Oct 4, 2022 at 13:13
  • $\begingroup$ @AlexKruckman (1) It's an abstract from the 1979 meeting of the ASL (JSL, 46, 2, 1981, p. 430). It seems like the paper has never been published. (2) The notion used by Corcoran is the notion of mutual interpretability introduced by Tarski in his 1953 monograph on undecidable theories. (3) Corcoran says that these are "two standard second-order axiomatizations of Peano arithmetic". So I suppose that P is a second-order variable as you say. By definitional extension of a theory he just means adding to it defining axioms for new predicates, functors and individual constants. $\endgroup$
    – Soennecken
    Oct 4, 2022 at 13:31
  • 2
    $\begingroup$ Maybe similar example $\endgroup$ Oct 4, 2022 at 13:48
  • $\begingroup$ Possible source $\endgroup$ Oct 4, 2022 at 13:53


You must log in to answer this question.

Browse other questions tagged .