整った公式

数理論理学、命題論理学、述語論理学において、整形式式（WFFまたはwffと略され、しばしば単に式と呼ばれる）は、形式言語の定義された文法に従って構築された、与えられたアルファベットからの有限個の記号列である。^[¹^]

略語wffは「ウーフ」または「ウィフ」、「ウェフ」、「ウィフ」と発音される。^{[ 12 ]}

形式言語は、その言語に含まれる式の集合と同一視できる。式とは、解釈によって意味を与えることができる構文上の対象である。式は、命題論理と述語論理において重要な役割を果たす。

導入

論理式の重要な用途の一つは、命題論理や述語論理（例えば一階述語論理）においてである。これらの文脈では、論理式は記号列φであり、φに含まれる自由変数がインスタンス化された後、「 φは真か？」と問うことが意味を持つ。形式論理では、証明は特定の性質を持つ論理式の列で表現でき、その列の最後の論理式が証明される。

「式」という用語は、書かれた記号（例えば、紙や黒板に書かれた記号）にも使われることがあるが、より正確には、表現されている記号のシーケンスとして理解され、記号は式の具体例である。この「性質」という曖昧な概念と、帰納的に定義された整形式の概念との区別は、ワイルの1910年の論文「数学的基本概念の定義について」に端を発している。^{[ 13 ]}したがって、同じ式が複数回書かれることもあり、原理的には、物理的な宇宙の中では全く書けないほど長い式も存在する可能性がある。

式そのものは構文上の対象である。式は解釈によって意味を与えられる。例えば、命題式においては、各命題変数は具体的な命題として解釈され、式全体としてはこれらの命題間の関係を表す。しかし、式は解釈されることなく、単に式として扱われる場合もある。

命題論理

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

これらの公式は、帰納的に以下のように定義される。

それぞれの命題変数は、それ自体が一つの式である。
φが論理式であるならば、¬φも論理式である。
φ と ψ が論理式であり、• が任意の二項結合子である場合、( φ • ψ) は論理式です。ここで、• は通常の演算子 ∨、∧、→、または ↔ である可能性があります (ただし、これらに限定されません)。

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

< alpha set > ::= p | q | r | s | t | u | ... (任意の有限命題変数の集合) < form > ::= < alpha set > | ¬ < form > | ( < form > ∧ < form > ) | ( < form > ∨ < form > ) | ( < form > → < form > ) | ( < form > ↔ < form > )

この文法を用いると、記号のシーケンスは

((( 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$ が自由出現する一階述語論理の式である場合、 ∀ $v$ $1$ $\dots$ $\forall$ $v$ $n$ を前に付けたA は $、$ Aの普遍閉包です。

数式に適用可能な特性

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

用語の使用

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

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

「整形式数式」（WFF）という表現も大衆文化に浸透した。WFFは、レイマン・アレン^[21^]がイェール大学ロースクール在学中に開発した学術ゲーム「 WFF 'N PROOF : The Game of Modern Logic」[ ²² ]の名称に使われている難解な言葉遊びの一部である（彼は後にミシガン大学の教授となった）。このゲーム群は、子供たちに記号論理の原理を教える（ポーランド記法）ように設計されている^[²³^] 。その名称は、イェール大学で応援歌として使われ、 「The Whiffenpoof Song」や「The Whiffenpoofs」で有名になったナンセンスな言葉「whiffenpoof」をもじったものである^[²⁴^]。

注記

↑論理式は入門論理学における標準的なトピックであり、Enderton (2001)、Gamut (1990)、Kleene (1967) を含むすべての入門教科書で扱われています。
↑ゲンスラー、ハリー（2002年9月11日）。『論理学入門』。ラウトレッジ。35 ページ。ISBN 978-1-134-58880-0。
↑ホール、コーデリア；オドネル、ジョン（2013年4月17日）。コンピュータを用いた離散数学。Springer Science & Business Media。p. 44。ISBN 978-1-4471-3657-6。
↑ Agler, David W. (2013). Symbolic Logic: Syntax, Semantics, and Proof . Rowman & Littlefield. p. 41. ISBN 978-1-4422-1742-3。
↑ Simpson, RL (2008-03-17). Essentials of Symbolic Logic - Third Edition . Broadview Press. p. 14. ISBN 978-1-77048-495-5。
↑ラデルート、カール（2022年10月24日）。形式論理学ポケットガイド。ブロードビュー・プレス。59ページ。ISBN 978-1-77048-868-7。
↑マウラー、スティーブン・B.、ラルストン、アンソニー（2005年1月21日）。離散アルゴリズム数学、第3版。CRC Press。p. 625。ISBN 978-1-56881-166-6。
↑マーティン、ロバート・M. (2002年5月6日). 『哲学者の辞典 ― 第三版』ブロードビュー・プレス. 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). The New Relational Database Dictionary: Terms, Concepts, and Examples . O'Reilly Media, Inc. p. 241. ISBN 978-1-4919-5171-2。
↑ Simpson, RL (1998-12-10). Essentials of Symbolic Logic . Broadview Press. p. 12. ISBN 978-1-55111-250-3。
↑
- 「ワン」^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}^{[ 5 ]}
- 「ウィフ」^{[ 6 ]}^{[ 7 ]}^{[ 8 ]}
- 「weff」^{[ 9 ]}^{[ 10 ]}
- 「かすかな」^{[ 11 ]}
すべての情報源が「woof」を支持していました。「wiff」「weff」「whiff」の発音について引用された情報源は、これらの発音を「woof」の代替として挙げていました。Genslerの情報源は、「woof」の母音の発音例として「wood」と「woofer」を挙げています。
↑ W. Dean、S. Walsh、『二階算術のサブシステムの先史時代』（2016年）、6ページ
↑一階述語論理と自動定理証明、メルビン・フィッティング著、シュプリンガー、1996年
↑論理学史ハンドブック（第5巻、ラッセルからチャーチまでの論理学）、タルスキの論理学、キース・シモンズ著、D・ギャベイおよびJ・ウッズ編、568ページ。
↑アロンゾ・チャーチ、[1996]（1944）、『数理論理学入門』、49ページ
↑ヒルベルト、デイヴィッド；アッカーマン、ヴィルヘルム(1950) [1937]、『数理論理学の原理』、ニューヨーク：チェルシー
↑ホッジス、ウィルフリッド (1997)、より短いモデル理論、ケンブリッジ大学出版局、 ISBN 978-0-521-58713-6
↑ Barwise, Jon編 (1982), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
↑コリ、レネ；ラスカー、ダニエル（2000）、『数理論理学：演習付きコース』、オックスフォード大学出版局、 ISBN 978-0-19-850048-3
↑エーレンブルク 2002
↑より技術的には、フィッチ式計算を用いた命題論理。
↑アレン（1965）は駄洒落を認めている。

参考文献

Allen, Layman 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-7MR 1950307
Rautenberg, Wolfgang (2010), 『数学論理学入門』（第3 版）、ニューヨーク：Springer Science+Business Media、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年9月11日）。『論理学入門』。ラウトレッジ。35 ページ。ISBN 978-1-134-58880-0。

[3] ホール、コーデリア；オドネル、ジョン（2013年4月17日）。コンピュータを用いた離散数学。Springer Science & Business Media。p. 44。ISBN 978-1-4471-3657-6。

[4] Agler, David W. (2013). Symbolic Logic: Syntax, Semantics, and Proof . Rowman & Littlefield. p. 41. ISBN 978-1-4422-1742-3。

[5] Simpson, RL (2008-03-17). Essentials of Symbolic Logic - Third Edition . Broadview Press. p. 14. ISBN 978-1-77048-495-5。

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

[7] マウラー、スティーブン・B.、ラルストン、アンソニー（2005年1月21日）。離散アルゴリズム数学、第3版。CRC Press。p. 625。ISBN 978-1-56881-166-6。

[8] マーティン、ロバート・M. (2002年5月6日). 『哲学者の辞典 ― 第三版』ブロードビュー・プレス. 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). The New Relational Database Dictionary: Terms, Concepts, and Examples . O'Reilly Media, Inc. p. 241. ISBN 978-1-4919-5171-2。

[11] Simpson, RL (1998-12-10). Essentials of Symbolic Logic . Broadview Press. p. 12. ISBN 978-1-55111-250-3。

[12] 
「ワン」^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}^{[ 5 ]}
「ウィフ」^{[ 6 ]}^{[ 7 ]}^{[ 8 ]}
「weff」^{[ 9 ]}^{[ 10 ]}
「かすかな」^{[ 11 ]}
すべての情報源が「woof」を支持していました。「wiff」「weff」「whiff」の発音について引用された情報源は、これらの発音を「woof」の代替として挙げていました。Genslerの情報源は、「woof」の母音の発音例として「wood」と「woofer」を挙げています。

[mwAiE] 「ワン」^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}^{[ 5 ]}

[mwAjI] 「ウィフ」^{[ 6 ]}^{[ 7 ]}^{[ 8 ]}

[mwAj8] 「weff」^{[ 9 ]}^{[ 10 ]}

[mwAkg] 「かすかな」^{[ 11 ]}

[13] W. Dean、S. Walsh、『二階算術のサブシステムの先史時代』（2016年）、6ページ

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

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

[16] アロンゾ・チャーチ、[1996]（1944）、『数理論理学入門』、49ページ

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

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

[19] Barwise, Jon編 (1982), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1

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

[21] エーレンブルク 2002

[22] より技術的には、フィッチ式計算を用いた命題論理。

[23] アレン（1965）は駄洒落を認めている。

[

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[21

[

[

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

整った公式

導入

命題論理

述語論理

原子式と開式

閉じた式

数式に適用可能な特性

用語の使用

関連項目

注記

参考文献

外部リンク

関連するトピック

数理論理学

命題論理学

述語論理学

形式言語