Constructing basic math from minimal foundations. This can be done from Minimal logic, Intuitionistic Type Theory (ITT) / Martin-Löf Type Theory (MLTT), or Com

Constructing basic math from minimal foundations. This can be done from Minimal logic, Intuitionistic Type Theory (ITT) / Martin-Löf Type Theory (MLTT), or Combinatorial Logic. For reason that I'll detail later, I wanted to go with an intuitionistic logic rather than classical logic. An interesting question, is what is the minimal axiom that you need to start with. I wa building at the same time both the multiverse and the logic on which it is built, so I have to be aware of information-symbolic resonance between physical stuff and the laws themselves. The Very First Axiom? So, what's the absolute "first" one? It depends on the framework: ITT/MLTT: The most plausible candidate for a single "first" axiom is the existence of the empty type (⊥). This establishes the notion of a type without requiring any prior concepts. All other types and rules are built from the ability to have types, and the empty type is the simplest possible type. Alternatively, you could say the "first axiom" is the concept of a judgment of the form a : A, which asserts that something is a type, or that something has a type. Combinatory Logic: The concept of application is the fundamental starting point. The axioms are the definitions of the combinators (S, K, and optionally I). Minimal/Intuitionistic Logic (more traditionally presented): Here, it's often presented in a sequent calculus or natural deduction system. The "first" rules are usually things like: Identity (or Axiom): A ⊢ A (A proves A) - this is about the very notion of provability. Weakening: If you can prove something from a set of assumptions, you can still prove it with more assumptions. Assumption: You are allowed to assume a proposition.