The Unnegatable Loop: Tetralemma's Performative Geometry (with Coq-Verification)
Siegfried Meister · PhilPapers (PhilPapers Foundation) · 2025
This paper is part 2 of a Triptychon. Complete paper + Coq verification of structural dependencies (Appendix B). Key result: the_unnegatable_loop : Qed. Tarski's undefinability manifests performatively via Coq's type system.