There's another approach, from Boyer and Moore. Boyer and Moore built up mathematics from constructs at the Peano axiom level (zero, add1, etc.) plus recursive functions that must terminate. It's constructive mathematics; there are no quantifiers, no ∀ or ∃. [1] They built an automatic theorem prover in the 1970s and 1980s that works on this theory. (I recently made it work on Gnu Common LISP and put it on Github, so people can run it again.)[2]
In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here's a definition of ORDERED for a list of number:
If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the "wrong" type is not useful. This provides the benefits of types without requiring a theory of types. It's a very clean way to look at the foundations of mathematics. It's simpler than Russell and Whitehead.
When you prove things using definitions like this, there's a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable.
(It's fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.)
In Boyer-Moore theory, all functions are total - you can apply any function to any object. Types are predicates. Here's a definition of ORDERED for a list of number:
If L is not a list, it is considered to be ordered. This makes it a total function, runnable on any input, even though the result for the "wrong" type is not useful. This provides the benefits of types without requiring a theory of types. It's a very clean way to look at the foundations of mathematics. It's simpler than Russell and Whitehead.When you prove things using definitions like this, there's a lot of case analysis. This gets worse combinatorially; a theorem with four variables with type constraints will generate at least 2⁴ cases, only one of which is interesting. Most of the cases, such as when L is not a list, are trivial, but have to be analyzed. Computers are great at this, and the Boyer-Moore prover deals with those cases without any trouble. But it went against a long tradition in mathematics of avoiding case analysis. That made this approach unpopular with the generation of pre-computer mathematicians. Today, it would be more acceptable.
(It's fun to run the Boyer-Moore prover today. In the 1980s, it took 45 minutes to grind through the basic theory of numbers. Now it takes a few seconds.)
[1] https://www.amazon.com/Computational-Logic-Robert-S-Boyer/dp... [2] https://github.com/John-Nagle/nqthm