Beyond Computation 2.0: Verified Meta-Trilemma - Mechanized Impossibility of Normatively Complete Computational Consciousness
Zenodo (CERN European Organization for Nuclear Research) January 19, 2026 DOI: 10.5281/zenodo.18695024 (opens in new tab)
Study at a glance
AI-extracted from the abstract| Characteristics | Theoretical or philosophical paper Peer reviewed |
|---|---|
| Keywords | Impossibility Mathematical proof Identity music Argument complex analysis Reductio ad absurdum Axiomatic system Computation Key lock Consistency knowledge bases Theoretical computer science Philosophy of language Relation database Calculus dental Deontic logic Normative Semantics computer science Epistemology |
| Key points | Proposes that accepting two minimal axioms (A2_norm and A4_limit) leads to the conclusion that computationalism is impossible, with three exhaustive paths: computationalism impossible, eliminativism, or mechanism. |
Abstract
# 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_norm (normative existence) + A4_limit (computational limitation) • **T1_ComputationalLimit:** 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_norm + A4_limit** → Computationalism impossible (⊥) - **Deny A2_norm** → Eliminativism (no normative subjects) - **Deny A4_limit** → Mechanism (universal provability) • **Verified Coq supplements:** Complete source code for all theorems included as supplementary files (Lucas_Penrose_Omniprover.v, T1_Weak_Omniprover.v, T1_Strong_Omniprover.v, Weak_Strong_Omniprover.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