3 ms·

To be more specific, propositions that can be written in the form "some member of X exists" can be proven by specifying such a member. Thanks to the ability to

To be more specific, propositions that can be written in the form "some member of X exists" can be proven by specifying such a member. Thanks to the ability to define dummy sets with 0 or 1 element, while keeping them separate with types, this is quite a lot of propositions - surprisingly many. But it's not a useful programming or proving technique.

ndriscoll 2y ago
What propositions cannot be written this way? If your answer is along the lines of "things that use the axiom of choice" or "things that use LEM", then you can instead prove `AC -> P` or `LEM -> P`, which are constructible (assuming no similar missing "magic" axioms, but those can be solved with the same technique). Then we can again look at programming where we have the Reader monad as a way to pretend `AC -> P` is just `P` and use it as if it were (but with the ability to pull `AC` out of a hat when needed). Arguably then, we can only prove `AC -> P` and not `P` itself because `P` is not true (obviously that's a controversial take). I don't know what strategies they're using, but mathlib in Lean has formalizations for measure theory for example: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Measure/MeasureSpace.lean https://github.com/leanprover-community/mathlib4/blob/master... For very practical programming work (like business software), I'd be surprised if there were any useful programs that can't be boiled down to `while True: f(x)` where f(x) is some finite terminating program that you can prove stuff about. When you do a bunch of work in a language/ecosystem like Scala's, you get used to the idea that if your function says it returns an A, then it returns an A; there's generally no failure modes to consider if they're not in the type (ignoring realities like a datacenter catching on fire that are outside of the programming model). Passing a B to a `Function[B,A]` is an actual proof that you now have an `A` in your hand.

ndriscoll 2y ago

What propositions cannot be written this way? If your answer is along the lines of "things that use the axiom of choice" or "things that use LEM", then you can instead prove `AC -> P` or `LEM -> P`, which are constructible (assuming no similar missing "magic" axioms, but those can be solved with the same technique). Then we can again look at programming where we have the Reader monad as a way to pretend `AC -> P` is just `P` and use it as if it were (but with the ability to pull `AC` out of a hat when needed). Arguably then, we can only prove `AC -> P` and not `P` itself because `P` is not true (obviously that's a controversial take). I don't know what strategies they're using, but mathlib in Lean has formalizations for measure theory for example: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Measure/MeasureSpace.lean https://github.com/leanprover-community/mathlib4/blob/master... For very practical programming work (like business software), I'd be surprised if there were any useful programs that can't be boiled down to `while True: f(x)` where f(x) is some finite terminating program that you can prove stuff about. When you do a bunch of work in a language/ecosystem like Scala's, you get used to the idea that if your function says it returns an A, then it returns an A; there's generally no failure modes to consider if they're not in the type (ignoring realities like a datacenter catching on fire that are outside of the programming model). Passing a B to a `Function[B,A]` is an actual proof that you now have an `A` in your hand.