aritmética acotada

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 generalmente se obtienen exigiendo que los cuantificadores estén acotados en el axioma de inducción o postulados equivalentes (un cuantificador acotado tiene la forma ∀ x  ≤  t o ∃ x  ≤  t , donde t es un término que no contiene  x ). El objetivo principal es caracterizar una u otra clase de complejidad computacional en el sentido de que una función es demostrablemente total si y sólo si pertenece a una clase de complejidad determinada. Además, las teorías de la aritmética acotada presentan contrapartes uniformes de los sistemas de prueba proposicionales estándar , 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 clases de complejidad estándar y la correspondencia con sistemas de prueba proposicionales permite interpretar las teorías de la aritmética acotada 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.

Teorias

La teoría ecuacional de Cook.

Stephen Cook introdujo una teoría ecuacional (para polinomialmente verificable) que formaliza pruebas constructivas factibles (resp. razonamiento en tiempo polinomial). ^[3] El lenguaje de consta de símbolos de funciones para todos los algoritmos de tiempo polinomial introducidos inductivamente utilizando la caracterización de funciones de tiempo polinomial de Cobham. 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 enunciados afirman únicamente que dos términos son iguales. Una extensión popular de es una teoría , una teoría ordinaria de primer orden. ^[4] Los axiomas de son oraciones universales y contienen todas las ecuaciones demostrables en . Además, contiene axiomas que reemplazan los axiomas de inducción para fórmulas abiertas. ${\displaystyle PV}$ ${\displaystyle PV}$ ${\displaystyle PV}$ ${\displaystyle PV_{1}}$ ${\displaystyle PV_{1}}$ ${\displaystyle PV}$ ${\displaystyle PV_{1}}$

Las teorías de primer orden 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 pretende 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 , donde es un término sin que aparezca . Un cuantificador acotado está fuertemente acotado si tiene la forma de para un término . Una fórmula está fuertemente acotada si todos los cuantificadores de la fórmula están fuertemente acotados. La jerarquía de las fórmulas y se define inductivamente: es el conjunto de fórmulas claramente acotadas. es el cierre de cuantificadores existenciales poco acotados y universales muy acotados, y es el cierre de cuantificadores existenciales poco acotados y universales muy acotados. Las fórmulas acotadas capturan la jerarquía de tiempo polinomial : para cualquiera , la clase coincide con el conjunto de números naturales definibles por in (el modelo estándar de aritmética) y dualmente . En particular, . ${\displaystyle S_{2}^{i}}$ ${\displaystyle S_{2}^{i}}$ ${\displaystyle L=\{0,S,+,\cdot ,\sharp ,|x|,\lfloor {\frac {x}{2}}\rfloor \}}$ ${\displaystyle |x|}$ ${\displaystyle \lceil \log(x+1)\rceil }$ ${\displaystyle x}$ ${\displaystyle x\sharp y}$ ${\displaystyle 2^{|x|\cdot |y|}}$ ${\displaystyle |x\sharp x|\sim |x|^{2}}$ ${\displaystyle \sharp }$ ${\displaystyle \exists x\leq t\dots :=\exists x(x\leq t\wedge \dots )}$ ${\displaystyle \forall x\leq t\dots :=\forall x(x\leq t\rightarrow \dots )}$ ${\displaystyle t}$ ${\displaystyle x}$ ${\displaystyle t}$ ${\displaystyle |s|}$ ${\displaystyle s}$ ${\displaystyle \phi }$ ${\displaystyle \Sigma _{i}^{b}}$ ${\displaystyle \Pi _{i}^{b}}$ ${\displaystyle \Sigma _{0}^{b}=\Pi _{0}^{b}}$ ${\displaystyle \Sigma _{i+1}^{b}}$ ${\displaystyle \Pi _{i}^{b}}$ ${\displaystyle \Pi _{i+1}^{b}}$ ${\displaystyle \Sigma _{i}^{b}}$ ${\displaystyle i\geq 1}$ ${\displaystyle \Sigma _{i}^{P}}$ ${\displaystyle \Sigma _{i}^{b}}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \Pi _{i}^{b}=\Pi _{i}^{P}(\mathbb {N} )}$ ${\displaystyle NP=\Sigma _{1}^{b}(\mathbb {N} )}$

La teoría consta de una lista finita de axiomas abiertos denominados BÁSICO y el esquema de inducción polinomial. ${\displaystyle S_{2}^{i}}$

${\displaystyle \phi (0)\wedge \forall x\leq a(\phi (\lfloor {\frac {x}{2}}\rfloor )\rightarrow \phi (x))\rightarrow \phi (a)}$

dónde . ${\displaystyle \phi \in \Sigma _{i}^{b}}$

Teorema de testigos de Buss

Buss (1986) demostró que los teoremas de son atestiguados por funciones de tiempo polinómico. ^[2] ${\displaystyle \Sigma _{1}^{b}}$ ${\displaystyle S_{2}^{1}}$

Teorema (Buss 1986)

Supongamos que , con . Entonces, existe un símbolo de función tal que . ${\displaystyle S_{2}^{1}\vdash \forall x\exists y\phi (x,y)}$ ${\displaystyle \phi \in \Sigma _{1}^{b}}$ ${\displaystyle PV}$ ${\displaystyle f}$ ${\displaystyle PV\vdash \forall x\phi (x,f(x))}$

Además, puede definir todas las funciones de tiempo polinomial. Es decir, las funciones definibles en son precisamente las funciones computables en tiempo polinomial. La caracterización se puede generalizar a niveles superiores de la jerarquía polinómica. ${\displaystyle S_{2}^{1}}$ ${\displaystyle \Sigma _{1}^{b}}$ ${\displaystyle \Sigma _{1}^{b}}$ ${\displaystyle S_{2}^{1}}$

Correspondencia a sistemas de prueba proposicionales

Las teorías de la aritmética acotada a menudo se estudian en relación con sistemas de prueba proposicionales. De manera similar a como las máquinas de Turing son equivalentes uniformes de modelos de computación 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 cortas. A menudo es más fácil demostrar un teorema en una teoría de aritmética acotada y traducir la demostración de primer orden en una secuencia de demostraciones breves en un sistema de demostración proposicional que diseñar demostraciones proposicionales breves directamente en el sistema de demostración proposicional.

La correspondencia fue presentada por S. Cook. ^[3]

De manera informal, una declaración puede expresarse de manera equivalente como una secuencia de fórmulas . Dado que es un predicado coNP, cada uno puede formularse a su vez como una tautología proposicional (que posiblemente contenga nuevas variables necesarias para codificar el cálculo del predicado ). ${\displaystyle \Pi _{1}^{b}}$ ${\displaystyle \forall x\Phi (x)}$ ${\displaystyle \Phi _{n}(x):=\forall x(|x|=n\rightarrow \Phi (x))}$ ${\displaystyle \Phi _{n}(x)}$ ${\displaystyle \Phi _{n}(x)}$ ${\displaystyle ||\phi ||^{n}}$ ${\displaystyle \Phi _{n}}$

Teorema (Cook 1975)

Supongamos que , dónde . Entonces las tautologías tienen pruebas de Frege extendidas de tamaño polinomial . Además, las pruebas se pueden construir mediante una función de tiempo polinomial y prueban este hecho. ${\displaystyle S_{2}^{1}\vdash \forall x\Phi (x)}$ ${\displaystyle \Phi \in \Pi _{1}^{b}}$ ${\displaystyle ||\phi ||^{n}}$ ${\displaystyle PV}$

Además, demuestra 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. ${\displaystyle S_{2}^{1}}$

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

• Complejidad de la prueba
• Complejidad computacional
• Lógica matemática
• Teoría de la prueba
• Clases de complejidad
• NP (complejidad)
• cNP

Referencias

1. Rohit J. Parikh. Existencia y viabilidad en aritmética, Jour. Lógica simbólica 36 (1971) 494–508.
2. Buss, Samuel . "Aritmética acotada". Bibliopolis, Nápoles, Italia, 1986 .
3. Cook, Stephen (1975). "Pruebas factibles constructivas y cálculo proposicional". Proc. Séptimo Simposio Anual ACM sobre Teoría de la Computación . págs. 83–97.
4. Krajíček, enero; Pudlák, Pavel; Takeuti, G. (1991). "Aritmética acotada y jerarquía polinómica". Anales de lógica pura y aplicada . págs. 143-153.
5. París, Jeff ; Wilkie, Alex (1985). "Problemas de conteo en aritmética acotada". Métodos en lógica matemática . vol. 1130. págs. 317–340.
6. Cocinero, Stephen ; Nguyen, Phuong (2010). "Fundamentos lógicos de la complejidad de la prueba". Perspectivas en lógica. Cambridge: Prensa de la Universidad de Cambridge. doi :10.1017/CBO9780511676277. ISBN 978-0-521-51729-4. SEÑOR  2589550.(borrador de 2008)

Otras lecturas

• Buss, Samuel , "Aritmética acotada", Bibliopolis, Nápoles, Italia, 1986.
• Cocinero, Esteban ; 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)
• Krajíček, Jan (1995), Aritmética limitada, lógica proposicional y teoría de la complejidad , Cambridge University Press
• Krajíček, Jan, Complejidad de la prueba, Cambridge University Press, 2019.
• Pudlák, Pavel (2013), Fundamentos lógicos de las matemáticas y complejidad computacional, una suave introducción , Springer

enlaces externos

• Lista de correo de complejidad de prueba.