原子公式

数理逻辑

在数理逻辑中，原子公式（Atomic formula）或原子是没有子公式的公式。把什么公式当作原子依赖于所使用的逻辑。例如在命题逻辑中，唯一的原子公式是命题变量。原子是在逻辑系统中最小的公式。在逻辑系统中的合式公式通常通过识别所有有效的原子公式，和给出从两个原子公式建立公式的规则而递归的定义。

公式简介

在离散数学中，设R（）是Γ的任意n元谓词，t1,t2,…,tn是任意F的任意的n个项，则称R（t1,t2,…tn）是Γ的原子公式。通常，原子公式由若干谓词符号和项组成，常量符号是最简单的的项，用来表示域内的物体或实体，它可以是实际的物体，也可以是概念或有名字的事情，变量符号也是项，它不必涉及是哪一个实体。在逻辑系统中的合式公式通常通过识别所有有效的原子公式，和给出从两个原子公式建立公式的规则而递归的定义。从原子公式制作的公式是复合公式。

例如，在命题逻辑中有如下的公式构造规则:

任何命题变量 p 是合式原子公式。

所以，我们可以建造任意的复杂的复合公式，比如，从简单的原子公式p、q 和 r 和我们的构造规则构造出 ((p ∧ ¬(q ⇒ r)) ∨ ¬p)。

谓词逻辑

简介

在数学断言、计算机程序以及系统规格说明中经常可以看到含有变量的语句，例如语句“x大于3”，谓词就是“大于3”，谓词表明语句的主语具有的一个性质。

谓词逻辑是一种逻辑模式，是迄今为止能表达思维和推理的最精确方法，是最广泛使用的知识表达方式。谓词逻辑的基本组成部分是谓词符号、变量符号和常量符号，并用圆括号、方括号、花括号和逗号隔开，以表示域内的关系。也可以称之为一阶逻辑。谓词逻辑也分为经典的谓词逻辑和非经典的谓词逻辑，后者包括作为子系统的非经典的命题逻辑。经典的一阶谓词逻辑是谓词逻辑的基本部分。第一个完整的谓词逻辑系统是G.弗雷格在1879年建立的。K.哥德尔等人系统地研究了谓词逻辑的元逻辑问题，证明了重要的定理。

在谓词逻辑中，使用量词应注意以下几点：

(1) 在不同个体域中，命题符号化的形式可能不同，命题的真值也可能会改变。

(2) 在考虑命题符号化时，如果对个体域未作说明，一律使用全总个体域。

(3) 多个量词出现时，不能随意颠倒它们的顺序，否则可能会改变命题的含义。

谓词公式只是一个符号串，没有什么意义，但我们给这个符号串一个解释，使它具有真值，就变成一个命题.。所谓解释就是使公式中的每一个变项都有个体域中的元素相对应。

公理系统

谓词逻辑的普遍有效的公式为数无穷，在一定意义上它们都是逻辑规律。为了系统地研究这类规律,需要对它们作整体的考虑,将它们总括在一个系统之中。谓词演算或者一阶谓词演算就是这样的系统。谓词演算是把谓词逻辑公理化和形式化而建立的形式系统。按照对作为演算出发点的初始符号、公理和变形规则的不同挑选，可以建立不同的谓词演算系统。在初始符号中有符号=的，称为带等词的一阶谓词演算，等词=是一个谓词常元；不带等词的系统就称为（一阶）谓词演算。构成一个谓词逻辑的公理系统的基本要素有：初始符号、形成规则、公理和变形规则等。对此，可以从一个不带等词的系统 F得到说明。 F的初始符号，包括个体变元、谓词变元、联结词和量词以及技术性符号四类。个体变元符号的小写拉丁字母为： x,y,z,x1,y1,z1,x2,…；谓词变元符号为大写拉丁字母，即：F,G,H,F1,G1,…。在原则上,对每一n≥1，应分别列出n元谓词变元，如：F1,G1,H1,…;F 2,G 2,H 2,…；等等。不过,省去上标1,2,…,n，在实践上不会产生混乱。联结词和量词符号为：塡、→、凬；技术性符号为括弧（，）和逗号，。　形成规则规定怎样的符号序列或符号的组合是 F中的合式公式。合式公式经解释后是有意义的。用来描述和讨论 F系统的语言即元语言的符号有：小写希腊字母α，α1，…,αn，δ表示任意的个体变元；fn表示任意的n元谓词变元;大写拉丁字母X,Y表示任意的符号序列。这些符号称为语法变元。F的形成规则有4条：①如果fn是一n元谓词变元,α1,…,αn是个体变元，则fn(α1,…,αn)是一合式公式；

②　如果 X是合式公式，则塡X是合式公式。如果X、Y 是合式公式，则(X→Y)是合式公式；

③　如果X是合式公式，α是个体变元，则(凬α)X是合式公式；

④　只有适合以上①～③的是合式公式。合式公式简称公式。用字母A,B,C表示任意的公式。A,B,C也是语法变元，属于元语言。

合式公式

命题公式是命题逻辑讨论的对象，而由命题变项使用联结词可构成任意多的复合命题，如P∧Q, P∧Q∨R, P→Q等。问题是它们是否都有意义呢？只有一个联结词的命题P, P∧Q, P→Q当然是有意义的。由两个联结词构成的命题P∧Q∨R至少意义不明确, 是先作P∧Q再对R做∨, 还是先作Q∨R再对P作∧呢? P∧Q也有同样的问题。解决运算次序是容易的, 可像初等代数那样使用括号的办法, 在逻辑运算中也常使用圆括号来区分运算的先后次序。这样由命题变项、命题联结词和圆括号便组成了命题逻辑的全部符号。进一步的问题是建立一个一般的原则以便生成所有的合法的命题公式，并能识别什么样的符号串是合法的。

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

合式公式（简记为Wff）的定义：

1. 简单命题是合式公式。

2. 如果A是合式公式, 那么A也是合式公式。

3. 如果A、B是合式公式, 那么(A∧B), (A∨B), (A→B)和(AB)是合式公式。

4. 当且仅当经过有限次地使用1.2.3所组成的符号串才是合式公式。

这个定义给出了建立合式公式的一般原则，也给出了识别一个符号串是否是合式公式的原则。

这是递归（归纳）的定义。在定义中使用了所要定义的概念，如在2和3中都出现了所要定义的合式公式字样，其次是定义中规定了初始情形，如1中指明了已知的简单命题是合式公式。

条件4说明了哪些不是合式公式，而1、2和3说明不了这一点。

依定义，若判断一个公式是否为合式公式，必然要层层解脱回归到简单命题方可判定。

(P∧Q), (P→(P∧Q)),

(((P→Q)∧(Q→R))(P→R))都是合式公式。而P∨Q∨, ((P→Q)→( ∧Q)), (P→Q都不是合式公式, 没有意义, 我们不讨论。