定理
若A(u1，u2，…，un)是有效的 iff ∀x1∀x2…∀xnA(x1，x2，…，xn) 是有效的。
证明：
A(u)有效 A(u)有效 iff ¬A(u)不可满足 ¬A(u)不可满足 iff ∃x(¬A(x))不可满足 ∃x(¬A(x))不可满足 iff ¬∀xA(x)不可满足 ¬∀xA(x)不可满足 iff ∀xA(x)有效的 ∀xA(x)有效的 使用归纳证明即可。
证明：
必要性：假设A 必要性：假设A ∉ ∑。 由∑是极大协调的，则∑∪{A}是不协调的，即 是极大协调的，则∑ {A}是不协调的，即 存在存在B Form(L ，使得∑ 存在存在B∈Form(L )，使得∑├B且∑├¬B。 可得∑ 可得∑， A ├B且∑，A ├¬B。因此， ∑├ ¬A。 因此， 这与∑ 这与∑协调矛盾。 充分性：易证。
可靠性定理（一） 可靠性定理（
设∑⊆Form(L )，A∈Form(L )。 Form(L Form(L
若∑├A，则∑╞A。 ，则∑ 若Ф├A，则Ф╞A。 Ф├A，则Ф
协调性
∑⊆Form(L )是协调的，当且仅当不存在 Form(L A∈Form(L )，使得∑├A且∑├¬A。 Form(L ，使得∑
定理
若A(u1，u2，…，un)是可满足的 iff ∃x1∃x2…∃xnA(x1，x2，…，xn) 是可满足的。
证明：
A(u)可满足 A(u)可满足 iff 存在赋值v，使得A(u)v=1 存在赋值v，使得A(u) v(u/uv)=1 iff 存在赋值v，使得A(u) 存在赋值v，使得A(u) iff 存在赋值v，使得(∃xA(x))v=1 存在赋值v，使得(∃xA(x)) iff ∃xA(x)可满足 ∃xA(x)可满足 使用归纳证明即可。
引理：设∑ Form(L 是极大协调集，构作真假赋值v 引理：设∑⊆Form(L p)是极大协调集，构作真假赋值v， 使得对于任何原子公式p 使得对于任何原子公式p，pv=1当且仅当p∈ ∑。于是， =1当且仅当p 对于任何A Form(L 对于任何A∈Form(L p)， Av=1当且仅当A∈ ∑。 =1当且仅当A 证明：
定理：
设∑⊆Form(L )是极大协调的。对于任何A Form(L 是极大协调的。对于任何A ∈Form(L )，¬A∈∑ iff A ∉ ∑。 Form(L
证明：
必要性：假设A 必要性：假设A∈∑。可得， ∑├A。 又因为¬ 又因为¬A∈∑，且∑├¬A 。这与∑协调矛盾。 这与∑ 充分性：因为A 充分性：因为A ∉ ∑且∑是极大协调的， ∑∪{A} 是不协调的，即存在B Form(L ，使得∑ 是不协调的，即存在B∈Form(L )，使得∑， A├B且∑，A├¬B，可得∑├¬A 。所以¬A∈∑。 ，可得∑ 。所以¬
可靠性定理（二） 可靠性定理（
设∑⊆Form(L )，A∈Form(L )。 Form(L Form(L
若∑是可满足的，则∑是协调的。 是可满足的，则∑是协调的。 若A是可满足的，则A是协调的。 是可满足的，则A是协调的。
证明：
假设∑是不协调的。即存在A Form(L 假设∑是不协调的。即存在A∈Form(L )，使得 ∑├A且∑├¬A。由可靠性定理（一），得到， ∑╞A且∑╞¬A。 因为∑是可满足的，可得，存在赋值v，使得∑ =1。 因为∑是可满足的，可得，存在赋值v，使得∑v=1。 =1，矛盾。 所以A =1且 所以Av=1且(¬A)v=1，矛盾。
极大协调性
∑⊆Form(L )是极大协调的，当且仅当 Form(L
∑是协调的。 是协调的。 对于任何A 对于任何A ∉ ∑，∑∪{A}是不协调的。 {A}是不协调的。
称∑为封闭于形式可推演性的，若对于任何 A， ∑├A蕴含A∈∑。 蕴含A
定理：
设∑⊆Form(L )是极大协调的。对于任何A Form(L 是极大协调的。对于任何A ∈Form(L )，∑├A iff A∈∑。 Form(L A∈
i）若A是原子公式，成立。 ）若A ii）¬A∈ ∑ iff A ∉ ∑ iff Av=0 iff (¬A)v=1。 ii）¬A∈ =1。 iii）A∧B∈ ∑ iff A ∈ ∑且B ∈ ∑ iff Av=1且 Bv=1 iff (A ∧ B)v=1。 iii） =1且 =1。 iv） A∨B∈ ∑ iff A ∈ ∑或B ∈ ∑ iff Av=1或 Bv=1 iff (A ∨ B)v=1。 iv） =1或 =1。 v） A→B∈ ∑ iff A ∈ ∑蕴含B ∈ ∑ iff Av=1蕴含Bv=1 iff (A → 蕴含B =1蕴含B B)v=1。 =1。 vi） A↔B∈ ∑ iff A ∈ ∑等值于B ∈ ∑ iff Av=1等值于 Bv=1 iff vi） A↔B 等值于B =1等值于 (A↔B =1。 (A↔B)v=1。
定理：
∑⊆Form(L )是协调的，当且仅当存在 Form(L A∈Form(L )，使得∑├/ 。 Form(L ，使得∑ A
证明：
必要性：假设对于任何A Form(L 必要性：假设对于任何A∈Form(L )，∑├A。这 与∑是协调的相矛盾。 充分性：假设∑是不协调的，即存在B Form(L 充分性：假设∑是不协调的，即存在B∈Form(L )， 使得∑ 使得∑├B且∑├¬B。则对于任何A∈Form(L ) ， 。则对于任何A Form(L ∑，¬A├B且∑，¬A ├¬B，可得到∑├A。矛盾。 ¬A├ ，可得到∑
定理：
A可满足 iff A的前束范式是可满足的 A的前束范式是可满足的 A有效 iff A的前束范式是有效的 A的前束范式是有效的
定义：
∑在论域D中可满足 iff 存在以D为论域的赋值v， 在论域D 存在以D为论域的赋值v 使得∑ =1。 使得∑v=1。 A在论域D中有效 iff 对于任何以D为论域的赋 在论域D 对于任何以D 值v，Av=1。 =1。
定理：
设∑⊆Form(L )是极大协调的。对于任何A， Form(L 是极大协调的。对于任何A B∈Form(L )，A∧B∈∑ iff A∈∑并且B∈∑。 Form(L A∈ 并且B
证明：
必要性：因为A 必要性：因为A∧B∈∑。可得， ∑├A ∧B。 进一步得到， ∑├A 且∑├ B 。所以A∈∑且 。所以A B∈∑。 充分性：因为A 充分性：因为A∈∑且B∈∑。可得，∑├A 且 。可得，∑ ∑├ B。 进一步得到， ∑├A ∧B 。所以A∧B∈∑。 。所以A
定理：设∑ Form(L 定理：设∑⊆Form(L p)，A∈Form(L p)，且∑为有限集。 Form(L ，且∑
若Ф╞ A，则Ф├A 。 ，则Ф├A 若∑╞A ，则∑├A 。 ，则∑
证明：
设A含不同的原子公式p1，p2，…，pn。令v1，v2是真假赋值， 含不同的原子公式p 。令v1，v2是真假赋值， 且p1v1=1， p1v2=0， p2v1= p2v2=1，piv1= piv2，i=3，…，n。由 =1， =0， =1， i=3， 引理，由于A =1，所以p 引理，由于Av1=1，所以p1，p2 ，…，An├A。由于Av2=1，所 。由于A =1，所 以¬p1，p2 ，…，An├A。可得， p1 ∨ ¬p1 ，p2 ，…，An├A， p2 ，…，An├ (p1 ∨ ¬p1 ) →A (p 又因为Ф├ 又因为Ф├ p1 ∨ ¬p1 ，所以 p2 ，…，An├ p1 ∨ ¬p1 。 可得， p2 ，…，An├ A。 再令u1，u2是真假赋值，且p =1， 再令u1，u2是真假赋值，且p1u1=1， p1u2=0， p2u1= p2u2=0，piu1= =0， =0， piu2，i=3，…，n。同理可得， ¬p2 ，…，An├ A。 i=3， 可得， A3 ，…，An├ A。 进一步指定真假赋值，可得Ф├A 进一步指定真假赋值，可得Ф├A 。
定理：
任何协调集都可扩充为极大协调集。
引理：
设A ∈Form(L p)含不同的原子公式p1，p2，…， Form(L 含不同的原子公式p pn，v是真假赋值。对于i=1，2，…，n，令 是真假赋值。对于i=1， 若piv=1，则Ai=pi；否则，Ai=¬pi。则 =1，则A ；否则，A 若Av=1，则A1，A2 ，…，An├A。 =1，则A 若Av=0，则A1，A2 ，…，An├¬A。 =0，则A
定理：
设∑⊆Form(L )是极大协调的。对于任何A，B∈Form(L )， Form(L 是极大协调的。对于任何A Form(L A∨B∈∑ iff A∈∑或B∈∑。 A∈
证明：
必要性：假设A 必要性：假设A ∉ ∑且B ∉ ∑。 可得， ¬A∈∑且¬B∈∑。 ¬B∈ 进一步可得，¬ 进一步可得，¬A ∧ ¬B∈∑， ¬(A ∨ B)∈ ∑， ∑├ ¬(A ¬B∈ ¬(A B)∈ ¬(A ∨ B) 。 又因为A 又因为A∨B∈∑， ∑├ A ∨ B。这与∑协调矛盾。 。这与∑ 充分性：因为A 充分性：因为A∈∑或B∈∑。可得，∑├A ∨B 或∑├ B 。可得，∑ ∨ A。 进一步得到， A ∨ B∈∑。
定理：
设∑⊆Form(L )是极大协调的。对于任何A， Form(L 是极大协调的。对于任何A B∈Form(L )， Form(L A→B∈∑ iff A∈∑蕴含B∈∑。 A∈ 蕴含B A↔B∈∑ iff A∈∑等值于B∈∑。 ↔B∈ A∈ 等值于B
定理：
设∑⊆Form(L )是极大协调的。对于任何A Form(L 是极大协调的。对于任何A ∈Form(L )，∑├/ iff ¬A∈∑。 Form(L A
命题逻辑的完备性定理（一） 命题逻辑的完备性定理（
设∑⊆Form(L p)，A∈Form(L p)。 Form(L Form(L
若∑是协调的，则∑是可满足的。 协调的，则∑ 可满足的 若A是协调的，则A是可满足的，所以∑ 因为∑是协调的，所以∑可以扩充为极大协调集 对于任何B 。因此，可得B =1， ∑*。对于任何B∈∑， B∈∑*。因此，可得Bv=1， v是构作真假赋值。即∑是可满足的。 是构作真假赋值。即∑ 可满足的。