5 ms·

No, a proof is not a value of the proposition you are proving. That is a very convoluted way of thinking about proofs, and just because you can (using some type

No, a proof is not a value of the proposition you are proving. That is a very convoluted way of thinking about proofs, and just because you can (using some type theory based logic), doesn't mean you should. It is like saying that 2 is the same as {∅, {∅}}, which is true in some set-theoretic formulations of the natural numbers, but which is not how we usually think about 2.

milesrout 2y ago
That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often bolded or double struck as U+1D7DA) used to mean "the set with two elements" and those elements are often called 0 and 1.
- auggierose 2y ago
  It is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} If you don't like the meaning of equality here, that is exactly my point. My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually. And the same is true for the "Curry-Howard" way of understanding proofs.
ndriscoll 2y ago
I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out to prove. If you want to prove to me that `A => B`, what other way is there to do so besides giving me logical steps to get from `A` to `B`? If you had a proof-of-A, would that not then be a function that takes your proof-of-A and returns a proof-of-B?
- immibis 2y ago
  Nobody else is seeing how it is not convoluted. A proof is already logical steps to get from proposition A to proposition B. What you're requesting is that it should be replaced with logical steps to get from a value of type A to a value of type B, where types A and B aren't ordinary object-class types suck as "pencil" or "employee" or "goblin", nor ordinary data-structure types such as "pair(int, list(string))", but (in most cases) some completely abstract labels that you made up in order for this mapping to work. You have a cool demonstration of disjunction elimination, which of course is no simpler than actual disjunction elimination, but how will you prove something non-constructive like "x mod 2 = 0 → not (x mod 4 = 1)" in your system, and how will it not be more complicated than proving it without your system? You mentioned passing in axioms as extra assumptions, like the law of the excluded middle. In programming terms, the law of the excluded middle is a magical function that, for every type T, returns an Either<T,Not<T>> - Not<T> being one of those made up types that only exist to make the correspondence work and don't actually mean anything. If you're working with Not you presumably also want a function that takes any Not<Not<T>> and returns a T. In programming terms this is completely unimplementable and meaningless so I'm not really sure why you think it would be useful. It seems like you might be suffering from fuckarounditis: https://news.ycombinator.com/item?id=43466252 https://news.ycombinator.com/item?id=43466252
  - ndriscoll 2y ago
    They are values though! That's my whole point! These languages are constructed and written about in a way that often obscures that. A lot of them are simple things like tuple(x: int, y: int, h: x<y). Here's a constructive proof of your proposition: import Mathlib.Data.Nat.ModEq example (h: x ≡ 0 [MOD 2]): ¬(x≡1[MOD4]) := λ xeq1mod4 ↦ by have h24 : 2 ∣ 4 := ⟨2,by tauto⟩ have h' := (h.congr (xeq1mod4.of_dvd h24)).mp (by rfl) contradiction You can see at one point, I make a proof that 2|4, which is a data structure that needs to remember that 2 is the solution to 2*n=4 as the proof. Then I pass that to a couple functions (lemmas) that require that assumption, and get an Iff, which is a pair of implications (lambda functions) going each direction. I pull out one of them and call it on a trivial proof of `x=x`. This all gives me a proof that 0=1 mod 2. Finally I can ask it to expand that definition until it reaches a contradiction. The whole thing is a proof that if you give me a proof that x=0 mod2 and x=1 mod4, I can build you a contradiction. Exactly like you'd expect in a proofs class. Since I'm a programmer, I wrote the whole thing as a big lambda function. Note that Not[T] is also not some arcane thing. It's just Function[T,Void]. Essentially, it's a function you could never possibly call (because the whole point is that you can't get a T to call it), but if you did, it would just crash the program/throw an exception. It has an obvious purpose if you're trying to formally prove a negative. The use of a reader monad to get a constructive-ish proof of things that need AC or LEM is just what programmers might call dependency injection. It's a normal pattern (in programming). It only "doesn't mean" something if you don't believe in those axioms at all, but even then many proofs don't need the full axiom and will work if you can bring your own choice function (e.g. you already have a basis for your vector space). Just like many (most?) real world programs basically don't need a turing machine, and actually work fine as a DFA with a trivial event loop or something. Fwiw, you can easily construct a ¬¬T from a t: T: `λ f↦f(t)` (so make a closure that remembers your t:T and passes it into any ¬T someone gives it). LEM essentially says all ¬¬T are of this form, so you can extract the T that's hidden inside. Sort of like how functionals in finite dimensions are all secretly hiding a vector to do a dot product.

milesrout 2y ago

That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often bolded or double struck as U+1D7DA) used to mean "the set with two elements" and those elements are often called 0 and 1.

auggierose 2y ago
It is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} If you don't like the meaning of equality here, that is exactly my point. My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually. And the same is true for the "Curry-Howard" way of understanding proofs.

ndriscoll 2y ago

I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out to prove. If you want to prove to me that `A => B`, what other way is there to do so besides giving me logical steps to get from `A` to `B`? If you had a proof-of-A, would that not then be a function that takes your proof-of-A and returns a proof-of-B?

immibis 2y ago
Nobody else is seeing how it is not convoluted. A proof is already logical steps to get from proposition A to proposition B. What you're requesting is that it should be replaced with logical steps to get from a value of type A to a value of type B, where types A and B aren't ordinary object-class types suck as "pencil" or "employee" or "goblin", nor ordinary data-structure types such as "pair(int, list(string))", but (in most cases) some completely abstract labels that you made up in order for this mapping to work. You have a cool demonstration of disjunction elimination, which of course is no simpler than actual disjunction elimination, but how will you prove something non-constructive like "x mod 2 = 0 → not (x mod 4 = 1)" in your system, and how will it not be more complicated than proving it without your system? You mentioned passing in axioms as extra assumptions, like the law of the excluded middle. In programming terms, the law of the excluded middle is a magical function that, for every type T, returns an Either<T,Not<T>> - Not<T> being one of those made up types that only exist to make the correspondence work and don't actually mean anything. If you're working with Not you presumably also want a function that takes any Not<Not<T>> and returns a T. In programming terms this is completely unimplementable and meaningless so I'm not really sure why you think it would be useful. It seems like you might be suffering from fuckarounditis: https://news.ycombinator.com/item?id=43466252 https://news.ycombinator.com/item?id=43466252
- ndriscoll 2y ago
  They are values though! That's my whole point! These languages are constructed and written about in a way that often obscures that. A lot of them are simple things like tuple(x: int, y: int, h: x<y). Here's a constructive proof of your proposition: import Mathlib.Data.Nat.ModEq example (h: x ≡ 0 [MOD 2]): ¬(x≡1[MOD4]) := λ xeq1mod4 ↦ by have h24 : 2 ∣ 4 := ⟨2,by tauto⟩ have h' := (h.congr (xeq1mod4.of_dvd h24)).mp (by rfl) contradiction You can see at one point, I make a proof that 2|4, which is a data structure that needs to remember that 2 is the solution to 2*n=4 as the proof. Then I pass that to a couple functions (lemmas) that require that assumption, and get an Iff, which is a pair of implications (lambda functions) going each direction. I pull out one of them and call it on a trivial proof of `x=x`. This all gives me a proof that 0=1 mod 2. Finally I can ask it to expand that definition until it reaches a contradiction. The whole thing is a proof that if you give me a proof that x=0 mod2 and x=1 mod4, I can build you a contradiction. Exactly like you'd expect in a proofs class. Since I'm a programmer, I wrote the whole thing as a big lambda function. Note that Not[T] is also not some arcane thing. It's just Function[T,Void]. Essentially, it's a function you could never possibly call (because the whole point is that you can't get a T to call it), but if you did, it would just crash the program/throw an exception. It has an obvious purpose if you're trying to formally prove a negative. The use of a reader monad to get a constructive-ish proof of things that need AC or LEM is just what programmers might call dependency injection. It's a normal pattern (in programming). It only "doesn't mean" something if you don't believe in those axioms at all, but even then many proofs don't need the full axiom and will work if you can bring your own choice function (e.g. you already have a basis for your vector space). Just like many (most?) real world programs basically don't need a turing machine, and actually work fine as a DFA with a trivial event loop or something. Fwiw, you can easily construct a ¬¬T from a t: T: `λ f↦f(t)` (so make a closure that remembers your t:T and passes it into any ¬T someone gives it). LEM essentially says all ¬¬T are of this form, so you can extract the T that's hidden inside. Sort of like how functionals in finite dimensions are all secretly hiding a vector to do a dot product.