2 ms·

The law of excluded middle always seemed like BS to me from the moment it was taught. It's wonderful that by removing it, proofs become "harder" to make, but co

The law of excluded middle always seemed like BS to me from the moment it was taught. It's wonderful that by removing it, proofs become "harder" to make, but consequently constructive and thus more rigoris. Too many people believe in the law of excluded middle, especially in their own lives, much to the folly of civilization itself.

constantcrying 3y ago
It directly leads to the continuum being inseperable. If you believe that "now" is real, you believe in LEM.
- Der_Einzige 3y ago
  Well, I'm an eternalist who remembers the basics of the Relativity of simultaneity, so I reject that "now is real" as such.
  - constantcrying 3y ago
    Do you believe that any thing can be seperated into two part, which, if put together exactly the same as before become the initial part?
ndriscoll 3y ago
Even if you "believe" in LEM, I think it could be helpful to conceptualize proofs that use it as instead being proofs in the "Reader monad" over LEM. So instead of proving `A => B`, you prove `A => Reader[LEM, B] = A => (LEM => B)`. If you really examine the proof you're doing, probably you don't need LEM in its full power, but actually some specific `Not[Not[X]] => X` (or a handful of specific instances like that). The neat thing about this is that in principle it could be tracked in a proof assistant with type inference. The ZIO framework for Scala has a super slick system for dependencies where e.g. an `RIO[Foo,A]` (an IO that requires a Foo and returns an A) and `A => RIO[Bar,B]` can compose to form an RIO[Foo&Bar, B] with the types inferred. So you could in principle have a proof system that lets you infer types like `A => Reader[LEM[Foo] & LEM[Bar], B]` (where LEM[T] = Not[Not[T]] => T), i.e. you get explicit types that show all of the instances of an LEM function you need to make your proof constructive, and since you're thinking of things as living in the Reader monad, you have the ergonomics of a proof that just assumes LEM. Same idea could be used with AC or any other "controversial" axiom. So you don't need to "believe" them to use them, and if you do "believe" them, you can benefit from pretending you don't.

constantcrying 3y ago

It directly leads to the continuum being inseperable. If you believe that "now" is real, you believe in LEM.

Der_Einzige 3y ago
Well, I'm an eternalist who remembers the basics of the Relativity of simultaneity, so I reject that "now is real" as such.
- constantcrying 3y ago
  Do you believe that any thing can be seperated into two part, which, if put together exactly the same as before become the initial part?

ndriscoll 3y ago

Even if you "believe" in LEM, I think it could be helpful to conceptualize proofs that use it as instead being proofs in the "Reader monad" over LEM. So instead of proving `A => B`, you prove `A => Reader[LEM, B] = A => (LEM => B)`. If you really examine the proof you're doing, probably you don't need LEM in its full power, but actually some specific `Not[Not[X]] => X` (or a handful of specific instances like that). The neat thing about this is that in principle it could be tracked in a proof assistant with type inference. The ZIO framework for Scala has a super slick system for dependencies where e.g. an `RIO[Foo,A]` (an IO that requires a Foo and returns an A) and `A => RIO[Bar,B]` can compose to form an RIO[Foo&Bar, B] with the types inferred. So you could in principle have a proof system that lets you infer types like `A => Reader[LEM[Foo] & LEM[Bar], B]` (where LEM[T] = Not[Not[T]] => T), i.e. you get explicit types that show all of the instances of an LEM function you need to make your proof constructive, and since you're thinking of things as living in the Reader monad, you have the ergonomics of a proof that just assumes LEM. Same idea could be used with AC or any other "controversial" axiom. So you don't need to "believe" them to use them, and if you do "believe" them, you can benefit from pretending you don't.