Show HN: A verified foundation of mathematics in Coq (Theory of Systems)
1 points
1 hour ago
| 0 comments
| HN
I’ve spent the last few months formalizing a new structural foundation for mathematics called Theory of Systems (ToS) in Coq.

The goal was to derive classical results (like the uncountability of [0, 1]) from a single principle of distinction ("A = exists") rather than starting with ZFC axioms.

Key Technical Highlights:

135 theorems, 0 Admitted for the main uncountability proof.

Solves Digit Stability: Instead of digit extraction, it uses geometric interval trisection to prove uncountability constructively.

L5-Resolution: Implements a deterministic "leftmost" rule for argmax, ensuring that optimization processes are Cauchy even on flat plateaus.

No Axiom of Infinity: The infinite emerges as a property of the process levels (P4).

I'm currently looking for an ArXiv endorsement (cs.LO or math.LO) to publish the full 60-page preprint.

Repo: https://github.com/Horsocrates/theory-of-systems-coq

I'd love to hear your thoughts on the E/R/R (Elements/Roles/Rules) framework and the inclusion of the "Law of Order" as a 5th law of logic.

No one has commented on this post.