論理式

形式言語を構成する統語論的実体の概念図。記号 (symbol) と記号列 (strings of symbols) は、その形式言語に含まれないものと含まれるもの（整式）に大別される。形式言語はその整論理式の集合と等価と考えることができる。整論理式の集合は定理 (theorem) とそうでないものに大別される。

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

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

概要

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

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

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

命題論理

命題論理の論理式は命題論理式とも呼ばれ、例えば $(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$ ($\neg$q $\wedge$ $\neg$s))

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

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

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

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

(((p $\rightarrow$ q) $\wedge$ (r $\rightarrow$ s)) $\vee$ ($\neg$q $\wedge$ $\neg$s))

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

p $\rightarrow$ q $\wedge$ r $\rightarrow$ s $\vee$ $\neg$q $\wedge$ $\neg$s

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

(p $\rightarrow$ (q $\wedge$ r)) $\rightarrow$ (s $\vee$ (($\neg$q) $\wedge$ ($\neg$s)))

述語論理

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

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

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

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

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

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

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) と呼ぶこともある。

閉論理式

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

論理式の属性

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

語用論

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

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

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

参考文献

• 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, http://www.springerlink.com/content/978-1-4419-1220-6/ 

関連項目

• 原子論理式

外部リンク

• Ehrenberg, Rachel (Spring 2002). “He's Positively Logical”. Michigan Today (University of Michigan). http://www.umich.edu/~newsinfo/MT/02/Spr02/mt9s02.html 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