Theorem quantgodel

Description: There can be no formula asserting its own non-universality, in parallel to bj-babygodel ; proof path is shorter but relying on a property of specialization which provability predicates do not have. For a matching proof, see quantgodelALT . (Contributed by Ender Ting, 9-May-2026)

	Ref	Expression
Hypothesis	quantgodel.s	$$⊢\phi \leftrightarrow \neg \forall x\phi$$
Assertion	quantgodel	$$⊢\perp$$

Proof

Step	Hyp	Ref	Expression
1		quantgodel.s	$$⊢\phi \leftrightarrow \neg \forall x\phi$$
2		sp	$$⊢\forall x\phi \to \phi$$
3	2 1	sylib	$$⊢\forall x\phi \to \neg \forall x\phi$$
4	3	pm2.01i	$$⊢\neg \forall x\phi$$
5	4 1	mpbir	$$⊢\phi$$
6	5	ax-gen	$$⊢\forall x\phi$$
7	6 4	pm2.24ii	$$⊢\perp$$