自然推理系统证明: ( ¬ x ) P ( x ) ⊢ ( ∃ x ) ¬ P ( x ) (\lnot x)P(x)\vdash (\exists x)\lnot P(x) (¬x)P(x)⊢(∃x)¬P(x)
题目很简短,但还是花了一些时间。
思考过程
先采用右 ∃ \exists ∃策略,即证 ¬ ( ∀ x ) P ( x ) ⊢ ¬ P ( x ) \lnot(\forall x)P(x)\vdash \lnot P(x) ¬(∀x)P(x)⊢¬P(x),差点以为可以用 ∀ − \forall- ∀−规则直接证出,但是前面有个 ¬ \lnot ¬
在此基础上用右 ¬ \lnot ¬策略, ¬ ( ∀ x ) P ( x ) , P ( x ) ⊢ ⊥ \lnot(\forall x)P(x),P(x)\vdash \bot ¬(∀x)P(x),P(x)⊢⊥好像也不行
于是又双被迫直接用右A策略:
¬ ( ∀ x ) P ( x ) , ¬ ( ∃ x ) ¬ P ( x ) ⊢ ⊥ \lnot(\forall x)P(x),\lnot(\exists x)\lnot P(x)\vdash \bot ¬(∀x)P(x),¬(∃x)¬P(x)⊢⊥
尝试推出 ( ∀ x ) P ( x ) (\forall x)P(x) (∀x)P(x)(这道题没让用导出规则,否则是显然的)
注意到左边都是约束变元,只需推出 P ( x ) P(x) P(x)
但是到这卡住了,看不出来
过了一会才想起来再用一次右A策略: ¬ ( ∀ x ) P ( x ) , ¬ ( ∃ x ) ¬ P ( x ) , ¬ P ( x ) ⊢ ⊥ \lnot(\forall x)P(x),\lnot(\exists x)\lnot P(x),\lnot P(x)\vdash \bot ¬(∀x)P(x),¬(∃x)¬P(x),¬P(x)⊢⊥
这次就显然了,矛盾选 ( ∃ x ) ¬ P ( x ) (\exists x)\lnot P(x) (∃x)¬P(x) ,再一路倒推回去就行
策略总结
右 ¬ \lnot ¬策略yyds,一次不行就两次
具体过程
1. ¬(∀ x)P(x),¬(∃ x)(¬P(x)) |- ¬(∀ x)P(x) ∈
2. ¬(∀ x)P(x),¬(∃ x)(¬P(x)),¬P(x) |- ¬P(x) ∈
3. ¬(∀ x)P(x),¬(∃ x)(¬P(x)),¬P(x) |- (∃ x)(¬P(x)) ∃+ 2 (x/x)
4. ¬(∀ x)P(x),¬(∃ x)(¬P(x)),¬P(x) |- ¬(∃ x)(¬P(x)) ∈
5. ¬(∀ x)P(x),¬(∃ x)(¬P(x)) |- ¬(¬P(x)) ¬+ 3,4
6. ¬(∀ x)P(x),¬(∃ x)(¬P(x)) |- P(x) ¬¬- 5
7. ¬(∀ x)P(x),¬(∃ x)(¬P(x)) |- (∀ x)P(x) ∀+ 6
8. ¬(∀ x)P(x),¬(∃ x)(¬P(x)) |- ¬(∀ x)P(x) ∈
9. ¬(∀ x)P(x) |- ¬(¬(∃ x)(¬P(x))) ¬+ 7,8
10. ¬(∀ x)P(x) |- (∃ x)(¬P(x)) ¬¬- 9