формула Харропа

В интуиционистской логике формулы Харропа , названные в честь Рональда Харропа, представляют собой класс формул , индуктивно определяемых следующим образом: ^{[1] [2] [3]}

• Атомарные формулы — Харропа, включая ложность (⊥);
• ${\displaystyle A\wedge B}$предоставлено ли Харропом и есть ли; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \neg F}$является Харропом для любой правильно построенной формулы ; ${\displaystyle F}$
• ${\displaystyle F\rightarrow A}$предоставлено Харропом , и является любой правильно построенной формулой; ${\displaystyle A}$ ${\displaystyle F}$
• ${\displaystyle \forall x.A}$предоставлено Харропом . ${\displaystyle A}$

Исключая дизъюнкцию и экзистенциальную квантификацию (за исключением антецедента импликации ), можно избежать неконструктивных предикатов, что имеет преимущества для компьютерной реализации.

Обсуждение

Формулы Харропа "хорошо себя ведут" также в конструктивном контексте. Например, в арифметике Гейтинга формулы Харропа удовлетворяют классической эквивалентности, которая обычно не удовлетворяется в конструктивной логике: ^[1] ${\displaystyle {\mathsf {HA}}}$

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

Однако существуют -утверждения, которые являются -независимыми, то есть это простые утверждения, для которых исключенное третье не является -доказуемым. Действительно, в то время как интуиционистская логика доказывает для любого , дизъюнкция не будет Харропом. ${\displaystyle \Pi _{1}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \forall x.A}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle \neg \neg (P\lor \neg P)}$ ${\displaystyle P}$

Наследственные формулы Харропа и логическое программирование

Более сложное определение наследственных формул Харропа используется в логическом программировании как обобщение предложений Хорна и составляет основу языка λProlog . Наследственные формулы Харропа определяются в терминах двух (иногда трех) рекурсивных наборов формул. В одной формулировке: ^[4]

• Жесткие атомарные формулы, т. е. константы или формулы , являются наследственными Харропами; ${\displaystyle r}$ ${\displaystyle r(t_{1},...,t_{n})}$
• ${\displaystyle A\wedge B}$является наследственным Харропом и обеспечены ; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \forall x.A}$наследственный Харроп при условии, что есть; ${\displaystyle A}$
• ${\displaystyle G\rightarrow A}$является наследственным Харропом при условии , что он жестко атомичен и является G -формулой. ${\displaystyle A}$ ${\displaystyle G}$

G -формулы определяются следующим образом: ^[4]

• Атомарные формулы — это G -формулы, включающие истину (⊤);
• ${\displaystyle A\wedge B}$является G -формулой и являются; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle A\vee B}$является G -формулой и являются; ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \forall x.A}$является G -формулой при условии, что есть; ${\displaystyle A}$
• ${\displaystyle \exists x.A}$является G -формулой при условии, что есть; ${\displaystyle A}$
• ${\displaystyle H\rightarrow A}$является G -формулой при условии , что является, и является наследственным Харропом. ${\displaystyle A}$ ${\displaystyle H}$

История

Формулы Харропа были введены около 1956 года Рональдом Харропом и независимо от него Хеленой Расиовой . ^[2] Вариации фундаментальной концепции используются в различных разделах конструктивной математики и логического программирования .

Смотрите также

• Реализуемость

Ссылки

1. Дамметт, Майкл (2000). Элементы интуиционизма (2-е изд.). Oxford University Press . стр. 227. ISBN 0-19-850524-8.
2. AS Troelstra ; H. Schwichtenberg (27 июля 2000 г.). Базовая теория доказательств . Cambridge University Press . ISBN 0-521-77911-1.
3. Рональд Харроп (1956). «О дизъюнкциях и экзистенциальных утверждениях в интуиционистских системах логики». Mathematische Annalen . 132 (4): 347–361. doi :10.1007/BF01360048. S2CID  120620003.
4. Дов М. Габбей , Кристофер Джон Хоггер, Джон Алан Робинсон , Справочник по логике в искусственном интеллекте и логическом программировании: Логическое программирование , Oxford University Press , 1998, стр. 575, ISBN 0-19-853792-1