查看“︁公式 (数理逻辑)”︁的源代码

{{Unreferenced|time=2022-10-09T15:11:16+00:00}}
在[[数理逻辑]]中，'''公式'''是{{clarify|表达[[命题]]的[[形式语法]]对象，除了这个命题可能依赖于这个公式的[[自由变量]]的值之外。|post-text=（似乎翻译自英语而语焉不详）}}

公式精确定义依赖于涉及到的特定的形式逻辑，但有如下一个非常典型的定义（特定于[[一阶逻辑]]）：公式是相对于特定[[语言 (数理逻辑)|语言]]而定义的；就是说，一组'''[[常量]]符号'''、'''[[泛函谓词|函数符号]]'''和'''[[谓词变量|关系符号]]'''，这里的每个函数和关系符号都带有一个[[元数]]（arity）来指示它所接受的参数的数目。
==定义==
===项的递归定义===
*一个变量
或
*一个常量符号
或
*<math>f(t_1,...,t_n)\,</math>，这里的<math>f\,</math>是一个''n''-元函数符号，而<math>t_1,...,t_n\,</math>是项。

===公式的递归定义===
*<math>t_1=t_2\,</math>，这里的<math>t_1\,</math>和<math>t_2\,</math>是项
或
*<math>R(t_1,...,t_n)\,</math>，这里的<math>R\,</math>是一个''n''-元关系符号，而<math>t_1,...,t_n\,</math>是项
或
*<math>(\neg \varphi)</math>，这里的<math>\varphi\,</math>是公式
或
*<math>(\varphi\land\psi)\,</math>，这里的<math>\varphi\,</math>和<math>\psi\,</math>是公式
或
*<math>(\exists x)(\varphi)\,</math>，这里的<math>x\,</math>是一个变量而<math>\varphi\,</math>是一个公式。

==解释==
{{original research|段落}}
;公式并''不一定''具备封闭形式（即''不一定''没有[[省略号]]）。
*阶乘“！”、求和式“∑”和求积式“∏”等都隐含省略号。
*排列数和组合数等都含有省略号。

;按照通项公式去计算有时比按照定义去计算更加复杂。

*斐波那契数列公式：
: <math>F_n = \frac{1}{\sqrt{5}} \left\{ \left( \frac{1+\sqrt{5}}{2} \right)^n -  \left( \frac{1-\sqrt{5}}{2} \right)^n \right\} = {\varphi^n \over \sqrt{5}} - {(1-\varphi)^n \over \sqrt{5}}</math>

但是相比较按照这个公式计算<math>f_{n}\,</math>，还是按照递归定义：<math>f_{n}=f_{n-2}+f_{n-1}(n\ge3)\,</math>进行计算更方便。


根据谓词逻辑的语义推导规则，语义应该具有一致性，就是对于一个命题逻辑语句集f，当且仅当至少存在这样一种解释i，f的一切元素在i之下都是真的，那么，f是语义一致的。在命题逻辑语义学内，一个赋值不能同时把真和假给予某个命题原子式。在命题逻辑语义学中，在同一解释下，一个集合不能既属于某个谓词的外延又不属于该谓词的外延。{现代西方哲学逻辑，复旦大学出版社235页}

==原子公式==
{{main|原子公式}}

==参见==
*[[WFF]]
*[[原子公式]]
*[[句子 (数理逻辑)]]
*[[原子句子]]
*[[T-模式]]

==外部链接==
*[http://dlmf.nist.gov/ NIST數學函數]{{Wayback|url=http://dlmf.nist.gov/ |date=20100610075107 }}

{{数理逻辑|state=expanded}}

[[Category:數理邏輯|G]]
[[Category:规则|科学]]