論理式 (数学)のソースを表示

[[数学]]、[[数理論理学]]、[[命題論理]]、[[述語論理]]などにおいて、'''論理式'''（ろんりしき、{{Lang-en|logical expression}}）とは、[[真理値]]を必要とする場所にあらわれる[[式]]のことであり、[[原子論理式]]や、それを[[論理演算子]]で結びあわせた式のことである<ref>共立『数学小辞典』「論理式」</ref>。

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

== 命題論理 ==
[[命題論理]]の論理式は{{仮リンク|命題論理式|en|propositional formula}}とも呼ばれ<ref>[https://books.google.co.jp/books?id=T8OMqvXvWWQC&lpg=PA11&dq=%22propositional+formula%22&hl=fr&pg=PA11&redir_esc=y#v=onepage&q=%22propositional%20formula%22&f=false First-order logic and automated theorem proving], Melvin Fitting, Springer, 1996</ref>、例えば『{{math|{{Font|(A&and;(B&or;C))|font=monospace}}}}』といった形で表現される。命題論理式は、{{仮リンク|命題変数|en|propositional variable}}と[[論理演算]]を表す[[論理記号の一覧|記号]]と括弧で定義され、命題変数を表すアルファベットは論理演算記号や括弧を含まないものとされる。論理式はそれらを並べたものである。

論理式は次のように[[再帰的定義|再帰的に定義]]される。
*命題変数は、単独でも論理式である。
*『{{Mvar|φ}}』が論理式であるとき『{{math|{{Font|&not;|font=monospace}}{{Mvar|φ}}}}』も論理式である。
*『{{Mvar|φ}}』と『{{Mvar|ψ}}』が論理式であるとき、二項結合子を『{{math|{{Font|&bull;|font=monospace}}}}』で表すとすると『{{math|{{Font|({{Mvar|φ}}&bull;{{Mvar|ψ}})|font=monospace}}}}』も論理式である。一般には、『{{math|{{Font|&or;|font=monospace}}}}』『{{math|{{Font|&and;|font=monospace}}}}』『{{math|{{Font|&rarr;|font=monospace}}}}』『{{math|{{Font|&harr;|font=monospace}}}}』といった記号が二項結合子として使われる。

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

:{{math|''&lang;alpha set&rang;'' ::{{=}} {{Font|p{{!}}q{{!}}r{{!}}s{{!}}t{{!}}u{{!}}&hellip;|font=monospace}}}}（命題変数の有限集合）
:{{math|''&lang;form&rang;'' ::{{=}} ''&lang;alpha set&rang;'' {{!}} {{Font|&not;|font=monospace}} ''&lang;form&rang;'' {{!}} {{Font|(|font=monospace}}''&lang;form&rang;'' {{Font|&and;|font=monospace}} ''&lang;form&rang;''{{Font|)|font=monospace}} {{!}} {{Font|(|font=monospace}}''&lang;form&rang;'' {{Font|&or;|font=monospace}} ''&lang;form&rang;''{{Font|)|font=monospace}} {{!}} {{Font|(|font=monospace}}''&lang;form&rang;'' {{Font|&rarr;|font=monospace}} ''&lang;form&rang;''{{Font|)|font=monospace}} {{!}} {{Font|(|font=monospace}}''&lang;form&rang;'' {{Font|&harr;|font=monospace}} ''&lang;form&rang;''{{Font|)|font=monospace}}}}

この文法を使って次のような記号列が記述できる。
:{{math|{{Font|(((p&rarr;q)&and;(r&rarr;s))&or;(&not;q&and;&not;s))|font=monospace}}}}
これは、文法的に正しいので論理式である。一方、
:{{math|{{Font|((p&rarr;q)&rarr;(qq))p))|font=monospace}}}}
こちらは文法に従っていないので論理式ではない。

複雑な論理式、特に括弧を多用した論理式は理解するのが難しい。この問題を緩和するため、数学における[[演算子の優先順位]]のように結合子間の優先順位を設けることもできる。例えば、優先される順に『{{math|{{Font|&not;|font=monospace}}}}』『{{math|{{Font|&rarr;|font=monospace}}}}』『{{math|{{Font|&and;|font=monospace}}}}』『{{math|{{Font|&or;|font=monospace}}}}』とする。すると
:{{math|{{Font|(((p&rarr;q)&and;(r&rarr;s))&or;(&not;q&and;&not;s))|font=monospace}}}}
という論理式は次のようにも表現できる。
:{{math|{{Font|p&rarr;q&and;r&rarr;s&or;&not;q&and;&not;s|font=monospace}}}}
ただし、これは論理式の記述を簡略化するための単なる取り決めである。したがって例えば、左結合性で優先順を『{{math|{{Font|&not;|font=monospace}}}}』『{{math|{{Font|&and;|font=monospace}}}}』『{{math|{{Font|&or;|font=monospace}}}}』『{{math|{{Font|&rarr;|font=monospace}}}}』と取り決めれば、上の括弧のない論理式は次のように解釈される。
:{{math|{{Font|(p&rarr;(q&and;r))&rarr;(s&or;((&not;q)&and;(&not;s)))|font=monospace}}}}

== 述語論理 ==
[[一階述語論理]] <math>\mathcal{QS}</math> における論理式の定義は、その理論の{{仮リンク|シグネチャ (論理)|en|Signature (logic)|label=シグネチャ}}に左右される。シグネチャとは、当該理論の非論理記号である定数記号、述語記号、関数記号を指定するもので、同時に関数記号や述語記号のアリティ（引数の数）の定義もシグネチャに含まれる。

シグネチャ<math display="inline">\Sigma</math>を指定したうえで、'''項'''を以下によって再帰的に定義する。項とは、[[議論領域]]の対象物を表現したものである。

# 任意の変数は項である。
# シグネチャ<math display="inline">\Sigma</math>に含まれる任意の定数記号は項である。
# ''t''<sub>1</sub>、&hellip;、''t''<sub>''n''</sub> が項、''f'' がアリティ ''n'' の関数記号ならば、''f''(''t''<sub>1</sub>,&hellip;,''t''<sub>''n''</sub>) は項である。

次に[[原子論理式]]が定義される。
# ''t''<sub>1</sub> と ''t''<sub>2</sub> が項ならば、''t''<sub>1</sub>=''t''<sub>2</sub> は原子論理式である。
# ''R'' がアリティ ''n'' の述語記号、''t''<sub>1</sub>、&hellip;、''t''<sub>''n''</sub> が項ならば、''R''(''t''<sub>1</sub>,&hellip;,''t''<sub>''n''</sub>) は原子論理式である。

最後に論理式は、原子論理式の集合を含む最小の集合として次のように定義される。
# 任意の原子論理式は論理式である。
# <math>\ \phi</math> が論理式ならば、<math>\neg\phi</math> は論理式である。
# <math>\ \phi</math> と <math>\ \psi</math> が論理式ならば、<math>(\phi \land \psi)</math> と <math>(\phi \lor \psi)</math> は論理式である。
# <math>\ x</math> が変数、<math>\ \phi</math> が論理式ならば、<math>\exists x\, \phi</math> は論理式である。
# <math>\ x</math> が変数、<math>\ \phi</math> が論理式ならば、<math>\forall x\, \phi</math> は論理式である（<math>\forall x\, \phi</math> は <math>\neg\exists x\, \neg\phi</math> の省略形と定義することもできる）。

何らかの変数 <math>\ x</math> があるとき、<math>\exists x</math> あるいは <math>\forall x</math> が全く出現しない論理式は'''量化子のない論理式'''と呼ばれる。量化子のない論理式の前に[[存在記号|存在量化]]がある論理式を'''存在論理式'''と呼ぶ。

=== 原子論理式と開論理式 ===
{{Main|原子論理式}}
原子論理式とは、[[論理演算|論理結合子]]や[[量化|量化子]]を含まない論理式、あるいは厳密な部分論理式を持たない論理式である。原子論理式の厳密な形式は、どんな[[形式体系]]のものかで変わってくる。例えば[[命題論理]]での原子論理式は{{仮リンク|命題変数|en|propositional variable}}である。[[一階述語論理]]では、項である引数を伴った述語記号が原子論理式である。

量化子を伴わず、論理結合子のみを使って原子論理式を結合した論理式を「開論理式」と呼ぶこともある<ref>[https://books.google.fr/books?id=IMgg0Uc00I4C&printsec=frontcover&dq=Logic+from+Russell+to+Church&hl=ja&sa=X&ei=QjtiUaO1E8i4rgfN94GoCg&ved=0CCwQ6AEwAA#v=onepage&q=Logic%20from%20Russell%20to%20Church&f=false 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.</ref>。

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

== 属性 ==
* 言語 <math>\mathcal{Q}</math> における論理式が「[[妥当性|妥当]]」であるとは、<math>\mathcal{Q}</math> のあらゆる[[解釈]]において真であることを意味する。
* 言語 <math>\mathcal{Q}</math> における論理式が「{{仮リンク|充足可能性と妥当性|en|satisfiability and validity|label=充足可能}}」であるとは、<math>\mathcal{Q}</math> のある解釈で真であることを意味する。
* A が [[ペアノの公理|算術]] における論理式で、それが「決定可能」であるとは、それが[[帰納的集合|決定可能集合]]を表している場合、すなわち A に出現する自由変数に値を代入したとき、その真偽を判定する実効的方法がある場合である。

== 語誌 ==
[[ファイル:Formal languages.svg|thumb|300px|right|[[形式言語]]を構成する統語論的実体の概念図。記号（{{lang-en-short|symbol}}）と記号列（{{lang-en-short|strings of symbols}}）は、その形式言語に含まれないものと含まれるもの（整式）に大別される。形式言語はその論理式の集合と等価と考えることができる（大袈裟な言いかたをしているだけで、コンピュータの[[プログラミング言語]]で言えば要するに、構文規則に沿ってないソースコードは構文エラー（シンタックスエラー）である、というのと同じ話）。論理式の集合は[[定理]] (theorem) とそうでないものに大別される。]]
初期の[[数理論理学]]者の幾人かは、『{{lang|en|formula}}』を「単なる記号列」、『{{lang|en|well-formed formula}}』を「{{lang|en|formula}} のうち、正しい構成規則に従って作られた記号列」として区別し<ref>Alonzo Church, [1996] (1944), Introduction to mathematical logic, page 49</ref>、幾人かは単に「{{lang|en|formula}}」と総称した<ref>Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea</ref><ref>Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6</ref><ref>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</ref><ref>Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3</ref>。

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

とはいえある程度は意識される概念であり、{{lang|en|well-formed formula}} という句は様々な著作に見られる<ref>Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3</ref><ref>R. L. Simpson (1999), Essentials of Symbolic Logic, page 12</ref><ref>Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall</ref>。

== 脚注 ==
{{Reflist}}

== 参考文献 ==
*{{Citation |first1=Layman E. |last1= Allen |title=Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games | journal= Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council |series= Monographs of the Society for Research in Child Development |volume=30 |issue=1 |year=1965 |pages=29–41}}
* {{Citation | last1=Boolos | first1=George | last2=Burgess | first2=John | last3=Jeffrey | first3=Richard | title=Computability and Logic | publisher=[[ケンブリッジ大学出版局|Cambridge University Press]] | edition=4th | id={{ISBN2|978-0-521-00758-0}} (pb.) | year=2002}}
* {{Citation | last1=Enderton | first1=Herbert | title=A mathematical introduction to logic | publisher=Academic Press | location=Boston, MA | edition=2nd | isbn=978-0-12-238452-3 | year=2001}}
* {{Citation | last1=Gamut | first1=L.T.F. | title=Logic, Language, and Meaning, Volume 1: Introduction to Logic |publisher= University Of Chicago Press | year= 1990 | isbn=0-226-28085-3}}
*{{Citation | author-last=Hodges | author-first=Wilfrid | section=Classical Logic I: First-Order Logic | editor1-last=Goble | editor1-first=Lou | title=The Blackwell Guide to Philosophical Logic | publisher=Blackwell | isbn=978-0-631-20692-7 | year=2001}}
*{{Citation | last1=Hofstadter | first1=Douglas | author1-link=ダグラス・ホフスタッター | title=[[ゲーデル、エッシャー、バッハ|Gödel, Escher, Bach: An Eternal Golden Braid]] | publisher=Penguin Books | isbn=978-0-14-005579-5 | year=1980}}
* {{Citation | last1=Kleene | first1=Stephen Cole | author1-link=スティーヴン・コール・クリーネ | title=Mathematical logic | origyear=1967 | publisher=[[ドーヴァー出版|Dover Publications]] | location=New York | isbn=978-0-486-42533-7 | mr=1950307 | year=2002 |ref={{SfnRef|Kleene|1967}}}}
* {{Citation |last=Rautenberg |first=Wolfgang |doi=10.1007/978-1-4419-1221-3 |title=A Concise Introduction to Mathematical Logic |url= http://www.springerlink.com/content/978-1-4419-1220-6/ |publisher=Springer Science+Business Media |location=[[ニューヨーク|New York]] |edition=3rd |isbn=978-1-4419-1220-6 |year=2010}}

== 関連項目 ==
*[[原子論理式]]

== 外部リンク ==
* {{Cite news | first=Rachel | last=Ehrenberg | title=He's Positively Logical | date=Spring 2002 | publisher=University of Michigan | url= http://www.umich.edu/~newsinfo/MT/02/Spr02/mt9s02.html | work=Michigan Today | accessdate=2007-08-19}}{{リンク切れ|date=2020年5月}}
* [http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/construction/wff_intro.html Well-Formed Formula for First Order Predicate Logic] - includes a short [[Java]] quiz.
* [http://www.apronus.com/provenmath/formulas.htm Well-Formed Formula at ProvenMath]
* [http://wffnproof.com/ WFF N PROOF game site]{{リンク切れ|date=2020年5月}}
* {{Kotobank|論理式}}

{{Mathematical logic}}
{{Logic}}

{{DEFAULTSORT:ろんりしき}}
[[Category:論理式|*]]
[[Category:形式言語]]
[[Category:数理論理学]]
[[Category:述語論理]]
[[Category:数学に関する記事]]