TLDR;
- We are within a context of weak logic, proof theory, a destructive world where uncertainty and limitation are the norm. Cf. Russel, Gödel, Kleene, Putnam and Quine et al.
- The text is deliberately written in parataxis. It offers a critique of the foundations underlying modern computer science, arguing that it inadvertently enshrined classical logic where constructive logic would have been the more appropriate foundation.
- Alignment is usually posed as a classical claim (“for every situation there is some good action”), but what is actually demanded is a uniformizer (“there exists a single policy that, given any situation, outputs a good action, with evidence.”) is exactly where oracles, hidden choices, semantics, and erased proof-structure sneaks in, putting alignment right in the neighborhood of canonical uniformization problems.
- One good step would be better proof theoretic hygiene.
1.
A derivation is a structured object, a consequence is a shadow of that object. Arithmetic, in standard algebraic settings, cancels structure. It has inverses on intended domains. Logic, in general, does not.
Analogy. The premise “wet street” underdetermines its cause. In arithmetic (where inverses exist), operations can cancel: Analogy. If a bus has -5 passengers then +5 restores it to an empty bus. Implication is not, in general, reversible; many algebraic operations are reversible on their intended domains.
Take “logic” as the consequence operation: , or a sequent .
Either way, internal interfaces are erased, the map is many-to-one: different proofs yield the same sequent, different premise geometries yield the same conclusion. Distinguishability drops. Example. Cut elimination removes that mediator. Derivability is preserved, intensional structure is not. Normalization behaves like deforestation. Lemmas inline, names vanish, proofs can shrink in interface; or explode in size. We see: Structure-forgetting under a quotient is an entropic process in a technical sense, loss of intensional data under extensional collapse. To know what to forget is to know how to think.
We push this further: (i) treat proofs as programs, (ii) treat connectives by their introduction rules, (iii) treat existence as obligation not as opinion.
We end up with Kleene realizability or the Brouwer-Heyting-Kolmogorow-Interpretation (BHK) for proof-relevant semantics, nothing new is needed. Existence becomes: “produce a realizer.” Implication becomes “done.” Disjunction becomes: “think.” We undermine the epistemic stance that treats Kripke frames (cf. Kripke semantics) as a satisfactory foundation for constructive or computational reasoning at object level. Logical consequence then reads as reachability not possibility. A preorder arises as the reflection of a richer category of proofs. The order is a shadow of the object, there is only computation.
2.
No single figure “invented” the computer: Babbage, Leibniz, Zuse, Turing, von Neumann, Mauchly, Moore School engineering, ENIAC, diffuseness is not merely historical; it is conceptual. “Computer” names: (i) a model, (ii) a practice, (iii) a semantics of programs.
These are not the same thing. A missed separation sits underneath. Rather, keep two domains distinct: (i) Classical reasoning for global specification; non-effective existence; disjunction without choice; meta-theory, philosophy. (ii) Constructive reasoning for operational content; witnesses; compilation; certificates; resource and termination data.
Remark. The intention is methodological: constructive discipline aligns with what can be transported into code, certificates, resource bounds, and termination arguments; classical reasoning remains indispensable for specification, exploration, and play: The problem is not classical logic is wrong, but classical commitments become invisible when used as if they carried computational content.
Our computer realizes finite-state encodings of transitive objects, together with conventions that mediate between ideal semantics and implementable approximations. A similar inversion occurs at the ISA level. Hardware forces that an instruction yields a next machine state in finite time, not a mathematical totality of function on ideals. Confusing these levels yields the appearance of classical total functions where there are only finite conventions. Note that former can simulate the latter, but with uncertainty.
A familiar fracture:
format(Decimal.from_float(0.1), '.17')
# Output: 0.10000000000000001Explanation. The discrepancy is not a malfunction but empirical and logical evidence that the machine operates on representations under specified error bounds, not on abstract reals under equality.
Problem. Numbers do not change with the base; expansions do. In base 2, behaves like in base 10: an eventually periodic description fails because the expansion is infinite. Naming the value as repairs representation, but then one must say what “the continuum” is, and what it means to compute over it.
Computation over arbitrary reals presupposes effective convergence data: not merely that a sequence converges, but how fast, or under what modulus. There is no uniform method that, given an arbitrary real presentation, returns a step bound for achieving a desired tolerance. This is the operational face of undecidability: not all semantic predicates are extractable as procedures.
The constructive lesson is sharper: computation over reals is computation over names of reals—Cauchy Data, Interval Data, effective Dedekind Cuts. One must specify convergence behavior: a modulus, or an admissible refinement discipline. Without such data, basic predicates are not uniformly decidable The operational obstruction is uniformity and extraction: the gap between “there exists” and “here is the method.” With the fixed point is in the distance and at 0, with it's everywhere if left unchecked. Partial mathematics is almost always totalized by definition: define inverse by case split; return a default at zero; prove the field law under a side condition . This seemingly keeps terms well-typed and evaluation total. Often pragmatic; but dangerous: It's not true. Note. You might notice that division is harder mentally.
Problem. Statements that look like theorems about partial mathematics become theorems about an engineered total operator. One can risks to silently slide between “the intended partial operation” and “the chosen totalization,” unless definedness and adequacy is tracked as data. The result is many-to-many unsoundness. Nobody knows what they are talking about because nobody knows that nobody knows. The risk is drift: theorems become theorems about the engineered totalization, not the intended partial operation, not the original specification. Drift is silent when definedness is not tracked as data, when certificates are pushed into lemmas, when surface syntax stays classical.
You would think cryptography and other fields suggests the right form: attach evidence to claims. Keys, group elements, and transcripts can come with certificates, proofs, or checkable invariants. Properties are carried by witnesses, not assumed as global predicates.
Problem. Enter complexity theory, strong and classically flavored: (i) quantifies over all inputs, (ii) quantifies over worst cases, (iii) quantifies asymptotically, (iv) shifts unboundedness into the metalanguage. Nothing a computer could ever provide.
The profound irony: (i) Church worked in a Platonist idiom (cf. Frege-Church Ontology), yet untyped -reduction is more rigorous then Heyting Arithmetic: only what normalizes is realized. (ii) Turing began from an operational picture (cf. Imitation Game), yet the model idealizes unbounded tape and time, reifies machines, can leave its finite state machine unexamined, inviting classical readings of total mappings on infinite domains. (iii) Kleene formalized the Church–Turing Thesis, that bridges from “effective procedure” to “formal computation.”
Problem. Its plausibility comes from convergence: many models agree extensionally up to coding—untyped -definability, partial recursive functions, Turing machines, register machines, RE languages. But extensional agreement hides intensional placement of structure: Diophantines vs Diophantine systems, Field extensions vs. rewrites. In untyped -calculus, control is syntax; the evaluator is fixed; partiality is non-normalization. In Turing machines, control is a finite transition table, data is tape, partiality is divergence, and most importantly: There is underspecification, this injects impredicativity.
3.
Many so called hard problems share the -shaped form:
Translation. Assume is decidable, or at least effectively checkable. For fixed , verifying a proposed can be local and mechanical. There is a demand for the realization, moving from conjecture to proof:
Problem. This is not a trivial strengthening, it asks for a selector, an algorithm. But in constructive logic:
Problem. To pass left-to-right one needs additional principles: choice, realizer extraction, oracles, filters, semantics, infinities as explicit constructions inside the proof. This is the constructive boundary. (i) You can't know what you can't know. (ii) deciding whether such a uniform witness exists is itself -shaped, as a canonical set is totality of programs:
Translation. Here means: “program halts on input within steps.” Decidable in (), hardness sits in the quantifier pattern. Note that this problem is readable by a Turing Machine, but is not utterable in -calculus. Exactly at that boundary where the hard problems lie, the Church–Turing Thesis shows its limits.
Logic. If one had a uniform classifier for which -specifications admit uniform realizers, one collapses standard undecidability barriers. One builds an oracle by definition.
Problem. We cannot prove this.
In this sense “entropy reversal” reappears: is a family of local successes, is a uniform realizer is a global compressor reconstructing missing interface—an inversion of a many-to-one projection. Constructive logic refuses the inversion unless the interface is supplied. Mathematics can't see the problem, if it could, it would have solved it already.
4.
Cast AI alignment in the same grammar. Let be states, actions, and mean: “action satisfies the value criterion in state .” State:
Conjecture. For every situation, some correct response must exists. The Alignment Problem proper asks for the uniform answer:
A single policy correct in all states. This is again is leap. When is arbitrary and is open-ended, the demand begins to resemble an oracle request.
The usual next step is to bound the problem: restrict , restrict , impose regularity conditions, but this introduces a second-order obligation. One must justify that the bounds themselves capture the intended notion of “alignment.” The specification problem thereby reappears at the meta-level, and in full generality it admits no uniform closure. Consequently, one should not expect a general proof that alignment is impossible (nor, symmetrically, a general proof that it is achievable) without substantial structural assumptions. This exposes a central divide between classical and intuitionistic reasoning. Call it empiricism vs. rationalism, the problem of induction, or the Law of the Excluded Middle (LEM), the truth is:
is itself such a statement.
Constructive logic blocks this inference per suspension of judgment unless one construct such an , i.e., a uniform choice of witnesses together with proofs of for all . Absent such data the left-hand side alone does not determine a uniform selector.
Classical logic can validate the step only under stronger principles—most notably choice (to select witnesses uniformly) or compactness together with classical reasoning (often formulated as LEM). In this sense, blanket uniformization principles are tightly entangled with classical principles: assuming enough uniform selection power tends to recover classically valid moves that constructive logic does not accept.
Remark. A witness-extractable (algorithmic) resolution of a major conjecture that effectively has the mentioned hierarchy—e.g. a uniform separation statement in complexity theory—would not merely settle a mathematical claim; it would shift the boundary between extensional existence and constructive content by demonstrating unexpected uniform realizers in a domain typically treated classically. The results in 2507.07696 and 1502.04135 suggest analogous phenomena for other Millennium problems as well. Interestingly, proving that an algorithmic solution is correct reintroduces the problem.
Remark. Much of this historical asymmetry traces back to Hilbert’s campaign against Brouwer in the early 1920s, which effectively marginalized intuitionism within foundational mathematics. As a result, the constructive insights that might have integrated naturally into mainstream logic were displaced and later reintroduced indirectly—first through recursive function theory and then through type theory. In that sense, type theory can be viewed as the rehabilitated, systematized continuation of the intuitionistic program that Hilbert’s formalism had once suppressed.
5.
A better reformulation of computation makes its accompanying information explicit: error bounds, stability conditions, termination measures, and proofs of definedness. Arithmetic should return not only values but also guarantees. Reals should appear via effective names, interval enclosures, Cauchy data with moduli, or comparable representations. Equality should be replaced where necessary by apartness or bounded equivalence.
Classical reasoning remains essential for specification, creative, probabilistic and global reasoning about systems. Constructive reasoning governs the operational core: what must be compiled, executed, certified, and transported across machine boundaries without importing non-effective commitments.
Today, common pedagogy and engineering surface syntax often treats programs and numeric operations as if they were classical total mathematics, while the operational substrate is finite and witness-driven. The proposal is not to abolish classical logic, but to mark the boundary. classical principles belong in specification and meta-theory; constructive data and witnesses belong in execution-facing semantics.
Consequence. Intuitionism and Platonism are often treated as opinions rather than as methodologies. Foundations are constructive at the point of execution, yet frequently expressed in classical dress that obscures where the witnesses live. The remedy is not invention but reapplication: make evidence first-class where computation demands it; allow classical reasoning where it functions as possibility, comparison, and external description.
Example. Meta-complexity (cf. Article) is complexity reappearing one level up: the cost of reasoning about cost of reasoning about the cost. If we insist that resource claims come with checkable certificates, e.g., a bound together with a proof that a program runs within , then the meta-claim becomes an object-level verification task with its own complexity. Conversely, without such certificates, deciding global resource properties (e.g. “this program runs in polynomial time on all inputs”) becomes a -shaped, generally non-decidable problem. In either case, the lesson is the same: resource assertions either travel as constructive data, or they migrate into an intractable meta-level.
Final Analogy. Constructive logic is a high-resolution source file; classical logic is a lossy compression format. You can apply the filter locally, but if you save the whole project in the compressed format, the witness- and proof-structure is gone. Both have their role to play, but you should compress only once.
To be continued.