Identity Types
bartoszmilewski.com
bartoszmilewski.com
{ s: S, P s },
That sounds like the way to go. No (identity) types needed.
You can’t start with one definition and then throw in another.
Does two equal two? What if the first one is written in a larger font?
Exactly. Obviously they're different, but they're equivalent for most purposes. In traditional mathematics you have to handle this in a very awkward way: you have to say there's some kind of platonic ideal of two, and then writing two in one font or another forms a model of this platonic ideal of two. Then you can work with the platonic ideal of two, and add two and two and get four - but you've already forgotten which font you're in. Whereas if you say that twos in one font are equivalent to twos in another font or to some canonical platonic ideal of two, you can lift the fact that two plus two is equal to four back along those equivalences and get a four in the right font. (Or, more commonly, you just ignore that detail and say that you've got something equivalent to four - but you haven't erased the details, they're always there if you need them).
That is not even wrong. You are mixing up syntax and semantics, and that is because type theorists don't have a concept of semantics.
Right back at you. I don't have to treat notation as something different from semantics, because I'm working in a theory that can handle both elegantly and consistently. Conventional mathematics struggles to describe mathematics as it is actually performed - working mathematicians rely extensively on "abuse of notation", but set-theoretic metamathematics pretends this is out of scope or safe to ignore.
What a load of malarkey. This statement is not a problem for traditional mathematics. I have 2 green apples and 2 red apples right here in my bag (eh, set), and the size of the set is 4, and all elements of the set are apples, some of them are red, some are green. What is the problem? I can tell you: type theory.
Well, is your set equal to a set of 3 green apples and 1 red apple, or not? (And actually how can you have multiple green apples in the same set if they're equal?)
Well, a green apple had better be equal to itself. So if you've got a green apple and another green apple that isn't equal to the first, you're already in trouble and going to have to resort to hacks like numbering them.
> No, the set is not equal to a set of 3 green apples and 1 red apple, under the assumption that a green apple cannot be a red apple (and vice versa).
What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
Nope, no trouble at all. Those troubles only exist in your type-infested mind.
> What if you want to manipulate it in a context where you only care about the number of apples, not their colour?
Then I'll do just that. Lol, you can't make this shit up.
I would suggest, like I do in another post in this thread, that the problem just disappears if one adds proof irrelevance as an axiom.
You get what you pay for.
> The thing is that if one wants to make set theory practical, one probably ends up implementing something close to type theory anyway.
That is wrong. Unless you want to argue that types are pretty close to sets already. Let's just throw away what makes types different from sets, and I am happy with that.
Your point is that axioms are scary, and I agree with that. When you use them, you should be aware where they come from, and why they are consistent with each other. In type theory, everything is definitions from the bottom up, but that also restricts your freedom in what you can do. But you can view these definitions just as one source of axioms that you trust, because you trust the type theory. But I argue that it would be just as safe to have two or three or ... sources of axioms, as long as you can argue why you trust the combination of these sources (in fact, every type theory implementation has multiple such sources inside, they just don't advertise that). Ideally that argument is machine-checked, which leads the way to trusted extensions of the prover without sacrificing flexibility.
I kind of like your idea of having trusted extensions to provers. I was myself thinking along the lines of taking the foundation that I got in my Calculus of Constructions project and see if it can be put on a smaller set theory foundation. I.e., prove it in ZFC, presumably with inaccessible cardinals added.
Yes, the type universe hierarchy is the canary in the coal mine that something is wrong with type theory as a foundation, but very few take it seriously. Some do though, see for example the first chapter of http://abstractionlogic.com .
Of course, in some contexts when one has those types, it may be better to forget any distinction between different ways a witness to an equality can be produced, leaving identity types with at most one element.
Just because the LEM is true doesn’t mean intuitionistic reasoning that avoids the use of the LEM isn’t sometimes useful.
Also the concept of a proof of equality strikes as relevant, because some equalities are actually incomputable. E.g. suppose you want a an equality type for whether two functions are equivalent (two instances of the same function type).
Admittedly the above (except program extraction I suppose) can all be achieved with ZFC + a layer of type theory on top, and again that's a reasonable thing to do, but I hope this makes a strong enough case for the type theoretical foundation.
But if you want an easy life, instead of trying to do what is right, why did you do math in the first place?
Of course that is a benefit in the "meta" level, but it is not like ZFC is a better foundation than topoi/types/etc..
I mean I don't know what you mean by right, but given how type theory/ZFC/categorical foundations there is no clear winner (unless you can make a good argument for set theory as our foundation, because again, the average mathematician seldomly thinks in ZFC), I'd say type theory is quite nice in its computational interpretations so let's go with that.
I also don't want to go there, but obviously research drains manpower and money. If we can get CS people to write PAs we really should do that. They're filthy rich in the grand scheme of research.
idgi. If you do your 101 logic class often you learn natural deduction, and how do you formalize natural deduction in a computer system? (Hint: type theory is "natural" for this).
Also how proofs work is far from simple.