論理式

出典: フリー百科事典『ウィキペディア(Wikipedia)』
整論理式から転送)
移動: 案内検索
形式言語を構成する統語論的実体の概念図。記号 (symbol) と記号列 (strings of symbols) は、その形式言語に含まれないものと含まれるもの(整式)に大別される。形式言語はその整論理式の集合と等価と考えることができる。整論理式の集合は定理 (theorem) とそうでないものに大別される。

論理式(ろんりしき、formula、well-formed formula、wff)とは、論理学において所定の形式文法から生成される形式言語の一部をなす文字列、すなわち、与えられたアルファベットに含まれる記号(シンボル)のを意味する[1]整式整論理式とも。形式言語はその論理式の集合全体と合致するとみなすことができる。

論理式は統語論上の形式的オブジェクトであり、意味論は非形式的に与えることができる。

概要[編集]

論理式は主に命題論理一階述語論理に代表される述語論理で使われている。その文脈において論理式は記号列 φ であり、φ の中の自由変数に値を設定したとき「φ は真か?」という問いが意味を持つ。形式論理において証明はある特性を持つ一連の論理式で表現され、その並びの最後の論理式は証明結果を意味する。

「論理式」という用語は(紙や黒板などに)書かれた記号列を意味するが、より正確にはその記号列が表現しているものを指していると理解され、記号列は論理式の具体的トークンと理解すべきである。具体的トークンがなくとも論理式は存在しうる。したがって形式言語にはトークン実体の有無に関わらず無限個の論理式が存在する。さらに言えば、1つの論理式は複数のトークン実体を持ちうる。

特に命題論理における論理式は命題と解釈されることが多い。しかし論理式は統語論的実体であり、形式言語における論理式は解釈とは無関係に存在する。論理式は、何かの名前形容詞副詞接置詞命令節、一連の節、一連の名前などに解釈される。ある形式言語の記号群を適当に並べれば、意味を持たない論理式となることもある。さらに言えば、論理式はどんな解釈をされる必要もない。

命題論理[編集]

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

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

  • 命題変数は、単独でも論理式である。
  • φ が論理式であるとき、\lnotφ も論理式である。
  • φ と ψ が論理式であるとき、二項結合子を • で表すとすると、(φ • ψ) も論理式である。一般には、∨、∧、→、↔ といった記号が二項結合子として使われる。

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

<alpha set> ::= p | q | r | s | t | u | ... (命題変数の有限集合)
<form> ::= <alpha set> | \neg<form> | (<form>\wedge<form>) | (<form>\vee<form>) | (<form>\rightarrow<form>) | (<form>\leftrightarrow<form>)

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

(((p \rightarrow q) \wedge (r \rightarrow s)) \vee (\negq \wedge \negs))

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

((p \rightarrow q)\rightarrow(qq))p))

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

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

(((p \rightarrow q) \wedge (r \rightarrow s)) \vee (\negq \wedge \negs))

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

p \rightarrow q \wedge r \rightarrow s \vee \negq \wedge \negs

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

(p \rightarrow (q \wedge r)) \rightarrow (s \vee ((\negq) \wedge (\negs)))

述語論理[編集]

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

論理式の定義はいくつかの部分から構成される。まず、 (term) が再帰的に定義される。項とは、議論領域の対象物を表現したものである。

  1. 任意の変数は項である。
  2. シグネチャに含まれる任意の定数記号は項である。
  3. t1,...,tn が項、f がアリティ n の関数記号ならば、f(t1,...,tn) は項である。

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

  1. t1t2 が項ならば、t1=t2 は原子論理式である。
  2. R がアリティ n の述語記号、t1,...,tn が項ならば、R(t1,...,tn) は原子論理式である。

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

  1. \ \phi が論理式ならば、\neg\phi は論理式である。
  2. \ \phi\ \psi が論理式ならば、(\phi \land \psi)(\phi \lor \psi) は論理式である。
  3. \ x が変数、\ \phi が論理式ならば、\exists x\, \phi は論理式である。
  4. \ x が変数、\ \phi が論理式ならば、\forall x\, \phi は論理式である(\forall x\, \phi\neg\exists x\, \neg\phi の省略形と定義することもできる)。

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

原子論理式と開論理式[編集]

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

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

閉論理式[編集]

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

論理式の属性[編集]

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

語用論[編集]

初期の数理論理学では、論理式 (formula) は単なる記号列、整論理式 (wff) はその中でも正しい構成規則に従って作られた記号列とされていた[4]

何人かの学者は単に論理式 (formula) と呼んでいる[5][6][7][8]。現代においては(特に計算機科学の文脈でモデル検査自動定理証明などのソフトウェアを扱う場合)、(論理)式といえば代数学的な概念とされ、well-formedness すなわち(論理)式を表す具体的文字列表現の規定(結合子や量化子にどの記号を用いるか、どのような括弧の使い方にするか、ポーランド記法中置記法かなど)は単なる記法の問題とされることが多い。

それでも well-formed formula という記述は様々な著作に見られるが[9][10][11]、任意の記号列という formula の古典的定義に対応する概念という使い方ではなく(むしろ fomula と wff は同義として使われている)、formula をそのような意味で使う数理論理学の用法は廃れた。

脚注[編集]

  1. ^ 論理式は論理学の初歩的概念であり、全ての入門書で説明されている。例えば Enderton 2001, Gamut 1990, Kleene 1967
  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

参考文献[編集]

関連項目[編集]

外部リンク[編集]