求闻百科
搜索
切换搜索
切换菜单
切换个人菜单
查看“合式公式”的源代码
求闻百科,共笔求闻
更多语言
阅读
查看源代码
查看历史
页面
讨论
更多操作
←
合式公式
因为下列原因,您没有权限编辑本页。请逐条确认下列问题是否解决后再试。
您所请求的操作,仅限具有
注册用户
权限的
用户
执行。
若您尚未登录求闻百科账号,请您
登录
求闻百科账号后操作。
您尚未完成实名制验证,因此操作受限。请尽快
完成实名制验证
,或联系
裁决委员会
以
获取操作权限
。
注:若您是非中国大陆用户,您应当联络电子邮件staff
qiuwen.org以获得帮助。
您尚未完成
电子邮件确认
,因此操作受限,请尽快
完成电子邮件确认
。
若您无法完成前述手续,请参考
帮助文档
,或通过适当渠道请求管理员或裁决委员协助。
您可以查看和复制此页面的源代码。
若您无权编辑本页面,您可以
提出编辑请求
,提请有权限者代为编辑。
在[[形式系統]]與[[逻辑]]中,'''WFF'''是'''合式公式'''(well-formed 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>A</math>是合式公式,则<math>\urcorner A</math>是合式公式. # 若<math>A, B</math>是合式公式,则<math>(A\rightarrow B)</math>是合式公式. # 若<math>A</math>是合式公式,<math>x</math>是变元,则<math>\forall xA</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 | | | }} * {{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||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] - 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] [[Category:数理逻辑|H]]
返回
合式公式
。