3 ms·

This “apple” thing…is it colored or not? You can’t start with one definition and then throw in another. Does two equal two? What if the first one is written i

This “apple” thing…is it colored or not? 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?

lmm 1y ago
> 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).
- auggierose 1y ago
  > Obviously they're different, but they're equivalent for most purposes 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.
  - lmm 1y ago
    > 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.
    - auggierose 1y ago
      If you say that semantics and syntax are the same, then you don't have semantics. That is not elegant, just confused, and your statements in this thread here are a great example of that.
auggierose 1y ago
Does two equal Two? Sometimes it does, sometimes it doesn't. That would depend on your definitions and axioms. I can definitely work with something without knowing all about it. It is called axiomatic reasoning. Some people seem to have a hard time with it.

This “apple” thing…is it colored or not? 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?

lmm 1y ago

> 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).

auggierose 1y ago
> Obviously they're different, but they're equivalent for most purposes 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.
- lmm 1y ago
  > 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.
  - auggierose 1y ago
    If you say that semantics and syntax are the same, then you don't have semantics. That is not elegant, just confused, and your statements in this thread here are a great example of that.

auggierose 1y ago

Does two equal Two? Sometimes it does, sometimes it doesn't. That would depend on your definitions and axioms. I can definitely work with something without knowing all about it. It is called axiomatic reasoning. Some people seem to have a hard time with it.