Abstract

This paper investigates the formalizability of St. Anselm’s ontological argument for the existence of God within the constructive framework of Martin-Löf’s Intuitionis- tic Type Theory (ITT). The argument, traditionally assessed through classical and modal logics, posits God as "that than which nothing greater can be conceived" (id quo maius cogitari nequit). We demonstrate that the argument is not merely in- valid but fundamentally un-formalizable in ITT. This failure is traced to three points of profound incompatibility. First, the argument’s reductio ad absurdum structure proves at best the proposition ¬¬∃x.G(x), which is not constructively equivalent to ∃x.G(x), thereby failing to provide a witness for God’s existence. Second, the cru- cial Anselmian distinction between existence in intellectu and in re is re-interpreted under the propositions-as-types paradigm, where ’conceivability’ corresponds to the definition of a well-formed type and ’actuality’ corresponds to its inhabitation by a constructed term. ITT rigorously separates these two concepts; to define a type is distinct from constructing a term (i.e., proving it is inhabited), and the latter cannot be deduced from the former’s definition. Third, and most decisively, the argument relies on an impredicative definition. It requires quantification over a totality of "all conceivable beings"a type Bto define its maximal element G, which must itself be a member of B. Such a self-referential totality is ill-formed in ITT, whose stratified universe hierarchy is designed precisely to preclude the paradoxes arising from such impredicativity. This analysis concludes that ITT acts as a diagnostic tool, revealing the ontological argument’s deep-seated reliance on non-constructive principles, a Pla- tonic assumption of a completed totality of concepts, and a treatment of existence as a predicateall of which are inadmissible from a constructive standpoint.