論理式 (数学)

数学、数理論理学、命題論理、述語論理などにおいて、論理式（ろんりしき、英語: logical expression）とは、真理値を必要とする場所にあらわれる式のことであり、原子論理式や、それを論理演算子で結びあわせた式のことである^[1]。

ここでは古典論理のものを例示するが、非古典論理をはじめ、他の多くの論理体系についても同様な議論は可能である。

命題論理

命題論理の論理式は命題論理式（英語版）とも呼ばれ^[2]、例えば『 $(A\land(B\lorC))$ 』といった形で表現される。命題論理式は、命題変数（英語版）と論理演算を表す記号と括弧で定義され、命題変数を表すアルファベットは論理演算記号や括弧を含まないものとされる。論理式はそれらを並べたものである。

論理式は次のように再帰的に定義される。

命題変数は、単独でも論理式である。
『 $φ$ 』が論理式であるとき『 $\neg φ$ 』も論理式である。
『 $φ$ 』と『 $ψ$ 』が論理式であるとき、二項結合子を『 $•$ 』で表すとすると『 $(φ • ψ)$ 』も論理式である。一般には、『 $\lor$ 』『 $\land$ 』『 $\to$ 』『 $\leftrightarrow$ 』といった記号が二項結合子として使われる。

この定義をバッカス・ナウア記法で形式文法として記述することもできる。変数の種類は有限とすると、次のようになる。

⟨alpha set⟩ ::= p|q|r|s|t|u|\dots

（命題変数の有限集合）

⟨form⟩ ::= ⟨alpha set⟩ | \neg ⟨form⟩ | (⟨form⟩ \land ⟨form⟩) | (⟨form⟩ \lor ⟨form⟩) | (⟨form⟩ \to ⟨form⟩) | (⟨form⟩ \leftrightarrow ⟨form⟩)

この文法を使って次のような記号列が記述できる。

(((p\toq)\land(r\tos))\lor(\negq\land\negs))

これは、文法的に正しいので論理式である。一方、

((p\toq)\to(qq))p))

こちらは文法に従っていないので論理式ではない。

複雑な論理式、特に括弧を多用した論理式は理解するのが難しい。この問題を緩和するため、数学における演算子の優先順位のように結合子間の優先順位を設けることもできる。例えば、優先される順に『 $\neg$ 』『 $\to$ 』『 $\land$ 』『 $\lor$ 』とする。すると

(((p\toq)\land(r\tos))\lor(\negq\land\negs))

という論理式は次のようにも表現できる。

p\toq\landr\tos\lor\negq\land\negs

ただし、これは論理式の記述を簡略化するための単なる取り決めである。したがって例えば、左結合性で優先順を『 $\neg$ 』『 $\land$ 』『 $\lor$ 』『 $\to$ 』と取り決めれば、上の括弧のない論理式は次のように解釈される。

(p\to(q\landr))\to(s\lor((\negq)\land(\negs)))

述語論理

一階述語論理 ${\mathcal {QS}}$ における論理式の定義は、その理論のシグネチャ（英語版）に左右される。シグネチャとは、当該理論の非論理記号である定数記号、述語記号、関数記号を指定するもので、同時に関数記号や述語記号のアリティ（引数の数）の定義もシグネチャに含まれる。

シグネチャ ${\textstyle \Sigma }$ を指定したうえで、項を以下によって再帰的に定義する。項とは、議論領域の対象物を表現したものである。

任意の変数は項である。
シグネチャ ${\textstyle \Sigma }$ に含まれる任意の定数記号は項である。
t₁、…、t_n が項、f がアリティ n の関数記号ならば、f(t₁,…,t_n) は項である。

次に原子論理式が定義される。

t₁ と t₂ が項ならば、t₁=t₂ は原子論理式である。
R がアリティ n の述語記号、t₁、…、t_n が項ならば、R(t₁,…,t_n) は原子論理式である。

最後に論理式は、原子論理式の集合を含む最小の集合として次のように定義される。

任意の原子論理式は論理式である。
$\ \phi$ が論理式ならば、 $\neg \phi$ は論理式である。
$\ \phi$ と $\ \psi$ が論理式ならば、 $(\phi \land \psi )$ と $(\phi \lor \psi )$ は論理式である。
$\ x$ が変数、 $\ \phi$ が論理式ならば、 $\exists x\,\phi$ は論理式である。
$\ x$ が変数、 $\ \phi$ が論理式ならば、 $\forall x\,\phi$ は論理式である（ $\forall x\,\phi$ は $\neg \exists x\,\neg \phi$ の省略形と定義することもできる）。

何らかの変数 $\ x$ があるとき、 $\exists x$ あるいは $\forall x$ が全く出現しない論理式は量化子のない論理式と呼ばれる。量化子のない論理式の前に存在量化がある論理式を存在論理式と呼ぶ。

原子論理式と開論理式

→詳細は「原子論理式」を参照

原子論理式とは、論理結合子や量化子を含まない論理式、あるいは厳密な部分論理式を持たない論理式である。原子論理式の厳密な形式は、どんな形式体系のものかで変わってくる。例えば命題論理での原子論理式は命題変数（英語版）である。一階述語論理では、項である引数を伴った述語記号が原子論理式である。

量化子を伴わず、論理結合子のみを使って原子論理式を結合した論理式を「開論理式」と呼ぶこともある^[3]。

閉論理式

閉論理式または文とは、自由変数がない論理式を指す。一階述語論理の論理式に変数が出現する場合、閉論理式とするためにはそれぞれの変数に対応して束縛作用素（量化子など）を前置する必要がある。

属性

言語 ${\mathcal {Q}}$ における論理式が「妥当」であるとは、 ${\mathcal {Q}}$ のあらゆる解釈において真であることを意味する。
言語 ${\mathcal {Q}}$ における論理式が「充足可能（英語版）」であるとは、 ${\mathcal {Q}}$ のある解釈で真であることを意味する。
A が算術における論理式で、それが「決定可能」であるとは、それが決定可能集合を表している場合、すなわち A に出現する自由変数に値を代入したとき、その真偽を判定する実効的方法がある場合である。

語誌

初期の数理論理学者の幾人かは、『formula』を「単なる記号列」、『well-formed formula』を「formula のうち、正しい構成規則に従って作られた記号列」として区別し^[4]、幾人かは単に「formula」と総称した^[5]^[6]^[7]^[8]。

いずれにせよ形式言語という考え方が定着した現代では、わざわざ断ることなどなく、整式のみが議論の対象である。すなわち、定められている構文規則に従った記号の並び（たとえば数式であれば 1 * (2 + 3) といったような）のみが議論の対象となる式であり、同様の記号を使っていても、単なるデタラメに並べたものにしか見えないようなもの（たとえば数式であれば * + ) 3 5 / といったような）は、何か変な議論を仕掛けようとしている哲学者などでもない限り、単に、議論の対象から外すだけである（オッカムの剃刀）。

とはいえある程度は意識される概念であり、well-formed formula という句は様々な著作に見られる^[9]^[10]^[11]。

脚注

^ 共立『数学小辞典』「論理式」
^ First-order logic and automated theorem proving, Melvin Fitting, Springer, 1996
^ Handbook of the history of logic, (Vol 5, Logic from Russell to Church), Tarski's logic by Keith Simmons, D. Gabbay and J. Woods Eds, p568.
^ Alonzo Church, [1996] (1944), Introduction to mathematical logic, page 49
^ Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea
^ Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
^ Barwise, Jon, ed. (1982), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
^ Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3
^ Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
^ R. L. Simpson (1999), Essentials of Symbolic Logic, page 12
^ Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall

参考文献

Allen, Layman E. (1965), “Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games”, Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council, Monographs of the Society for Research in Child Development 30 (1): 29–41
Boolos, George; Burgess, John; Jeffrey, Richard (2002), Computability and Logic (4th ed.), Cambridge University Press, ISBN 978-0-521-00758-0 (pb.)
Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
Gamut, L.T.F. (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic, University Of Chicago Press, ISBN 0-226-28085-3
Goble, Lou, ed. (2001), The Blackwell Guide to Philosophical Logic, Blackwell, ISBN 978-0-631-20692-7
Hofstadter, Douglas (1980), Gödel, Escher, Bach: An Eternal Golden Braid, Penguin Books, ISBN 978-0-14-005579-5
Kleene, Stephen Cole (2002) [1967], Mathematical logic, New York: Dover Publications, ISBN 978-0-486-42533-7, MR1950307
Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6

外部リンク

Ehrenberg, Rachel (Spring 2002). “He's Positively Logical”. Michigan Today (University of Michigan) 2007年8月19日閲覧。 ^{[リンク切れ]}
Well-Formed Formula for First Order Predicate Logic - includes a short Java quiz.
Well-Formed Formula at ProvenMath
WFF N PROOF game site^{[リンク切れ]}
『論理式』 - コトバンク

[1] 共立『数学小辞典』「論理式」

[2] First-order logic and automated theorem proving, Melvin Fitting, Springer, 1996

[3] Handbook of the history of logic, (Vol 5, Logic from Russell to Church), Tarski's logic by Keith Simmons, D. Gabbay and J. Woods Eds, p568.

[4] Alonzo Church, [1996] (1944), Introduction to mathematical logic, page 49

[5] Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea

[6] Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6

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

[8] Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3

[9] Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3

[10] R. L. Simpson (1999), Essentials of Symbolic Logic, page 12

[11] Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

表話編歴数理論理学
一般	形式言語構成規則形式体系演繹システム（英語版）形式的証明形式意味論論理式集合元クラス古典論理公理自然演繹推論規則関係定理論理的帰結公理系型理論記号（英語版）統語論（英語版）理論（英語版）
Traditional logic（英語版）	命題推論論証妥当性 Cogency 三段論法 Square of opposition（英語版）ベン図
命題論理・ブール論理	ブール関数命題論理命題論理式（英語版）論理演算真理値表多値論理
述語論理	一階量化子述語（英語版）二階 Monadic predicate calculus（英語版）
素朴集合論	集合空集合元数え上げ外延有限集合無限集合部分集合冪集合可算集合非可算集合帰納的集合定義域終域像写像関数関係順序対
集合論	数学基礎論ツェルメロ＝フレンケル集合論選択公理一般集合論（英語版） Kripke–Platek 集合論（英語版）フォン・ノイマン＝ベルナイス＝ゲーデル集合論（英語版）モース-ケリー集合論タルスキ＝グロタンディーク集合論（英語版）
モデル理論	モデル（英語版）解釈（英語版）超準モデル（英語版）有限モデル理論真理値妥当性
証明論	形式的証明演繹システム（英語版）形式体系定理論理的帰結推論規則統語論（英語版）シークエント計算
計算理論再帰理論	計算可能性計算複雑性複雑性クラス P≠NP予想再帰帰納的集合帰納的可算集合決定問題停止性問題チャーチ＝チューリングのテーゼ計算可能関数原始再帰関数 μ再帰関数チューリングマシンラムダ計算