オープンフォーミュラ

オープン式とは、少なくとも 1 つの自由変数を含む式です。^[^要出典^]

開いた式には真理値が割り当てられません。一方、閉じた式は命題を構成し、真偽のような真理値を持つことができます。開いた式は、各自由変数に量指定子を適用することで閉じた式に変換できます。この変換は、自由変数を束縛変数にするための捕捉と呼ばれます。

例えば、自然数について推論する場合、「 x +2 > y 」という式は自由変数xとyを含んでいるため、開式となります。一方、「∃ y ∂ x : x +2 > y」という式は閉式であり、真理値はtrue となります。

オープンフォーミュラは、次のような厳密な数学的性質の定義でよく使用されます。

「ある人物zにとって、 z がyの親であり、xがzの姉妹である場合、xはyの叔母である」

（自由変数x、y、束縛変数z）は、「親」と「姉妹」の観点から「叔母」という概念を定義しています。素数であるという性質を定義する、より正式な別の例は、

「P ( x ) は, ∈ : m >1 ∧ n > 1 → x ≠ m ⋅ nの場合」

\mathbb {N}

（自由変数xと束縛変数m、n）。

真理値が偽である閉式の例としては、フェルマー数の列が挙げられる。

F_{n}=2^{2^{n}}+1,

フェルマーが素数性に関連して研究した。フェルマー数列の各数に述語文字P（素数）を付与することで、一連の閉じた式が得られる。これらの式はn = 0,...,4の場合には真であるが、2023年現在、真の式を与えるより大きなn^[update]の値は知られていない。例えば、は素数ではない。したがって、閉じた式 ∀ n P ( F _n ) は偽である。 $F_{5}=4\,294\,967\,297=641\cdot 6\,700\,417$

データベース理論では、クエリをオープンな一階述語論理式として表現する場合、自由変数は SQLクエリの SELECT句に出現する変数を表します。例えば、次のような式を考えます。

\varphi (son)=birthYear(son,2020)\land \exists mom{\textbf {.}}(motherOf(mom,son)\land birthYear(mom,1999))

は唯一の自由変数であり、SQL では次のように表現できます。 $son$

SELECT y1 . person AS son FROM birth_year y1 WHERE y1 . year = 2020 AND EXISTS ( SELECT * FROM mother_of m1 JOIN birth_year y2 ON m1 . mother = y2 . person WHERE m1 . son = y1 . person AND y2 . year = 1999 )

2020 年に生まれ、母親が 1999 年生まれの人をすべて選択します。

正式には、データベースに対して上記の SQL クエリを実行することは、のエルブラン解釈がを満たすような定数を持つの自由変数のすべての置換を探すことと同等です。ここで、はデータベースを表す基底原子の集合です。 $\sigma$ $\varphi$ ${\mathcal {D}}$ $\sigma (\varphi )$ ${\mathcal {D}}$

参照

参考文献

Wolfgang Rautenberg (2008)、Einführung in die Mathematische Logik (ドイツ語) (3 版)、ヴィースバーデン: Vieweg+Teubner、ISBN 978-3-8348-0578-2
H.-P. Tuschik、H. Wolter (2002)、Mathematische Logik – kurzgefaßt (ドイツ語)、Heidelberg: Spektrum、Akad。フェルラーグ、ISBN 3-8274-1387-7