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	⊢ ( 𝜑 ↔ ¬ ∀ 𝑥 𝜑 )
Assertion	quantgodel	⊢ ⊥

Proof

Step	Hyp	Ref	Expression
1		quantgodel.s	⊢ ( 𝜑 ↔ ¬ ∀ 𝑥 𝜑 )
2		sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
3	2 1	sylib	⊢ ( ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 𝜑 )
4	3	pm2.01i	⊢ ¬ ∀ 𝑥 𝜑
5	4 1	mpbir	⊢ 𝜑
6	5	ax-gen	⊢ ∀ 𝑥 𝜑
7	6 4	pm2.24ii	⊢ ⊥