自动推理的逻辑04-命题微积分

自动推理的逻辑04-命题微积分

任何逻辑的两个重要属性是
可靠性soundness: Γ ⊢ α ⇒ Γ |= α
完整性completeness: Γ |= α ⇒ Γ ⊢ α
可靠性保证人们不能从真实的假设中推断出错误
完整性可以推断出真实假设的所有后果
重言式，蕴涵，等价Tautologies, Entailment, Equivalence
α ∈ Φ is a tautology (or valid), written |= α,
if [α]v = 1 for all v
Γ ⊆ Φ (semantically) entails α ∈ Φ, written Γ |= α,
if [β]v = 1 implies [α]v = 1 for all v and β ∈ Γ
α, β ∈ Φ are logically equivalent, written α ≡ β,
if [α]v = [β]v for all v

经典命题微积分的健全性和完备性
对于完整性/完整性证明，我们考虑限制语法
Φ ::= ⊥ | p | (Φ ∧ Φ) | (Φ → Φ)
回想一下，我们处于经典逻辑中，因此我们可以推导出其他连接词。
¬α ⊣⊢ α → ⊥
⊤ ⊣⊢ ¬⊥
α ∨ β ⊣⊢ ¬(¬α ∧ ¬β)

健全性：可证明的事物是有效的
我们将证明稳健性定理：
if Γ ⊆ Φ and α ∈ Φ, then Γ ⊢ α ⇒ Γ |= α
每当Γ ⊢ α 时，我们想证明某事是真的。 这意味着有证据树，其假设在 Γ 中，其结论为 α。
我们将通过考虑证明树而不是陈述 α 本身

建立健全性Establishing soundness
因为我们要证明一些关于递归构造的证明树的东西，所以我们将利用：非空树的结构归纳原理
为了证明声明 Cl(t) 对所有非空树 t 成立，足以：
基本情况：证明 Cl 适用于所有单元素树；
步骤案例：证明，如果一个节点的所有直接子树都满足Cl，那么节点本身为根的树。
这两种类型的证明树是什么样的？

考虑用于基本情况的树
您可以拥有的最小证明树是只有一个元素的证明树。 这些树
只需写下一个陈述 α，但它尚未用于任何东西和证明树的其余部分仍然需要构建。 我们拥有的唯一规则允许我们构建这样的树的是
要么 α ∈ Γ，即它是假设之一
或 α = β ∨ ¬β，即我们使用排中律

Soundness Theorem
if Γ ⊆ Φ and α ∈ Φ, then Γ ⊢ α ⇒ Γ |= α
证明：通过证明树的结构归纳

基本情况：
如果 α ∈ Γ，则 Γ |= α 微不足道，因为任何估值都可以创造一切;在 Γ 中为真必须使 α 为真；
如果 α = β ∨ ¬β，则 α 是重言式，因为 ∨ 的真表是定义。 无论您使用什么估值，α 都会评估为真。

步骤案例：这是使用的最后一条规则是 (→I) 时的证明。
任何 (→I) 证明都通过推导某些 α1、α2 的 Γ ⊢ α1 → α2 得出结论。
直接子证明是 Γ, α1 ⊢ α2 并且我们的归纳假设说
这个证明证明了一些有效的东西，即Γ, α1 |= α2。
换句话说，给定任何赋值 v，
if [α1]v = 1 and [β]v = 1 for all β ∈ Γ,
then [α2]v = 1.
Therefore, for all v,
if every β ∈ Γ satisfies [β]v = 1,
then [α1 → α2]v = 1
thus Γ |= α1 → α2

一致性Consistency
A set Γ ⊆ Φ is consistent if Γ ̸⊢ ⊥
hence Γ is inconsistent if Γ ⊢ ⊥

事实：Γ 一致 ⇔ 无 α 满足 Γ ⊢ α 和 Γ ⊢ ¬α
Proof:
if Γ ⊢ α and Γ ⊢ ¬α for some α, then Γ ⊢ ⊥ by (¬E)
if Γ ⊢ ⊥, then Γ ⊢ α and Γ ⊢ ¬α by (⊥E)

FACT:
Γ ∪ {α} inconsistent ⇒ Γ ⊢ ¬α
Γ ∪ {¬α} inconsistent ⇒ Γ ⊢ α

可满足性意味着一致性Satisfiability Implies Consistency
事实：每组可满足的公式都是一致的

Proof:
Γ inconsistent 	⇒ Γ ⊢ ⊥
				⇒ Γ |= ⊥ (by soundness)
				⇒ there’s no v such that JαKv = 1 for all α ∈ Γ
				⇒ Γ is unsatisfiable
1
2
3
4
5

一致性意味着可满足性
如果我们能证明一致性意味着可满足性,然后我们得到完整性

Γ ̸⊢ α 	⇒ Γ ∪ {¬α} consistent
		⇒ Γ ∪ {¬α} satisfiable
		⇒ Γ ̸|= α
1
2
3

as we’ll see (and hence Γ |= α =⇒ Γ ⊢ α)

最大一致性Maximal Consistency
一个一致的集合Γ是最大一致的，如果
Γ ⊆ ∆ ⇒ Γ = ∆ for all consistent ∆
观察: 添加新公式时，最大一致集变得不一致

林登鲍姆引理Lindenbaum’s Lemma
林登鲍姆引理: 每个一致的集合都包含在一个最大一致的集合中。
证明：假设Γ一致，令α0, α1, α2, . . . 是所有公式的列表。
构造一个无限链Γ ⊆ Γ1 ⊆ · · · ⊆ Γ*

Γ0 = Γ
Γn+1 =	Γn ∪ {αn} if this set is consistent
		Γn 			otherwise
Γ∗ = U  Γn
	n∈N

1
2
3
4
5
6

最后，我们观察到 Γ*是最大的。 因为假设 ∆ 是一个一致的集合可能更大。 这意味着Γ * ⊆ Δ。 我们将证明 ∆ ⊆ Γ ∗ 必须保持为，所以这两组实际上是相等的。
选择任何 β ∈ Δ;对于公式列表中的某些 k，这必须是 αk；它必须与 Γk 一致，因为 Γk ⊆ Γ * ⊆ ∆ 和 ∆ (其中∆ 包含β) 是一致的；
so Γk+1 = Γk ∪ {αk } = Γk ∪ {β};
but β ∈ Γk+1 ⊆ Γ *

所以 ∆ 中的每个 β 也在 Γ * 中，并且 ∆ ⊆ Γ * 如所声称的那样

最大一致性Maximal Consistency
最大一致集包含足够的数据让我们构建估值满足他们
我们还需要两个事实才能证明这一点

事实：如果 Γ 最大一致，则 Γ ⊢ α ⇔ α ∈ Γ
证明：假设Γ是最大一致的
如果 α ̸∈ Γ，则 Γ ∪ {α} 不一致（因为它大于 Γ）
这意味着 Γ, α ⊢ ⊥
这意味着 Γ ⊢ α → ⊥
这与 Γ ⊢ ¬α 相同，
因此 Γ ̸⊢ α （因为 Γ 是一致的）。
相反的方向是微不足道的：可以得出任何假设

事实：如果 Γ 最大一致，那么对于所有 α，β：

¬α ∈ Γ ⇔ α ∈/ Γ
α ∧ β ∈ Γ ⇔ α ∈ Γ and β ∈ Γ
α ∨ β ∈ Γ ⇔ α ∈ Γ or β ∈ Γ
α → β ∈ Γ ⇔ α ∈ Γ implies β ∈ Γ

1
2
3
4
5

一致性意味着可满足性
宣称: 每组一致的公式都是可满足的。
证明：假设 Γ 是一致的，让 Γ∗ 是一个最大一致集，包含Γ。 对于每个命题变量 p 定义

v(p) =	1 if p ∈ Γ∗
		0 otherwis
for all p ∈ P		
1
2
3

那么 α ∈ Γ∗ ⇒ [α]v = 1。
证明是通过结构归纳。

完整性Completeness
从我们所看到的情况来看：
小完备性定理:一组公式是一致的当且仅当它是可满足的
命题逻辑的完备性定理
if Γ ⊆ Φ and α ∈ Φ, then Γ |= α ⇒ Γ ⊢ α

Proof:
Γ ̸⊢ α 	⇒ Γ ∪ {¬α} consistent
		⇒ Γ ∪ {¬α} satisfiable
		⇔ there is v such that JαKv = 0, and JβKv = 1 for all β ∈ Γ
		⇔ Γ ̸|= α

1
2
3
4
5
6

Prop 的健全性和完整性
我们已经看到 Prop 是合理的。
所以：Γ ⊢ α ⇔ Γ |= α

关于 Prop 的一些最终事实
紧致定理The compactness theorem:
当且仅当 Γ 的每个有限子集都可满足时，集合 Γ 是可满足的。
证明：
如果 Γ 是可满足的，那么每个子集也是可满足的
反过来，

Γ unsatisfiable ⇒ Γ inconsistent
				⇒ Γ0 ⊢ ⊥ for some finite Γ0 ⊆ Γ
				⇒ some finite Γ0 ⊆ Γ is inconsistent
				⇒ some finite Γ0 ⊆ Γ is unsatisfiable
1
2
3
4

建模示例
许多计算系统可以使用命题逻辑建模,鉴于其有限的表现力，这可能会令人惊讶
许多现实世界的例子太复杂，无法在这里讨论.所以我们看一些人为的例子,其他可以在讲义中找到

Sudoku
数独基于 9 × 9 网格，分为九个不相交的 3 × 3 区域，具有一些细胞的初始标记
每个剩余的单元格 (i, j) 需要用 [1, 9] 中的整数标记，使得每一行、每一列和每一区域都只包含每个标签一次