| _version_ | 1866901943434084352 |
|---|---|
| author | Salhab, Najih |
| author_facet | Salhab, Najih |
| contents | <p> </p> <blockquote> <p><strong>This work identifies a formation-level vulnerability that directly concerns safety-critical systems.<br>The implications are not abstract: human lives are at stake.<br>For this reason, the results warrant full and serious technical scrutiny.<br>Any critique should therefore be precise, technical, and scientific in nature.</strong></p> </blockquote> <p>We establish a <strong>necessity result</strong> identifying a <strong>formation-level vulnerability</strong> underlying classical self-referential paradoxes. The source of the pathology is shown to be an <strong>implicit type confusion</strong> that permits unguarded lifting from syntactic entities to propositions, thereby admitting <strong>evaluation-dependent constructions</strong> into the space of truth-bearers.</p> <p>We prove that, under <strong>minimal classical formation assumptions</strong>—namely:<br>(1) strict separation between entities and propositions,<br>(2) restriction of truth-valuation to propositions only, and<br>(3) the requirement of <strong>explicit, inhabited formation witnesses</strong> for all admissible lifts—<br>such evaluation-dependent constructions <strong>fail to form propositions at all</strong>. Consequently, logical leakage across formation levels is <strong>prevented prior to semantic evaluation</strong>, rather than being contained post hoc through stratification, partial semantics, or meta-theoretic restrictions.</p> <p>The result is <strong>necessity-based and independent of truth-theoretic choices</strong>. It does not revise semantics, weaken classical logic, or impose ad hoc semantic constraints. Instead, it identifies a <strong>formation-prior admissibility boundary</strong> that determines which expressions are eligible to become truth-bearers in the first place. Classical paradoxes are thereby diagnosed as downstream artifacts of formation failure, not as primitive semantic anomalies.</p> <p>The criterion is <strong>mechanically validated</strong> using two independent formal realizations:<br>an SMT-based encoding in <strong>Z3</strong>, which eliminates all countermodels while preserving non-trivial well-formed propositions; and a type-theoretic implementation in <strong>Cubical Agda</strong>, where evaluation-dependent constructions fail at the formation (type-checking) stage prior to any notion of truth or falsity.</p> <p>The result constitutes a <strong>formation-prior, necessity-level invariant</strong>, formally derived and mechanically verified, which rules out an entire <strong>structural class of ill-formed propositions independently of semantics</strong>, while remaining conservative with respect to all evaluator-independent and legitimately formed propositions.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18216160 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | A Necessary Formation-Theoretic Invariant Against Illegitimate Propositional Lifting 3 Salhab, Najih formation theory, type theory, self-reference, logical paradoxes, AI safety, formal verification, pre-semantic validation, safety-critical systems, software reliability, smart contract security, proof assistants, soundness, system failure prevention, formal methods <p> </p> <blockquote> <p><strong>This work identifies a formation-level vulnerability that directly concerns safety-critical systems.<br>The implications are not abstract: human lives are at stake.<br>For this reason, the results warrant full and serious technical scrutiny.<br>Any critique should therefore be precise, technical, and scientific in nature.</strong></p> </blockquote> <p>We establish a <strong>necessity result</strong> identifying a <strong>formation-level vulnerability</strong> underlying classical self-referential paradoxes. The source of the pathology is shown to be an <strong>implicit type confusion</strong> that permits unguarded lifting from syntactic entities to propositions, thereby admitting <strong>evaluation-dependent constructions</strong> into the space of truth-bearers.</p> <p>We prove that, under <strong>minimal classical formation assumptions</strong>—namely:<br>(1) strict separation between entities and propositions,<br>(2) restriction of truth-valuation to propositions only, and<br>(3) the requirement of <strong>explicit, inhabited formation witnesses</strong> for all admissible lifts—<br>such evaluation-dependent constructions <strong>fail to form propositions at all</strong>. Consequently, logical leakage across formation levels is <strong>prevented prior to semantic evaluation</strong>, rather than being contained post hoc through stratification, partial semantics, or meta-theoretic restrictions.</p> <p>The result is <strong>necessity-based and independent of truth-theoretic choices</strong>. It does not revise semantics, weaken classical logic, or impose ad hoc semantic constraints. Instead, it identifies a <strong>formation-prior admissibility boundary</strong> that determines which expressions are eligible to become truth-bearers in the first place. Classical paradoxes are thereby diagnosed as downstream artifacts of formation failure, not as primitive semantic anomalies.</p> <p>The criterion is <strong>mechanically validated</strong> using two independent formal realizations:<br>an SMT-based encoding in <strong>Z3</strong>, which eliminates all countermodels while preserving non-trivial well-formed propositions; and a type-theoretic implementation in <strong>Cubical Agda</strong>, where evaluation-dependent constructions fail at the formation (type-checking) stage prior to any notion of truth or falsity.</p> <p>The result constitutes a <strong>formation-prior, necessity-level invariant</strong>, formally derived and mechanically verified, which rules out an entire <strong>structural class of ill-formed propositions independently of semantics</strong>, while remaining conservative with respect to all evaluator-independent and legitimately formed propositions.</p> |
| title | A Necessary Formation-Theoretic Invariant Against Illegitimate Propositional Lifting 3 |
| topic | formation theory, type theory, self-reference, logical paradoxes, AI safety, formal verification, pre-semantic validation, safety-critical systems, software reliability, smart contract security, proof assistants, soundness, system failure prevention, formal methods |
| url | https://doi.org/10.5281/zenodo.18216160 |