ハロップ式

直観主義論理において、ハロップ公式はロナルド・ハロップにちなんで名付けられ、次のように帰納的に定義される公式 のクラスである。 ^{[1] [2] [3]}

• 原子式はハロップ式であり、偽（⊥）を含みます。
• ${\displaystyle A\wedge B}$Harrop が提供されています。 ${\displaystyle A}$ ${\displaystyle B}$
• ${\displaystyle \neg F}$任意の整形式の式に対するハロップです。 ${\displaystyle F}$
• ${\displaystyle F\rightarrow A}$は、Harrop が規定するものであり、任意の適切な式です。 ${\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の基礎となっている。遺伝的ハロップ公式は、2つ（場合によっては3つ）の再帰的な公式集合によって定義される。ある定式では、次のように表される。^[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版）.オックスフォード大学出版局. p. 227. ISBN 0-19-850524-8。
2. AS Troelstra ; H. Schwichtenberg (2000年7月27日). 『基礎証明理論』ケンブリッジ大学出版局. ISBN 0-521-77911-1。
3. ロナルド・ハロップ (1956). 「直観主義的論理体系における選言と存在論的言明について」. Mathematische Annalen . 132 (4): 347– 361. doi :10.1007/BF01360048. S2CID  120620003.
4. Dov M. Gabbay、Christopher John Hogger、John Alan Robinson、「人工知能と論理プログラミングにおけるロジックのハンドブック：ロジックプログラミング」、オックスフォード大学出版局、1998年、p 575、ISBN 0-19-853792-1

Retrieved from "https://en.wikipedia.org/w/index.php?title=Harrop_formula&oldid=1322626147"