fórmula de harrop

En lógica intuicionista , las fórmulas de Harrop , denominadas así en honor a Ronald Harrop, son la clase de fórmulas definidas inductivamente de la siguiente manera: ^{[1] [2] [3]}

• Las fórmulas atómicas son Harrop, incluida la falsedad (⊥);
• ${\displaystyle A\wedge B}$se proporciona Harrop y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \neg F}$es Harrop para cualquier fórmula bien formada ; ${\displaystyle F}$
• ${\displaystyle F\rightarrow A}$¿Se proporciona Harrop ? y es cualquier fórmula bien formada; ${\displaystyle A}$ ${\displaystyle F}$
• ${\displaystyle \forall x.A}$¿Se proporciona Harrop ? ${\displaystyle A}$

Al excluir la disyunción y la cuantificación existencial (excepto en el antecedente de implicación), se evitan los predicados no constructivos , lo que tiene beneficios para la implementación informática.

Discusión

Las fórmulas de Harrop "se portan bien" también en un contexto constructivo. Por ejemplo, en aritmética de Heyting , las fórmulas de Harrop satisfacen una equivalencia clásica que generalmente no se satisface en lógica constructiva: ^[1] ${\displaystyle {\mathsf {HA}}}$

${\displaystyle \neg \neg A\leftrightarrow A.}$

Sin embargo, hay afirmaciones que son independientes, lo que significa que son afirmaciones simples para las cuales el medio excluido no es demostrable. De hecho, si bien la lógica intuicionista es válida para cualquiera , la disyunción no será la de Harrop. ${\displaystyle \Pi _{1}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \forall x.A}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle \neg \neg (P\lor \neg P)}$ ${\displaystyle P}$

Fórmulas hereditarias de Harrop y programación lógica.

Una definición más compleja de fórmulas hereditarias de Harrop se utiliza en programación lógica como una generalización de las cláusulas de Horn y constituye la base del lenguaje λProlog . Las fórmulas hereditarias de Harrop se definen en términos de dos (a veces tres) conjuntos recursivos de fórmulas. En una formulación: ^[4]

• Las fórmulas atómicas rígidas, es decir, constantes o fórmulas , son hereditarias de Harrop; ${\displaystyle r}$ ${\displaystyle r(t_{1},...,t_{n})}$
• ${\displaystyle A\wedge B}$es hereditario Harrop proporcionado y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \forall x.A}$es hereditario Harrop siempre que sea; ${\displaystyle A}$
• ${\displaystyle G\rightarrow A}$Harrop es hereditaria, siempre que sea rígidamente atómica y tenga una fórmula G. ${\displaystyle A}$ ${\displaystyle G}$

Las fórmulas G se definen de la siguiente manera: ^[4]

• Las fórmulas atómicas son G -fórmulas, incluida la verdad (⊤);
• ${\displaystyle A\wedge B}$se proporciona una fórmula G y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle A\vee B}$se proporciona una fórmula G y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \forall x.A}$es una fórmula G siempre que sea; ${\displaystyle A}$
• ${\displaystyle \exists x.A}$es una fórmula G siempre que sea; ${\displaystyle A}$
• ${\displaystyle H\rightarrow A}$es una fórmula G proporcionada y es hereditaria Harrop. ${\displaystyle A}$ ${\displaystyle H}$

Historia

Las fórmulas de Harrop fueron introducidas alrededor de 1956 por Ronald Harrop e independientemente por Helena Rasiowa . ^[2] Se utilizan variaciones del concepto fundamental en diferentes ramas de la matemática constructiva y la programación lógica .

Ver también

• Realizabilidad

Referencias

1. Dummett, Michael (2000). Elementos del intuicionismo (2ª ed.). Prensa de la Universidad de Oxford . pag. 227.ISBN​ 0-19-850524-8.
2. AS Troelstra ; H. Schwittenberg (27 de julio de 2000). Teoría básica de la prueba . Prensa de la Universidad de Cambridge . ISBN 0-521-77911-1.
3. Ronald Harrop (1956). "Sobre disyunciones y enunciados existenciales en sistemas de lógica intuicionista". Annalen Matemáticas . 132 (4): 347–361. doi :10.1007/BF01360048. S2CID  120620003.
4. Dov M. Gabbay , Christopher John Hogger, John Alan Robinson , Manual de lógica en inteligencia artificial y programación lógica: programación lógica , Oxford University Press , 1998, p 575, ISBN 0-19-853792-1