数理論理学、命題論理、述語論理における well-formed formula とは、形式文法の規則に合った式のことである。論理式や整論理式ということもある。

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

語誌編集

 
形式言語を構成する統語論的実体の概念図。記号 (symbol) と記号列 (strings of symbols) は、その形式言語に含まれないものと含まれるもの(整式)に大別される。形式言語はその整論理式の集合と等価と考えることができる(大袈裟な言いかたをしているだけで、コンピュータのプログラミング言語で言えば要するに、構文規則に沿ってないソースコードは構文エラー(シンタックスエラー)である、というのと同じ話)。整論理式の集合は定理 (theorem) とそうでないものに大別される。

初期の数理論理学者の幾人かは、"formula" を「単なる記号列」、wff を「formulaのうち、正しい構成規則に従って作られた記号列」として区別し[1]、幾人かは単に "formula" と総称した[2][3][4][5]

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

とはいえある程度は意識される概念であり、well-formed formula というフレーズは様々な著作に見られる[6][7][8]

命題論理編集

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

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

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

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

<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))

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

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

(((p   q)   (r   s))   ( q    s))

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

p   q   r   s    q    s

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

(p   (q   r))   (s   (( q)   ( s)))

述語論理編集

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

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

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

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

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

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

  1. 任意の原子論理式は論理式である。
  2.   が論理式ならば、  は論理式である。
  3.    が論理式ならば、   は論理式である。
  4.   が変数、  が論理式ならば、  は論理式である。
  5.   が変数、  が論理式ならば、  は論理式である(   の省略形と定義することもできる)。

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

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

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

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

閉論理式編集

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

属性編集

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

脚注編集

  1. ^ Alonzo Church, [1996] (1944), Introduction to mathematical logic, page 49
  2. ^ Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea
  3. ^ Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6
  4. ^ 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
  5. ^ Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3
  6. ^ Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
  7. ^ R. L. Simpson (1999), Essentials of Symbolic Logic, page 12
  8. ^ Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall
  9. ^ First-order logic and automated theorem proving, Melvin Fitting, Springer, 1996
  10. ^ 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.

参考文献編集

  • 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/ 

関連項目編集

外部リンク編集