El teorema de base baja es uno de varios teoremas de base en la teoría de la computabilidad , cada uno de los cuales muestra que, dado un subárbol infinito del árbol binario , es posible encontrar un camino infinito a través del árbol con propiedades de computabilidad particulares. El teorema de la base baja, en particular, muestra que debe haber un camino que sea bajo ; es decir, el salto de Turing del camino es el equivalente de Turing al problema de detención .
El teorema de base baja establece que toda clase no vacía en (ver jerarquía aritmética ) contiene un conjunto de bajo grado (Soare 1987:109). Esto equivale, por definición, a la afirmación de que cada subárbol computable infinito del árbol binario tiene un camino infinito de bajo grado.
La prueba utiliza el método de forzar con clases (Cooper 2004:330). Hájek y Kučera (1989) demostraron que la base baja es demostrable en el sistema formal de aritmética conocido como .
El argumento del forzamiento también puede formularse explícitamente de la siguiente manera. Para un conjunto X ⊆ω, sea f ( X ) = Σ { i }( X )↓ 2 − i , donde { i }( X )↓ significa que la máquina de Turing i se detiene en X (con la suma sobre todos esos i ). Entonces, para cada S ⊆2 ω no vacío (lightface) , el (único) X ∈ S que minimiza f ( X ) tiene un grado de Turing bajo. Esto se debe a que X satisface { i }( X )↓ ⇔ ∀ Y ∈ S ({ i }( Y )↓ ∨ ∃ j < i ({ j }( Y )↓ ∧ ¬{ j }( X )↓)), entonces la función i ↦ { i }( X )↓ se puede calcular por inducción en i ; tenga en cuenta que ∀ Y ∈ S φ( Y ) es para cualquier conjunto φ. En otras palabras, si una máquina se detiene en X es forzada por una condición finita, que permite que X ′ = .
Una aplicación del teorema de base baja es construir terminaciones de teorías efectivas de modo que las terminaciones tengan un grado de Turing bajo. Por ejemplo, el teorema de la base baja implica la existencia de grados de PA estrictamente por debajo .
