Traducción de Friedman
En lógica matemática , la traducción de Friedman es una cierta transformación de fórmulas intuicionistas . Entre otras cosas, puede usarse para mostrar que los teoremas Π 0 2 de varias teorías de primer orden de la matemática clásica son también teoremas de la matemática intuicionista. Lleva el nombre de su descubridor, Harvey Friedman .
Definición
Deje que A y B sean fórmulas intuicionistas, donde no variable libre de B se cuantifica en A . La traducción A B se define mediante la sustitución de cada subfórmula atómica C de A por C ∨ B . A los efectos de la traducción, ⊥ también se considera una fórmula atómica, por lo que se reemplaza con ⊥ ∨ B (que es equivalente a B ). Tenga en cuenta que ¬ A se define como una abreviatura de A → ⊥, por lo tanto (¬ A ) B = AB → B .
Solicitud
La traducción de Friedman se puede utilizar para mostrar el cierre de muchas teorías intuicionistas bajo la regla de Markov y para obtener resultados de conservadurismo parcial . La condición clave es que las oraciones de la lógica sean decidibles, permitiendo que los teoremas no cuantificados de las teorías intuicionista y clásica coincidan.
Por ejemplo, si A se puede demostrar en la aritmética de Heyting (HA), entonces A B también se puede demostrar en HA. [1] Por otra parte, si A es un Σ 0 1 fórmula de L , entonces A B es en HA equivalente a A ∨ B . Esto implica que:
- La aritmética de Heyting se cierra bajo la regla de Markov recursiva primitiva (MP PR ): si la fórmula ¬¬ A es demostrable en HA, donde A es una fórmula Σ 0 1 , entonces A también es demostrable en HA.
- La aritmética de Peano es Π 0 2 -conservadora sobre la aritmética de Heyting: si la aritmética de Peano demuestra una Π 0 2- fórmula A , entonces A ya es demostrable en HA.
Ver también
Notas
- ^ Harvey Friedman. Funciones clásicas e intuicionistas probables recursivas. En Scott, DS y Muller, GH Editors, Higher Set Theory, Volumen 699 de Lecture Notes in Mathematics, Springer Verlag (1978), págs. 21-28. doi : 10.1007 / BFb0103100
