自然推理系统证明：$(\neg x)P(x)⊢(\exists x)\neg P(x)$

题目很简短，但还是花了一些时间。

思考过程

先采用右$\exists$策略，即证$\neg (\forall x)P(x)⊢\neg P(x)$,差点以为可以用$\forall -$规则直接证出，但是前面有个$\neg$

在此基础上用右$\neg$策略，$\neg (\forall x)P(x),P(x)⊢\perp$好像也不行

于是又双被迫直接用右A策略:

$\neg (\forall x)P(x),\neg (\exists x)\neg P(x)⊢\perp$

尝试推出$(\forall x)P(x)$（这道题没让用导出规则，否则是显然的）

注意到左边都是约束变元，只需推出$P(x)$

但是到这卡住了，看不出来

过了一会才想起来再用一次右A策略:$\neg (\forall x)P(x),\neg (\exists x)\neg P(x),\neg P(x)⊢\perp$

这次就显然了，矛盾选$(\exists x)\neg P(x)$ ，再一路倒推回去就行

策略总结

右$\neg$策略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