Π⁰₁ classes and degrees of theories 论文

1972Transactions of the American Mathematical Society引用 352
Computability, Logic, AI Algorithmssemigroups and automata theoryLogic, programming, and type systems

摘要

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>