Con-E.8 — Formalism Is Rhetorical, Not Rigorous

Severity: E (Moderate) | Sphere: Se1 | Target: All Group VI (th5–th11)

The Group VI theorems (th5–th11) deploy mathematical notation (\(\forall\), \(\exists\), \(\Box\), \(\Diamond\), \(\leq\)) to present arguments that are, at their core, informal philosophical reasoning. The predicates Stable, Extensible, LifeFriendly, and Lasting are undefined primitives — unlike the mereological \(\leq\) (which has CEM semantics) or the modal operators (which have S5 semantics), these predicates have no formal truth conditions. The “formal statements” are natural-language claims dressed in mathematical notation, not statements in a formal system with deterministic truth conditions.

th5–th11’s proofs use English-language reasoning about these informal predicates, not formal derivations that could be mechanically checked. Contrast with th1–th4, which use only the mereological and modal apparatus and are genuinely formal: th1’s proof is a valid derivation in S5.

Steel-man: When Gödel’s ontological argument was genuinely formalized in Isabelle/HOL (Benzmüller and Woltzenlogel Paleo 2014), previously unnoticed consequences emerged (modal collapse). This demonstrates that informal “formal-looking” proofs and genuine machine-checkable proofs are qualitatively different. Lakatos (1976) showed that even within mathematics, proofs that seem rigorous contain hidden informal steps — and the gap between seeming-formal and genuinely-formal is widest when predicates are left undefined.

(Source: C8 from OOv1 Critique Round 1.)