0
点赞
收藏
分享

微信扫一扫

自然推理系统证明:¬(∀x)P(x)⊢(∃x)¬P(x)

sunflower821 2022-04-17 阅读 51
抽象代数

自然推理系统证明: ( ¬ 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
举报

相关推荐

0 条评论