Π⁰₁ classes and degrees of theories

Abstract

Using the methods of recursive function theory we derive several results about the degrees of unsolvability of members of certain <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Pi 1 Superscript 0"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Π<!-- Π --></mml:mi> <mml:mn>1</mml:mn> <mml:mn>0</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Pi _1^0</mml:annotation> </mml:semantics> </mml:math> </inline-formula> classes of functions (i.e. degrees of branches of certain recursive trees). As a special case we obtain information on the degrees of consistent extensions of axiomatizable theories, in particular effectively inseparable theories such as Peano arithmetic, <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper P"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">P</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {P}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. For example: THEOREM 1. <italic>If a degree <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold a"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">a</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {a}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> contains a complete extension of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper P"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">P</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {P}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, then every countable partially ordered set can be embedded in the ordering of degrees</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="less-than-or-slanted-equals bold a"> <mml:semantics> <mml:mrow> <mml:mo>⩽<!-- ⩽ --></mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">a</mml:mi> </mml:mrow> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">\leqslant {\mathbf {a}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. (This strengthens a result of Scott and Tennenbaum that no such degree <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold a"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">a</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {a}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is a minimal degree.) THEOREM 2. <italic>If <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper T"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">T</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {T}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is an axiomatizable, essentially undecidable theory, and if <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="left-brace bold a Subscript n Baseline right-brace"> <mml:semantics> <mml:mrow> <mml:mo fence="false" stretchy="false">{</mml:mo> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">a</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>n</mml:mi> </mml:msub> </mml:mrow> <mml:mo fence="false" stretchy="false">}</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\{ {{\mathbf {a}}_n}\}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is a countable sequence of nonzero degrees, then <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper T"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">T</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {T}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> has continuum many complete extensions whose degrees are pairwise incomparable and incomparable with each</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold a Subscript n"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">a</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>n</mml:mi> </mml:msub> </mml:mrow> <mml:annotation encoding="application/x-tex">{{\mathbf {a}}_n}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. THEOREM 3. <italic>There is a complete extension <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper T"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">T</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {T}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper P"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">P</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {P}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> such that no nonrecursive arithmetical set is definable in</italic> <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper T"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">T</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {T}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. THEOREM 4. <italic>There is an axiomatizable, essentially undecidable theory <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper T"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">T</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {T}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> such that any two distinct complete extensions of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper T"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">T</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {T}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> are Turing incomparable</italic>. THEOREM 5. <italic>The set of degrees of consistent extensions of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="bold upper P"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="bold">P</mml:mi> </mml:mrow> </mml:mrow> <mml:annotation encoding="application/x-tex">{\mathbf {P}}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is meager and has measure zero</italic>.