Where Do Qualia Enter the Model? A Coq-Verified Analysis of the Non-Derivability of Phenomenology from Functional Structure

Abstract

Claims about phenomenal consciousness frequently move from functional, representational, self-referential, informational, or behavioral properties of a system to the conclusion that the system must possess qualia or phenomenal experience. This paper asks a more elementary question: where, formally, does phenomenology enter the model?We provide a mechanically checked analysis in the Coq proof assistant. The formal development constructs explicit countermodels showing that self-modeling, self-reference, functional self-awareness, reportability, privacy, and intransferability do not by themselves entail phenomenal properties. More strongly, two models can be functionally identical while being assigned incompatible phenomenal predicates.The resulting conclusion is deliberately narrower than a metaphysical elimination of consciousness. The formal results establish a non-derivability claim: the cited functional properties are insufficient to determine phenomenology unless an additional bridge principle is introduced. If such a bridge principle is simply stipulated, then the phenomenal conclusion has been added to the theory rather than derived from its functional premises.This exposes a recurring methodological problem. A purported explanation of phe- nomenology cannot merely rename an unexplained phenomenal predicate or insert it as an additional axiom and then present the resulting connection as a consequence of functional organization. The burden is instead to specify what additional formal structure distinguishes a phenomenal state from a functionally identical non-phenomenal state.The argument leaves open the possibility that such a bridge exists. What it rejects is the claim that the bridge is supplied automatically by self-reference, self-modeling, reportability, privacy, intransferability, or functional equivalence.