整形式の式

数理論理学、命題論理学、述語論理学において、整形式論理式（じょうけいじりじき、英: well-formed formula、WFFまたはwffと略記、単に論理式とも呼ばれる）は、形式言語の一部である特定のアルファベットからの有限の記号列である。^[1]

略語wffは「woof」と発音されるが、時には「wiff」、「weff」、「whiff」と発音されることもある。^[12]

形式言語は、言語内の一連の式で識別できます。式は、解釈によって意味を与えることができる構文オブジェクトです。式の主な用途は、命題論理と述語論理の 2 つです。

導入

式の主な用途は、命題論理と述語論理、たとえば一階述語論理です。これらのコンテキストでは、式は記号 φ の文字列であり、記号 φ 内の任意の自由変数がインスタンス化されると、「φ は真か?」と尋ねることが意味を持ちます。形式論理では、証明は特定のプロパティを持つ式のシーケンスで表すことができ、シーケンスの最後の式が証明されます。

「公式」という用語は、書かれたマーク（たとえば、紙や黒板に書かれたマーク）を指すために使用されることもありますが、より正確には、マークが公式の象徴的なインスタンスである、表現される記号のシーケンスとして理解されます。この「プロパティ」という漠然とした概念と、帰納的に定義された整形式の公式という概念との区別は、ワイルの 1910 年の論文「数学の基礎の定義について」に由来しています。^[13]したがって、同じ公式が複数回記述される可能性があり、原理的には、公式が長すぎて物理宇宙内でまったく記述できない場合もあります。

式自体は構文オブジェクトです。解釈によって意味が与えられます。たとえば、命題式では、各命題変数は具体的な命題として解釈され、式全体がこれらの命題間の関係を表します。ただし、式を単に式として考えるために解釈する必要はありません。

命題計算

命題計算の公式は命題式とも呼ばれ、^[14]のような表現である。その定義は命題変数の集合Vを任意に選択することから始まる。アルファベットはVの文字と命題接続詞および括弧「(」と「)」の記号から成り、これらはすべてVに含まれないものと想定される。公式はこのアルファベット上の特定の表現（つまり記号の列）となる。 $(A\land (B\lor C))$

式は次のように帰納的に定義されます。

それぞれの命題変数は、それ自体が式です。
φ が式であれば、¬φ も式です。
φ と ψ が式であり、 • が任意の二項接続詞である場合、 ( φ • ψ) は式です。ここで、 • は通常の演算子 ∨、∧、→、または ↔ ですが、これらに限定されません。

この定義は、変数の集合が有限であれば、バッカス・ナウア形式の形式文法として記述することもできます。

<アルファ セット>  ::= p | q | r | s | t | u | ... (命題変数の任意の有限集合)
 <フォーム>  ::=  <アルファ セット> | ¬ <フォーム> | ( <フォーム> ∧ <フォーム> ) | ( <フォーム> ∨ <フォーム> ) | ( <フォーム> → <フォーム> ) | ( <フォーム> ↔ <フォーム> )

この文法を用いると、記号の並びは

((( p → q ) ∧ ( r → s )) ∨ (¬ q ∧ ¬ s ))

は文法的に正しいので、公式です。記号の並びは

(( p → q )→( qq )) p ))

文法に準拠していないため、公式ではありません。

複雑な式は、例えば括弧が多すぎるために読みにくい場合があります。この最後の現象を軽減するために、演算子間に優先順位ルール（標準的な数学の演算順序に類似）が想定され、一部の演算子が他の演算子よりも拘束力を持つようになります。たとえば、優先順位（最も拘束力の強いものから最も拘束力の弱いものまで）を 1. ¬ 2. → 3. ∧ 4. ∨ と仮定すると、式は次のようになります。

((( p → q ) ∧ ( r → s )) ∨ (¬ q ∧ ¬ s ))

と略されることもある

p → q ∧ r → s ∨ ¬ q ∧ ¬ s

しかし、これは式の表記を簡略化するための慣例に過ぎません。優先順位が、例えば、1. ¬ 2. ∧ 3. ∨ 4. → の順で左から右への結合であると仮定すると、上の式（括弧なし）は次のように書き直されます。

( p → ( q ∧ r )) → ( s ∨ (¬ q ∧ ¬ s ))

述語論理

一階述語論理における式の定義は、手元の理論のシグネチャに相対的です。このシグネチャは、手元の理論の定数記号、述語記号、関数記号、および関数記号と述語記号のアリティを指定します。 ${\mathcal {QS}}$

公式の定義はいくつかの部分に分かれています。まず、用語のセットが再帰的に定義されます。非公式には、用語は談話ドメインのオブジェクトを表す表現です。

あらゆる変数は項です。
シグネチャの定数記号は項である
f ( t ₁ ,..., t _n )という形式の式（fはn項関数記号、t ₁ ,..., t _nは項）もまた項です。

次のステップは原子式を定義することです。

t ₁とt _{2 が}項である場合、 t ₁ = t ₂は原子式である。
Rがn項述語記号で、t ₁ ,..., t _nが項である場合、R ( t ₁ ,..., t _n )は原子式である。

最後に、式の集合は、次の式が成り立つような原子式の集合を含む最小の集合として定義されます。

$\neg \phi$ は式であるとき $\phi$
$(\phi \land \psi )$ およびは、およびが式である場合に式です。 $(\phi \lor \psi )$ $\phi$ $\psi$
$\exists x\,\phi$ は変数であり、は式であるとき、は式です。 $x$ $\phi$
$\forall x\,\phi$ は、が変数であり、が式である場合に式になります (または、の省略形として定義することもできます)。 $x$ $\phi$ $\forall x\,\phi$ $\neg \exists x\,\neg \phi$

式にまたはが含まれず、どの変数もでない場合は、その式はと呼ばれます。 $\exists x$ $\forall x$ $x$ 量指定子なし。存在式は、存在量化のシーケンスで始まり、量指定子なしの式が続く式です。

原子式とオープン式

原子式は、論理接続子も量指定子も含まない式、または厳密に部分式を持たない式です。原子式の正確な形式は、検討中の形式体系によって異なります。たとえば、命題論理の場合、原子式は命題変数です。述語論理の場合、アトムは述語記号とその引数であり、各引数は項です。

いくつかの用語によれば、開いた式は、量指定子を除外して論理接続詞のみを使用して原子式を組み合わせることによって形成されます。^[15]これを閉じていない式と混同しないでください。

閉じた式

閉じた式 (基底式または文ともいう)は、変数が自由に出現しない式である。Aが、変数 $v$ $1$ $、\dots、$ $v$ $n が$ 自由に出現する第一階言語の式である場合、 $\forall$ $v$ $1$ $\dots \forall$ $v$ $n$ が先行するA は、 Aの普遍閉包である。

数式に適用可能なプロパティ

言語の式A は、のすべての解釈に対して真である場合に有効です。 ${\mathcal {Q}}$ ${\mathcal {Q}}$
言語の式A は、の何らかの解釈に対して真である場合に満足可能である。 ${\mathcal {Q}}$ ${\mathcal {Q}}$
算術言語の式A は、それが決定可能な集合を表す場合、つまり、Aの自由変数の置換を与えられたときに、結果として得られるAのインスタンスまたはその否定が証明可能であることを示す有効な方法がある場合、決定可能です。

用語の使用

数理論理学に関する初期の研究（例えばチャーチ^[16]）では、式は任意の記号列を指し、これらの列の中で、整形式の式は（正しい）式の形成規則に従った列でした。

著者の中には単に「式」と言う者もいる。^[17]^[18]^[19]^{[20]現代の用法（特に、}モデルチェッカー、自動定理証明器、対話型定理証明器などの数学ソフトウェアを使用するコンピュータサイエンスの文脈）では、式の概念を代数的概念のみに保持し、式の整形式性、つまり式の具体的な文字列表現（接続詞や量指定子にこの記号またはその記号を使用する、この括弧規則またはその括弧を使用する、ポーランド記法または挿入記法を使用するなど）の問題を単なる表記法の問題として残す傾向がある。

「整形式の公式」（WFF）という表現も大衆文化に浸透した。WFFは、レイマン・アレン^[21]がイェール大学ロースクール在学中に開発した学術ゲーム「WFF 'N PROOF : 現代論理のゲーム」（後にミシガン大学教授）の名前に使われている難解な語呂合わせの一部である。このゲーム群は、子供たちに記号論理学の原理を教えるために考案された（ポーランド語表記）。^{[22]その名前は、}イェール大学で応援に使われ、ウィッフェンプーフの歌やウィッフェンプーフスで有名になったナンセンスな言葉、ウィッフェンプーフを模倣したものである。^[23]

参照

注記

^ 公式は入門論理学の標準的なトピックであり、Enderton (2001)、Gamut (1990)、Kleene (1967) を含むすべての入門教科書で取り上げられています。
^ ゲンスラー、ハリー (2002-09-11). 論理学入門. ラウトレッジ. p. 35. ISBN 978-1-134-58880-0。
^ Hall, Cordelia; O'Donnell, John (2013-04-17). コンピューターを使った離散数学。Springer Science & Business Media。p. 44。ISBN 978-1-4471-3657-6。
^ Agler, David W. (2013). 記号論理学: 構文、意味論、証明。Rowman & Littlefield。p. 41。ISBN 978-1-4422-1742-3。
^シンプソン、RL (2008-03-17)。記号論理学の基礎 - 第3版。ブロードビュー・ プレス。p. 14。ISBN 978-1-77048-495-5。
^ ラデルート、カール（2022-10-24）。形式論理のポケットガイド。ブロードビュープレス。p.59。ISBN 978-1-77048-868-7。
^ マウラー、スティーブン B.; ラルストン、アンソニー (2005-01-21)。離散アルゴリズム数学、第 3 版。CRC プレス。p. 625。ISBN 978-1-56881-166-6。
^ マーティン、ロバート M. (2002-05-06). 哲学者の辞典 - 第 3 版. ブロードビュープレス. p. 323. ISBN 978-1-77048-215-9。
^ Date, Christopher (2008-10-14). リレーショナルデータベース辞書、拡張版。Apress。p. 211。ISBN 978-1-4302-1042-9。
^ Date, CJ (2015-12-21)。新しいリレーショナルデータベース辞書: 用語、概念、および例。「O'Reilly Media, Inc.」。p. 241。ISBN 978-1-4919-5171-2。
^シンプソン、RL (1998-12-10)。記号論理学の基礎。ブロードビュー・ プレス。p. 12。ISBN 978-1-55111-250-3。
^
- 「ワンワン」^[2]^[3]^[4]^[5]
- 「ウィフ」^[6]^[7]^[8]
- 「ウェフ」^[9]^[10]
- 「匂い」^[11]
すべてのソースが「woof」を支持しました。「wiff」、「weff」、および「whiff」について引用されたソースは、これらの発音を「woof」の代替として示しました。Gensler の情報源は、「woof」の母音の発音例として「wood」と「woofer」を示しています。
^ W. ディーン、S. ウォルシュ、「第 2 階算術のサブシステムの前史」(2016)、p.6
^ 一階述語論理と自動定理証明、メルビン・フィッティング、シュプリンガー、1996年 [1]
^ 論理学の歴史ハンドブック（第5巻、ラッセルからチャーチまでの論理学）、タルスキーの論理学、キース・シモンズ、D.ギャベイ、J.ウッズ編、p568 [2]。
^ アロンゾ・チャーチ、[1996] (1944)、数理論理学入門、49ページ
^ ヒルベルト、デイヴィッド、アッカーマン、ヴィルヘルム（1950）[1937]、数学論理の原理、ニューヨーク：チェルシー
^ ホッジス、ウィルフリッド（1997）、短縮モデル理論、ケンブリッジ大学出版局、ISBN 978-0-521-58713-6
^ バーワイズ、ジョン、編（1982）、数理論理学ハンドブック、論理学と数学の基礎研究、アムステルダム：北ホラント、ISBN 978-0-444-86388-1
^ コリ、ルネ、ラスカー、ダニエル（2000）、数学論理学：演習付きコース、オックスフォード大学出版局、ISBN 978-0-19-850048-3
^ エーレンバーグ 2002
^ より技術的には、フィッチスタイルの計算を使用した命題論理。
^ アレン（1965）は、この語呂合わせを認めている。

参考文献

アレン、レイマン E. (1965)、「WFF 'N PROOF ゲームによる数学的論理の自律的学習に向けて」、数学的学習: 社会科学研究評議会の知的プロセス研究委員会主催の会議報告、児童発達研究協会のモノグラフ、30 (1): 29–41
ブーロス、ジョージ、バージェス、ジョン、ジェフリー、リチャード（2002）、計算可能性と論理（第4版）、ケンブリッジ大学出版局、ISBN 978-0-521-00758-0
エーレンバーグ、レイチェル (2002 年春)。「彼は積極的に論理的だ」。ミシガントゥデイ。ミシガン大学。2009 年 2 月 8 日にオリジナルからアーカイブ。2007年 8 月 19 日に取得。
エンダートン、ハーバート（2001）、論理学への数学的入門（第2版）、ボストン、マサチューセッツ州：アカデミックプレス、ISBN 978-0-12-238452-3
Gamut, LTF (1990)、論理、言語、意味、第1巻：論理入門、シカゴ大学出版局、ISBN 0-226-28085-3
ホッジス、ウィルフリッド (2001)、「古典論理学 I: 一階述語論理」、ゴブル、ルー (編)、ブラックウェル哲学論理ガイド、ブラックウェル、ISBN 978-0-631-20692-7
ホフスタッター、ダグラス（1980年）、ゲーデル、エッシャー、バッハ：永遠の黄金の編み紐、ペンギンブックス、ISBN 978-0-14-005579-5
クリーネ、スティーブン・コール（2002）[1967]、数学論理学、ニューヨーク：ドーバー出版、ISBN 978-0-486-42533-7、MR 1950307
ラウテンバーグ、ヴォルフガング（2010）、数理論理学の簡潔な入門（第3版）、ニューヨーク：シュプリンガーサイエンス+ビジネスメディア、doi：10.1007 / 978-1-4419-1221-3、ISBN 978-1-4419-1220-6

外部リンク

第一階述語論理の適切な形式式 - 短いJavaクイズが含まれています。
ProvenMath の正しい公式

[1] 公式は入門論理学の標準的なトピックであり、Enderton (2001)、Gamut (1990)、Kleene (1967) を含むすべての入門教科書で取り上げられています。

[2] ゲンスラー、ハリー (2002-09-11). 論理学入門. ラウトレッジ. p. 35. ISBN 978-1-134-58880-0。

[3] Hall, Cordelia; O'Donnell, John (2013-04-17). コンピューターを使った離散数学。Springer Science & Business Media。p. 44。ISBN 978-1-4471-3657-6。

[4] Agler, David W. (2013). 記号論理学: 構文、意味論、証明。Rowman & Littlefield。p. 41。ISBN 978-1-4422-1742-3。

[5] ^シンプソン、RL (2008-03-17)。記号論理学の基礎 - 第3版。ブロードビュー・ プレス。p. 14。ISBN 978-1-77048-495-5。

[6] ラデルート、カール（2022-10-24）。形式論理のポケットガイド。ブロードビュープレス。p.59。ISBN 978-1-77048-868-7。

[7] マウラー、スティーブン B.; ラルストン、アンソニー (2005-01-21)。離散アルゴリズム数学、第 3 版。CRC プレス。p. 625。ISBN 978-1-56881-166-6。

[8] マーティン、ロバート M. (2002-05-06). 哲学者の辞典 - 第 3 版. ブロードビュープレス. p. 323. ISBN 978-1-77048-215-9。

[9] Date, Christopher (2008-10-14). リレーショナルデータベース辞書、拡張版。Apress。p. 211。ISBN 978-1-4302-1042-9。

[10] Date, CJ (2015-12-21)。新しいリレーショナルデータベース辞書: 用語、概念、および例。「O'Reilly Media, Inc.」。p. 241。ISBN 978-1-4919-5171-2。

[11] ^シンプソン、RL (1998-12-10)。記号論理学の基礎。ブロードビュー・ プレス。p. 12。ISBN 978-1-55111-250-3。

[12] 
「ワンワン」^[2]^[3]^[4]^[5]

「ウィフ」^[6]^[7]^[8]

「ウェフ」^[9]^[10]

「匂い」^[11]
すべてのソースが「woof」を支持しました。「wiff」、「weff」、および「whiff」について引用されたソースは、これらの発音を「woof」の代替として示しました。Gensler の情報源は、「woof」の母音の発音例として「wood」と「woofer」を示しています。

[13] 「ワンワン」^[2]^[3]^[4]^[5]

[14] 「ウィフ」^[6]^[7]^[8]

[15] 「ウェフ」^[9]^[10]

[16] 「匂い」^[11]

[13] W. ディーン、S. ウォルシュ、「第 2 階算術のサブシステムの前史」(2016)、p.6

[14] 一階述語論理と自動定理証明、メルビン・フィッティング、シュプリンガー、1996年 [1]

[15] 論理学の歴史ハンドブック（第5巻、ラッセルからチャーチまでの論理学）、タルスキーの論理学、キース・シモンズ、D.ギャベイ、J.ウッズ編、p568 [2]。

[16] アロンゾ・チャーチ、[1996] (1944)、数理論理学入門、49ページ

[17] ヒルベルト、デイヴィッド、アッカーマン、ヴィルヘルム（1950）[1937]、数学論理の原理、ニューヨーク：チェルシー

[18] ホッジス、ウィルフリッド（1997）、短縮モデル理論、ケンブリッジ大学出版局、ISBN 978-0-521-58713-6

[19] バーワイズ、ジョン、編（1982）、数理論理学ハンドブック、論理学と数学の基礎研究、アムステルダム：北ホラント、ISBN 978-0-444-86388-1

[20] コリ、ルネ、ラスカー、ダニエル（2000）、数学論理学：演習付きコース、オックスフォード大学出版局、ISBN 978-0-19-850048-3

[21] エーレンバーグ 2002

[22] より技術的には、フィッチスタイルの計算を使用した命題論理。

[23] アレン（1965）は、この語呂合わせを認めている。