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	|- ( ph <-> -. A. x ph )
Assertion	quantgodel	|- F.

Proof

Step	Hyp	Ref	Expression
1		quantgodel.s	|- ( ph <-> -. A. x ph )
2		sp	|- ( A. x ph -> ph )
3	2 1	sylib	|- ( A. x ph -> -. A. x ph )
4	3	pm2.01i	|- -. A. x ph
5	4 1	mpbir	|- ph
6	5	ax-gen	|- A. x ph
7	6 4	pm2.24ii	|- F.