Teorem med låg bas

Den låga bassatsen är en av flera bassatser inom beräkningsbarhetsteorin, som var och en visar att, givet ett oändligt delträd av det binära trädet $2^{<\omega }$ , är det möjligt att hitta en oändlig väg genom trädet med särskilda beräkningsegenskaper. Särskilt lågbassatsen visar att det måste finnas en väg som är låg ; det vill säga, banans Turinghopp är Turing ekvivalent med stoppproblemet $\emptyset '$ .

Uttalande och bevis

Den låga bassatsen säger att varje icke-tom $\Pi _{1}^{0}$ klass i $2^{\omega }$ (se aritmetisk hierarki ) innehåller en uppsättning av låg grad ( Soare 1987:109). Detta motsvarar per definition påståendet att varje oändligt beräkningsbart underträd i det binära trädet $2^{<\omega }$ har en oändlig väg av låg grad.

Beviset använder metoden att forcera med $\Pi _{1}^{0}$ klasser (Cooper 2004:330). Hájek och Kučera (1989) visade att den låga basen är bevisbar i det formella aritmetiska systemet känt som ${\text{I-}}\Sigma _{1}$ .

Det tvingande argumentet kan också uttryckligen formuleras enligt följande. För en mängd X ⊆ω, låt f ( X ) = Σ _{{ i }( X )↓} 2 ^{− i} , där { i }( X )↓ betyder att Turingmaskinen i stannar på X (med summan över alla sådana i ). Sedan, för varje icke-tom (lightface) $\Pi _{1}^{0}$ S ⊆2 ^ω , har den (unika) X ∈ S - minimeringen f ( X ) en låg turinggrad. För att se detta, { i }( X )↓ ⇔ ∀ Y ∈ S ({ i }( Y )↓ ∨ ∃ j < i ({ j }( Y )↓ ∧ ¬{ j }( X )↓)), som kan beräknas från 0′ genom induktion på i ; Observera att ∀ Y ∈ S φ( Y ) är $\Sigma _{1}^{0}$ för $\Sigma _{1}^{0}$ φ. Med andra ord, huruvida en maskin stannar på X tvingas av ett ändligt tillstånd, med tillåter X ′ = 0′ .

Ansökan

En tillämpning av lågbassatsen är att konstruera kompletteringar av effektiva teorier så att kompletteringarna har låg Turinggrad. Till exempel antyder lågbassatsen att det finns PA-grader strikt under $\emptyset '$ .

•     Cenzer, Douglas (1999). " $\Pi _{1}^{0}$ klasser i beräkningsbarhetsteori" . I Griffor, Edward R. (red.). Handbok i beräkningsteori . Hingst. Logik hittad. Matematik. Vol. 140. Nord-Holland. s. 37–85 . ISBN 0-444-89882-4 . MR 1720779 . Zbl 0939.03047 .
•   Cooper, S. Barry (2004). Beräkningsbarhetsteori . Chapman och Hall/CRC. ISBN 1-58488-237-9 . .
•   Hájek, Petr; Kučera, Antonín (1989). "Om rekursionsteori i IΣ1". Journal of Symbolic Logic . 54 (2): 576–589. doi : 10.2307/2274871 . JSTOR 2274871 .
•     Jockusch, Carl G., Jr.; Soare, Robert I. (1972). "Π(0, 1) Teoriklasser och grader" . Transaktioner från American Mathematical Society . 173 : 33–56. doi : 10.1090/s0002-9947-1972-0316227-0 . ISSN 0002-9947 . JSTOR 1996261 . Zbl 0262.02041 . Originalpublikationen, inklusive ytterligare förtydligande prosa.
•    Nies, André (2009). Beräkningsbarhet och slumpmässighet . Oxford Logic Guides. Vol. 51. Oxford: Oxford University Press. ISBN 978-0-19-923076-1 . Zbl 1169.03034 . Sats 1.8.37.
•    Soare, Robert I. (1987). Rekursivt uppräknade mängder och grader. En studie av beräkningsbara funktioner och beräkningsbart genererade uppsättningar . Perspektiv i matematisk logik. Berlin: Springer-Verlag . ISBN 3-540-15299-7 . Zbl 0667.03030 .