Fórmula de Harrop

En la lógica intuicionista , las fórmulas de Harrop , llamadas 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 de Harrop, incluida la falsedad (⊥);
• ${\displaystyle A\wedge B}$Harrop proporciona y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \neg F}$es Harrop para cualquier fórmula bien formada ; ${\displaystyle F}$
• ${\displaystyle F\rightarrow A}$es Harrop siempre que sea, y es cualquier fórmula bien formada; ${\displaystyle A}$ ${\displaystyle F}$
• ${\displaystyle \forall x.A}$Harrop lo proporciona . ${\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 también se comportan bien en un contexto constructivo. Por ejemplo, en la aritmética de Heyting , las fórmulas de Harrop satisfacen una equivalencia clásica que no se cumple generalmente en la lógica constructiva: ^[1] ${\displaystyle {\mathsf {HA}}}$

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

Sin embargo, existen enunciados que son independientes, es decir, enunciados simples para los que no se puede demostrar el término medio excluido . De hecho, si bien la lógica intuicionista demuestra que para cualquier , la disyunción no será 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

En la programación lógica se utiliza una definición más compleja de las fórmulas hereditarias de Harrop 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 (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 es; ${\displaystyle A}$
• ${\displaystyle G\rightarrow A}$es hereditario Harrop siempre que sea rígidamente atómico, y es una G -fórmula. ${\displaystyle A}$ ${\displaystyle G}$

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

• Las fórmulas atómicas son G -fórmulas, incluyendo la verdad (⊤);
• ${\displaystyle A\wedge B}$es una fórmula G proporcionada y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle A\vee B}$es una fórmula G proporcionada y son; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \forall x.A}$es una fórmula G proporcionada es; ${\displaystyle A}$
• ${\displaystyle \exists x.A}$es una fórmula G proporcionada es; ${\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 las matemáticas constructivas y la programación lógica .

Véase 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. Schwichtenberg (27 de julio de 2000). Teoría básica de la prueba . Cambridge University Press . ISBN 0-521-77911-1.
3. Ronald Harrop (1956). "Sobre disyunciones y enunciados existenciales en sistemas intuicionistas de lógica". Mathematische Annalen . 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ág. 575, ISBN 0-19-853792-1