La aritmética acotada es un nombre colectivo para una familia de subteorías débiles de la aritmética de Peano . Estas teorías se obtienen típicamente al exigir que los cuantificadores estar limitadas en el axioma de inducción o postulados equivalentes (un cuantificador acotada es de la forma ∀ x ≤ t o ∃ x ≤ t , donde t es un término que no contiene x ). El propósito principal es caracterizar una u otra clase de complejidad computacional en el sentido de que una función es demostrablemente total si y solo si pertenece a una clase de complejidad dada. Además, las teorías de la aritmética acotada presentan contrapartes uniformes a los estándaressistemas de prueba proposicionales como el sistema de Frege y son, en particular, útiles para construir pruebas de tamaño polinómico en estos sistemas. La caracterización de las clases de complejidad estándar y la correspondencia con los sistemas de prueba proposicionales permite interpretar las teorías de la aritmética limitada como sistemas formales que capturan varios niveles de razonamiento factible (ver más abajo).
El enfoque fue iniciado por Rohit Jivanlal Parikh [1] en 1971, y posteriormente desarrollado por Samuel R. Buss . [2] y varios otros lógicos.
Teorías
Teoría de Cook
Stephen Cook introdujo una teoría de ecuaciones(para polinomialmente verificable) formalizar pruebas constructivas factibles (resp. polinomio-tiempo razonamiento). [3] El idioma deconsiste en símbolos de función para todos los algoritmos de tiempo polinomial introducidos inductivamente usando la caracterización de Cobham de funciones de tiempo polinómico. Los axiomas y derivaciones de la teoría se introducen simultáneamente con los símbolos del lenguaje. La teoría es ecuacional, es decir, sus declaraciones afirman solo que dos términos son iguales. Una extensión popular de es una teoria , una teoría ordinaria de primer orden. [4] Axiomas de son oraciones universales y contienen todas las ecuaciones demostrables en . Además, contiene axiomas que reemplazan los axiomas de inducción por fórmulas abiertas.
Teorías de Buss
Samuel Buss introdujo las teorías de primer orden de la aritmética acotada. [2] son teorías de primer orden con igualdad en el lenguaje , donde la función tiene la intención de designar (el número de dígitos en la representación binaria de ) y es . (Tenga en cuenta que, es decir permite expresar límites polinomiales en la longitud de bits de la entrada.) Los cuantificadores acotados son expresiones de la forma , , dónde es un término sin una ocurrencia de . Un cuantificador acotado está muy acotado si tiene la forma de por un término . Una fórmulaestá muy delimitado si todos los cuantificadores de la fórmula están muy delimitados. La jerarquía de y fórmulas se define inductivamente: es el conjunto de fórmulas muy delimitadas. es el cierre de bajo cuantificadores universales existenciales delimitados y fuertemente delimitados, y es el cierre de bajo cuantificadores existenciales universales acotados y fuertemente acotados. Las fórmulas limitadas capturan la jerarquía de tiempo polinomial : para cualquier, la clase coincide con el conjunto de números naturales definibles por en (el modelo estándar de aritmética) y dualmente . En particular,.
La teoría Consiste en una lista finita de axiomas abiertos denominados BASIC y el esquema de inducción polinomial
dónde .
Teorema de testigo de Buss
Buss (1986) demostró que teoremas de son atestiguados por funciones de tiempo polinomial. [2]
Teorema (Buss 1986)
Asumir que , con . Entonces, existe un-símbolo de función tal que .
Es más, lata -definir todas las funciones de tiempo polinomial. Es decir,-funciones definibles en son precisamente las funciones computables en tiempo polinomial. La caracterización se puede generalizar a niveles superiores de la jerarquía polinomial.
Correspondencia a los sistemas de prueba proposicionales
Las teorías de la aritmética acotada a menudo se estudian en relación con los sistemas de prueba proposicionales. De manera similar, como las máquinas de Turing son equivalentes uniformes de modelos de cálculo no uniformes como los circuitos booleanos , las teorías de la aritmética acotada pueden verse como equivalentes uniformes de los sistemas de prueba proposicionales. La conexión es particularmente útil para construcciones de demostraciones proposicionales breves. A menudo es más fácil probar un teorema en una teoría de la aritmética acotada y traducir la prueba de primer orden en una secuencia de pruebas breves en un sistema de prueba proposicional que diseñar pruebas proposicionales cortas directamente en el sistema de prueba proposicional.
La correspondencia fue presentada por S. Cook. [3]
Informalmente, un declaración se puede expresar de forma equivalente como una secuencia de fórmulas . Desde es un predicado coNP, cada puede a su vez formularse como una tautología proposicional (posiblemente conteniendo nuevas variables necesarias para codificar el cálculo del predicado ).
Teorema (Cook 1975)
Asumir que , dónde . Entonces tautologíastienen pruebas de Frege extendidas de tamaño polinomial . Además, las demostraciones son construibles mediante una función de tiempo polinomial y prueba este hecho.
Más, prueba el llamado principio de reflexión para el sistema de Frege extendido, lo que implica que el sistema de Frege extendido es el sistema de prueba más débil con la propiedad del teorema anterior: cada sistema de prueba que satisface la implicación simula Frege extendido.
Una traducción alternativa entre enunciados de segundo orden y fórmulas proposicionales dada por Jeff Paris y Alex Wilkie (1985) ha sido más práctica para capturar subsistemas de Frege extendido como Frege o Frege de profundidad constante. [5] [6]
Ver también
Referencias
- ^ Rohit J. Parikh. Existencia y viabilidad en aritmética, Jour. Symbolic Logic 36 (1971) 494–508.
- ^ a b c Buss, Samuel . "Aritmética acotada". Bibliopolis, Nápoles, Italia, 1986 .
- ^ a b Cook, Stephen (1975). "Pruebas factiblemente constructivas y el cálculo proposicional". Proc. Séptimo Simposio Anual ACM sobre Teoría de la Computación . págs. 83–97.
- ^ Krajíček, Jan; Pudlák, Pavel; Takeuti, G. (1991). "Aritmética acotada y la jerarquía polinomial". Anales de lógica pura y aplicada . págs. 143-153.
- ^ París, Jeff ; Wilkie, Alex (1985). "Contando problemas en aritmética acotada". Métodos en lógica matemática . 1130 . págs. 317–340.
- ^ Cook, Stephen ; Nguyen, Phuong (2010). "Fundamentos lógicos de la complejidad de la prueba". Perspectivas en lógica. Cambridge: Cambridge University Press. doi : 10.1017 / CBO9780511676277 . ISBN 978-0-521-51729-4. Señor 2589550 .( borrador de 2008 )
Otras lecturas
- Buss, Samuel , "Bounded Arithmetic", Bibliopolis, Nápoles, Italia, 1986.
- Cook, Stephen ; Nguyen, Phuong (2010), Fundamentos lógicos de la complejidad de la prueba , Perspectivas en la lógica, Cambridge: Cambridge University Press, doi : 10.1017 / CBO9780511676277 , ISBN 978-0-521-51729-4, MR 2589550( borrador de 2008 )
- Krajíček, Jan (1995), aritmética acotada, lógica proposicional y teoría de la complejidad , Cambridge University Press
- Krajíček, Jan, Proof Complexity , Cambridge University Press, 2019.
- Pudlák, Pavel (2013), "Fundamentos lógicos de las matemáticas y la complejidad computacional, una suave introducción", Springer Falta o vacío
|title=
( ayuda )
enlaces externos
- Prueba de la complejidad de la lista de correo.