Beyond Computation: A Formalized Meta-Trilemma Mechanized Philosophical Argument

This paper presents a formalized meta-trilemma for computationalism in higher-order type theory, with full mechanization in Coq. The axioms are philosophically motivated, drawing from Gödel-Penrose arguments, semantic underdetermination, and normative foundations; the verification demonstrates internal consistency and derivability. The framework models the intuition that no finite computational system can capture the full depth of mental phenomena, particularly self-referential insight and normative judgment. Alternative formulations and their implications are discussed.