Set theory with types
lawrencecpaulson.github.io
lawrencecpaulson.github.io
Of course I don't believe that set theory is the One True Foundation and everything else is a lie, the fact that one can give a foundation with just one type of object, just one binary relation and relatively few simple axioms (or axiom schemas) is quite relaxing and I would say a bit unappreciated.
And also unlike other fellow students I never encountered any problem with more seemingly complicated constructions like tensor products or free groups since one can easily see how they are coded in set theory if one is familiar with it as a foundation.
You don't need to choose a concrete implementation. If you don't want to choose a construction, you can just say something like "let (N, 0, +, *) be a structure satisfying the peano axioms" and work from there.
> For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly.
Why is that problematic? The constructions are isomorphic under the sentences that actually matter. This kind of statement is usually called a "junk theorem", and they are a thing in type theory too, see for example this quote from a faq by Kevin Buzzard about why Lean defines division by zero to be zero:
> The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.
https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
> Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized.
Is that actually true? At the very least writing out the axioms and derivation rules is easier for set theory, since it's simpler than type theory. And there has been plenty of computer-verified mathematics done in Metamath/set.mm and Isabelle/ZF, even though less has been done than in type theory. Currently the automated tools are better for type theory, but it seems likely to me that that has more to do with how much effort has been put into type theory than any major inherent advantages of it.
---
More generally, types in type theory are also constructed! The real numbers in Lean don't come from the platonic realm of forms, they are constructed as equivalence classes of cauchy sequences. And the construction involves a lot of type-theoretic machinery which I'd usually rather ignore when working with reals, much like I'd usually rather ignore the set-theoretic construction of the real numbers. And the great thing is that I can ignore them, in either foundation!
So I just don't really buy these common criticisms of set theory, which to me seem like double standards.
In what situation do you ever actually need a set theoretic foundation of the natural numbers to get work done?
Which of course means state is real.
Which mean langauge, syntax and semantics can be traced all the way down to fundementals.
Which means human meaning making is making the meaning of the universe, like an accidental organ of the universe.
And far from human meaning making being subjective its tied directly to physical existence and is objective.
And a cesium clock is all you need to derive everything fundemental.
That's what I play around with at least.
The idea that if stars are a process that emits photons and change energy gradients, humans are a process that emits complex meaning and change causal leverage gradients.
In mathematics labels are _not_ important, definitions are.
One simple example that everybody can relate to: do natural numbers include 0 or not? Who cares? Some definitions include it, some do not. There's even a convention of using N for N with 0, and N+ for excluding it, but even the convention is just a convention, not a definition. You could call them "funky numbers, the set of whole positive numbers including 0", and you're fine. Funky, natural, those are just names, labels, as long as you define them, it doesn't matter.
Same applies to set theory, there's many, many set theories, and they differ between properties, and this has never caused problems, because in mathematical discussion or literature...you provide or point to a definition. So you'll never discuss about "set theory" without providing one or pointing to one.
This is very, very different from how normal people waste their time.
E.g. arguing whether AI "thinks" or not, but never defining what thinking means, thus you can't even conclude whether you think or not, because it's never been defined.
The advantage is, then, that we can use a simple first order logic, where all objects in the logic are of the same type. This makes certain things easier and more pleasant. That the proposition `1 ∈ 2` can be written (i.e. that it is not a syntax error, though it's value is unknowable) should not bother us, just as that the English proposition "the sky is Thursday" is not a grammatical error and yet is nonsensical, doesn't bother us. It is no more or less bothersome than being able to write the proposition `1/x = 13`, with its result remaining equally "undefined" (i.e. unknowable and uninteresting) if x is 0. If `1/x = 13` isn't a syntax error, there's no reason `1 ∈ 2` must be a syntax error, either.
That a proposition is nonsensical (for all assignments of variables or for some specific ones, as in x = 0 in 1/x) need not be encoded in the grammar of the logic at all, and defining nonsense as "unknowable and uninteresting" is both convenient and elegant. I think that some logicians overlook this because they're attracted to intuitionist theories, where the notion of provability is more reified, whereas in classical theories every proposition is either true or false. They're bothered perhaps less by the ability to write 1 ∈ 2 and more by the idea that 1 ∈ 2 has a truth value. But while the notion of provability itself is not reified in classical logics, unprovable propositions are natural and common. 1 ∈ 2 has a meaning only in a very abstract sense; the theory can make that statement valid yet practically nonsensical by not offering axioms that can prove or disprove it. Things can be "undefined" in a precise way: the axioms do not allow you to come to any definition.
Indeed, this is exactly how the formal set theory in TLA+ is defined: https://pron.github.io/posts/tlaplus_part2
This actually comes in handy: While 1 ∈ 2 is undefined, `(2 > 1) ∨ (1 ∈ 2)` is true, and `(1 > 2) ∧ (1 ∈ 2)` is false, and this is useful because it means you can write:
x = 0 ∨ 1/x ≠ 0
y = 0 ∨ 1/x ≠ 0
To make this convenient, typed theories will often define 1/0 = 0 or somesuch (but they don't complain about that). In untyped set theory, 1 ∈ 2 and 1/0 can remain valid yet undefined.
Of course a ZF set theory operates with different objects than Peano arithmetic - it's a different theory. But Peano arithmetic nevertheless applies to any encoding of the integers, even the ones where 1 ∈ 2 is undefined.