# Beyond Computation 2. 0: Verified Meta-Trilemma This paper presents the second iteration of the Charta Research Program on mechanized anti-computationalism. ## Relation to Version 1. 0 Version 1. 0 Publication, December 2025 introduced a broad-spectrum axiomatic framework (A1-A4, modal depth limitations, emergent subject-functor S), establishing the philosophical foundations and demonstrating the performative irrefutability (T5) of the anti-computationalist position. ## Version 2. 0 radically extends 1. 0 through • **Minimal axiomatization: ** A2ₙorm (normative existence) + A4ₗimit (computational limitation) • **T1ComputationalLimit: ** Direct proof of computational impossibility (constructive, Coq 8. 19 verified) • **DavisSafe: ** Closes the Martin Davis consistency loophole • **Meta-logical Identity Lock: ** Formal preservation of absolute identity under realization • **Ur-Matrix framework: ** Primordial source structure of normative identity → DOI: 10. 5281/zenodo. 18056466 (https: //doi. org/10. 5281/zenodo. 18056466) • **Exhaustive trilemma: ** - **Accept A2ₙorm + A4ₗimit** → Computationalism impossible (⊥) - **Deny A2ₙorm** → Eliminativism (no normative subjects) - **Deny A4ₗimit** → Mechanism (universal provability) • **Verified Coq supplements: ** Complete source code for all theorems included as supplementary files (LucasPenroseOmniprover. v, T1WeakOmniprover. v, T1StrongOmniprover. v, WeakStrongOmniprover. v). Run `coqc` on any file to verify the proofs yourself. ## Key advancement 2. 0 achieves a sharper, more destructive result with strictly weaker assumptions than 1. 0 – reducing the anti-computationalist argument to its logical essence: two axioms, one Coq-verified theorem, three exhaustive paths. **Keywords: ** computationalism, consciousness, Coq, formal verification, Gödel, meta-trilemma, philosophy of mind, verified proofs
Siegfried Meister (Mon,) studied this question.