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

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

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

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

Обсуждение

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

$\neg \neg A\leftrightarrow A.$

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

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

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

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

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

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

История

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

См. также

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