命题公式的类型
命题公式的类型分为：永真式、可满足式、矛盾式。命题永真公式亦称重言式，是一种命题公式。对于任何指派，其真值总是真的命题公式称为命题的永真公式。可满足式（satisfiable）是一个数学公式，设A为任一命题公式，若A在各种真值指派下至少存在一组成真指派，则A是可满足式，反之为矛盾式。换言之，对于命题公式A，若A不是矛盾式，则称A是可满足式。矛盾式（contradictory formula）又称永假式、不可满足公式，是逻辑演算的一类公式。如果对任意一个赋值V，都有V[A]=0，即公式A对任一赋值均取“假”值，则公式A为矛盾式。命题公式介绍及定义：命题公式：命题公式（propositional formula）亦称合式公式，是数理逻辑术语，它是按照一定规律形成的符号序列，在命题演算中，公式通常用归纳定义给出。命题公式是对由命题变项、联结间和圆括号按照一定逻辑关系构成的复合命题的形式化描述。定义：1、设A是一个命题公式，是出现在A中的所有命题变项。对这些命题变项各赋予一个确定的真值，那这一组真值称为对命题公式的一种赋值。2、设A、B是命题公式，是出现在A和B中的所有命题变项，如果对于的任何一组赋值，A的真值和B的真值都相同，则称公式A等值于公式B（或A与B等值）。
合适公式是命题吗?
不是。
合式公式（或叫做命题公式）是由命题变元和连接词构成的式子。没有确定的真值，即不能判断真假，所以不是命题。当用命题常量替代命题变元后，合式公式变为命题，但此时它就不再是合式公式了。
这与其他数学公式类似。比如公式：X = (X1 + X2 + ……+Xn) / n 是用于计算各门课程平均成绩的公式。但这个公式本身，计算不出任何结果。它不能代表任何一个人的平均成绩——它只是表达了单科成绩与平均成绩的关系。只有带入具体数值，它才真正可以计算某个人的平均成绩。
谓词演算的形成规则
形成规则定义项，公式和自由变量。项项的集合按如下规则递归的定义：任何常量是项。任何变量是项。n ≥ 1 个参数的任何表达式 f(t1,...,tn) （这里的每个参数 ti 都是项，而 f 是 n 价的函数符号） 是项。闭包条款： 其他东西都不是项。合式公式合式公式（通常叫做 wff 或只是公式）按如下规则递归的定义：简单和复杂谓词 如果 P 是 n ≥ 1 价的关系而 ai 是项，则 P(a1,...,an) 是合式的。如果等式被认为是逻辑的一部分，则 (a1 = a2） 是合式的。所有这个公式都被称为是原子。归纳条款 I: 如果 φ 是 wff，则 ¬；φ 是 wff。归纳条款 II: 如果 φ 和 ψ 是 wff，则 （φ → ψ） 是 wff。归纳条款 III: 如果 φ 是 wff 而 x 是变量，则x φ 是 wff。闭包条款： 其他东西都不是 wff。因为 ¬；（φ → ¬；ψ） 逻辑等价于 （φ ∧ ψ），（φ ∧ ψ） 经常用做简写。（φ ∨ ψ） 和 （φ ψ） 也是同样的道理。还有x φ 是 ¬?y ¬；φ 的简写。实际中，如果 P 是 2 价关系，我们经常写 a P b 替代 P a b；例如，我们写 1 < 2 而不是 <（1 2）。类似的，如果 f 是 2 价函数，我们有时写 a f b 替代 f(a b)；例如，我们写 1 + 2 而不是 +（1 2）。经常省略某些圆括号，如果不导致歧义的话。有时声称 P(x) 对精确的一个 x 成立是有用的，这可表达为！x P(x）。还可以表达为x (P(x) ∧y (P(y) → (x = y)))。在计算机科学术语中，公式实现内置“布尔”类型，而项实现所有其他类型。自由变量原子公式 如果 φ 是原子公式则 x 在 φ 中是自由的，当且仅当 x 出现在 φ 中。归纳条款 I: x 在 ¬；φ 中是自由的，当且仅当 x 在 φ 中是自由的。归纳条款 II: x 在 （φ → ψ） 中是自由的，当且仅当 x 在 φ 中是自由的或者 x 在 ψ 中是自由的。归纳条款 III: x 在y φ 中是自由的，当且仅当 x 在 φ 中是自由的并且 x?y。闭包条款： 如果 x 在 φ 中不是自由的，则它是约束的。例如，在 x y (P(x) Q(x,f(x),z)) 中，x 和 y 是约束变量，而 z 是自由变量，而 w 不是二者因为它没有出现在任何公式中。
