Could you recommend me a good introductory textbook into constructive/intuitionist math?
My impression is that you guys operate under some extra constraints, but I have been unable to figure out what exactly those constraints are. (Is there even a common standard, or does everyone use their own definition?)
okay i wrote you a reply and apparently lesswrong thinks its llm written (which is insane) bottom line is that the standard is "Constructivism in Mathematics, Vol 1 (Studies in Logic and the Foundations of Mathematics, Volume 121)" by A.S. Troelstra and D. van Dalen i also explained how assuming less are not additional constraints but naturally correspond to a harder system and gave the irrationality of root 2 as an example for typical law of the excluded middle proof.
Any natural number can be uniquely written as a sum of non-consecutive Fibonacci numbers. This is called Zeckendorf representation.
Consider,
15 = 2 + 13,
or
54 = 2 + 5 + 13 + 34.
This outlines a very weak RE language employing only {N,+,var}. We can also see that it is able to encode:
https://www.milanrosko.com/demo/zeck.html (.js demo)
Because you cannot use adjacent Fibonacci numbers in the sum, each “gap” between Fibonacci indices becomes meaningful: which indices are used encodes structure in a kind of “sparse bitvector.” In that sense: if you leave at least one gap (i.e. you do not use consecutive Fibonacci numbers), you can use the pattern of used vs unused Fibonacci indices to store information additively.
Thus, unlike binary or prime-exponent encodings the Zeckendorf representation stores data by selecting a unique subset of Fibonacci “slots,” rather than bits or prime powers.
From this we can construct a novel injective pairing function.
It has multiple advantages over known methods: it is typed and arithmetic at the same time, meaning that the structure of the Fibonacci-index bands enforces a clean separation between components while still remaining a purely additive numerical encoding. Because Zeckendorf representations never use consecutive Fibonacci numbers, we can allocate disjoint “regions’’ of indices to each element of the pair, guaranteeing that no carries occur and that decoding is mechanically bounded. This yields a pairing function that is reversible without multiplication, exponentiation, or factorization; preserves type distinctions at the level of index geometry; and remains compatible with very weak arithmetic theories that nonetheless require robust Gödel-style encodings.
For purposes of constructive logic, this is advantageous because the encoding avoids reliance on ontological commitments such as the Fundamental Theorem of Arithmetic (FTA), which guarantees unique prime factorization only through a classical, non-constructive global property of the integers. The Carryless Pairing works instead by local, finitely verifiable constraints: one checks only the absence of adjacent Fibonacci indices and the disjoint placement of index bands. All decoding steps are constructive, bounded, and justified by the combinatorial behavior of the Fibonacci sequence rather than by an external uniqueness ontology. This keeps the encoding aligned with intuitionistic standards, grounding arithmetic representation in directly inspectable structure rather than in classical inductive principles.
Classical constructions in arithmetic encoding, including those used in weak theories, almost always depended on prime factorization with superpolynomial reversal, total bijective Cantor-style polynomial pairings, or digit interleaving in fixed bases; additive, gap-controlled encodings based on Fibonacci structure are not part of the standard toolkit.
I posted this because first-order algorithms within such an RE system can, in principle, admit refinements in someone’s project X, where even small advances in encoding structure may yield correspondingly more efficient constructive methods.
Originally it was conceived to get rid of primality based Gödel Numbering so that we obtain a bona fide constructive method grounded entirely in additive structure. The paper: https://arxiv.org/abs/2509.10382