查看“︁合式公式”︁的源代码

在[[形式系統]]與[[逻辑]]中，'''合式公式'''（well-formed formula，WFF）又称'''合適公式'''<ref>http://terms.naer.edu.tw/detail/18145751/{{Dead link}}</ref>、'''良式公式'''，可简称'''公式'''（formula），即“符合語法規則的公式”，是一逻辑体系中的“一个[[表达式]]”或“一个有限[[符号]]序列”；此表达式或序列，来自给定的[[字母表]]（字符），且属于形式语言的一种。合式公式与该逻辑体系的构成规则相符合，类似于自然语言中的一个语法句子。

若给定一[[形式文法]]，则WFF是这个文法生成的任何字符串。

例如，在[[命题演算]]中符号序列<math>((\alpha\rightarrow\beta)\rightarrow(\neg\beta\rightarrow\neg\alpha))</math>是一个WFF，因为它在文法上正确。符号序列<math>((\alpha\rightarrow\beta)\rightarrow(\beta\beta))\alpha))</math>不是WFF，因为它不符合命题演算的文法。

在形式逻辑中，[[证明]]是有特定性质的WFF序列，而序列中最终的WFF就是要证明的。

== 命题逻辑中的合式公式 ==
设S是联结词的集合. 由S生成的合式公式定义如下：
# [[原子公式]]是由S生成的合式公式.
# 若c是S中的0元联结词，则c是由S生成的合式公式.
# 若n<math>\geqslant</math>1，<math>F</math>是S中的n元联结词，<math>A_1, A_2,..., A_n</math>是由S生成的公式，则<math>FA_1A_2... A_n</math>是由S生成的合式公式.

== [[一階邏輯|谓词逻辑]]中的合式公式 ==
合式公式是按以下规则构成的有穷长符号串：
# [[原子公式]]是合式公式.
# 若<math>\mathcal{A}</math>是合式公式，则<math>(\neg \mathcal{A})</math>是合式公式.
# 若<math>\mathcal{A},\,\mathcal{B}</math>是合式公式，则<math>(\mathcal{A}\Rightarrow \mathcal{B})</math>是合式公式.
# 若<math>\mathcal{A}</math>是合式公式，<math>x</math>是变元，则<math>(\forall x\mathcal{A})</math>是合式公式.

==参见==
*[[公式 (数理逻辑)]]

==參考文獻==
{{refbegin|2}}
*{{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
  | author1-link=:en:George Boolos
  | last2=Burgess
  | first2=John
  | last3=Jeffrey
  | first3=Richard
  | author3-link=:en:Richard Jeffrey
  | title=Computability and Logic
  | publisher=[[Cambridge University Press]]
  | edition=4th
  | isbn=978-0-521-00758-0 
  | year=2002}}
* {{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
 |deadurl     = yes
 |archiveurl  = https://web.archive.org/web/20090208141433/http://umich.edu/~newsinfo/MT/02/Spr02/mt9s02.html
 |archivedate = 2009-02-08
}}
* {{Citation
  | last1=Enderton
  | first1=Herbert
  | title=A mathematical introduction to logic
  | publisher={{link-en|Academic Press|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
 | last=Hodges
 | 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=Douglas Hofstadter
  | 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=:en:Stephen Kleene
  | title=Mathematical logic
  | origyear=1967
  | publisher={{link-en|Dover Publications|Dover Publications}}
  | location=New York
  | isbn=978-0-486-42533-7
  | mr=1950307 
  | year=2002
}}
* {{Citation|last=Rautenberg|first=Wolfgang|authorlink=:en:Wolfgang Rautenberg|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 City|New York]]|edition=3rd|isbn=978-1-4419-1220-6|year=2010}}{{Dead link|date=2020年2月 |bot=InternetArchiveBot |fix-attempted=yes }}
{{refend}}

==外部連結==
*[http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/construction/wff_intro.html Well-Formed Formula for First Order Predicate Logic]{{Wayback|url=http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/construction/wff_intro.html |date=20060320104444 }} - includes a short [[爪哇岛|Java]] quiz.
*[http://www.apronus.com/provenmath/formulas.htm Well-Formed Formula at ProvenMath]{{Wayback|url=http://www.apronus.com/provenmath/formulas.htm |date=20160405072544 }}
*[http://wffnproof.com/ WFF N PROOF game site]{{Wayback|url=http://wffnproof.com/ |date=20121114004740 }}

[[Category:形式语言]]
[[Category:元逻辑学]]
[[Category:句法 (逻辑学)]]
[[Category:數理邏輯]]
[[Category:逻辑表达式| ]]