5 ms·

A proof is not a statement that something is true, but a demonstration that it is true. Are you familiar with the proofs-as-programs idea? The uh, something i

by drdeca 2y ago

A proof is not a statement that something is true, but a demonstration that it is true. Are you familiar with the proofs-as-programs idea? The uh, something isomorphism? Idr the name. Not all programs that implement a function are the same. When you boil things down to the fundamental steps of the logic you are working on, you needn’t get the same thing. For one thing, it may be that axioms A and B suffice to prove Z, and that axioms B and C suffice to prove Z, but that B alone doesn’t, and that A and B doesn’t prove C and that B and C doesn’t prove A. So, the proofs using A and the proofs using C are certainly different.

js8 2y ago
I think "propositions-as-types" is exactly why we should consider proofs to be the same if they prove the same type. As others have already said, if you want to distinguish between different proofs, it's better to encode those distinctions formally into types (and thus potentially into another mathematical theory).
- drdeca 2y ago
  There are multiple values of type integer? I don’t see why we should truncate the types representing propositions so that they have at most one element each.
  - js8 2y ago
    We shouldn't, that's the point! At least not in mathematics, programming is a different story. It's perfectly fine to have type of all integers alongside type of all squares and types that only contain number 1 or number 1729. Relations of these types will then reflect the relations of their respective proofs. There is no need to consider "proof equivalence" or other kind of proof properties. That's already accomplished by studying types themselves. The choice of types already reflects what we want to study.
    - drdeca 2y ago
      I would think that asking if two proofs are equivalent would be analogous to “do these two expressions of type integer evaluate to the same value?” ?
      - js8 2y ago
        Hm. Take for example formalization in Calculus of Constructions (Coq, Lean). What you propose is essentially beta-equivalence of the underlying lambda calculus terms. However, this is not without problems (undecidability aside). Different CoC formalizations can use, for example, different LC representations of natural numbers (Church numerals, binary..) or other basic types, such as pairs. Does that mean that proof using Church numerals and proof using binary numerals are different? Intuitively, I don't think so, yet they are according to above definition. Another example. One can embed classical propositional logic into intuitionistic one using translation of LC terms (basically continuation-passing style transform). Is the translated proof the same or different? It operates on different terms and is thus different as a program. I think the fundamental problem is the idea that there is some universal and absolute equivalence relation between proofs. Rejecting that leads to accepting equivalence relative to the type of the proposition. (I think you can get some absoluteness back using univalence axiom, but I don't comprehend that.)
        drdeca 2y ago
        It isn’t clear to me why the encoding of the natural numbers would come up. I would have thought that some statement about the natural numbers would involve some type, considered as the type of natural numbers, which I suppose if you construct it from other simpler primitives would have some kind of encoding, But, if the proof uses only uses the terms of that type through the use of the constructors etc. associated with that type, you wouldn’t have multiple proofs which differ only by the encoding, and belonging to the same type (proposition), as the encoding would just be whatever encoding is used for the type of integers used. It seems likely that I’ve misunderstood what you meant. Still, if you have two different natural numbers objects, there’s an isomorphism between them… I guess one could use this to translate between proofs for one and proofs for the other, but I don’t know if translating and then translating back would yield the original proof. I wouldn’t be surprised if by default it doesn’t. It wouldn’t surprise me if there is a way to “make it the same” while still keeping other proofs distinct, though. I suppose one could make some sort of quotient type? Also, for (intuitionistic) existential statements, the proof can almost be seen as just the thing claimed to exist along with a witness that it is that thing. So, if you say, “for all x:X, there exists y:Y, such that P(x,y)” , then two proofs might differ by giving two different functions x:X->(y:Y,p:P(x,y)) which, could be regarded as different if the X->Y part is different without considering whether the p part is different. Maybe if one e.g. required equality types to be sub-singletons (i.e. if p,q : Eq(Nat,x,y) then p is q ) but allowed other propositions to have multiple distinct elements, that could be, something? You might know more about this than me.

by drdeca 2y ago

js8 2y ago

I think "propositions-as-types" is exactly why we should consider proofs to be the same if they prove the same type. As others have already said, if you want to distinguish between different proofs, it's better to encode those distinctions formally into types (and thus potentially into another mathematical theory).

drdeca 2y ago
There are multiple values of type integer? I don’t see why we should truncate the types representing propositions so that they have at most one element each.
- js8 2y ago
  We shouldn't, that's the point! At least not in mathematics, programming is a different story. It's perfectly fine to have type of all integers alongside type of all squares and types that only contain number 1 or number 1729. Relations of these types will then reflect the relations of their respective proofs. There is no need to consider "proof equivalence" or other kind of proof properties. That's already accomplished by studying types themselves. The choice of types already reflects what we want to study.
  - drdeca 2y ago
    I would think that asking if two proofs are equivalent would be analogous to “do these two expressions of type integer evaluate to the same value?” ?
    - js8 2y ago
      Hm. Take for example formalization in Calculus of Constructions (Coq, Lean). What you propose is essentially beta-equivalence of the underlying lambda calculus terms. However, this is not without problems (undecidability aside). Different CoC formalizations can use, for example, different LC representations of natural numbers (Church numerals, binary..) or other basic types, such as pairs. Does that mean that proof using Church numerals and proof using binary numerals are different? Intuitively, I don't think so, yet they are according to above definition. Another example. One can embed classical propositional logic into intuitionistic one using translation of LC terms (basically continuation-passing style transform). Is the translated proof the same or different? It operates on different terms and is thus different as a program. I think the fundamental problem is the idea that there is some universal and absolute equivalence relation between proofs. Rejecting that leads to accepting equivalence relative to the type of the proposition. (I think you can get some absoluteness back using univalence axiom, but I don't comprehend that.)
      - drdeca 2y ago
        It isn’t clear to me why the encoding of the natural numbers would come up. I would have thought that some statement about the natural numbers would involve some type, considered as the type of natural numbers, which I suppose if you construct it from other simpler primitives would have some kind of encoding, But, if the proof uses only uses the terms of that type through the use of the constructors etc. associated with that type, you wouldn’t have multiple proofs which differ only by the encoding, and belonging to the same type (proposition), as the encoding would just be whatever encoding is used for the type of integers used. It seems likely that I’ve misunderstood what you meant. Still, if you have two different natural numbers objects, there’s an isomorphism between them… I guess one could use this to translate between proofs for one and proofs for the other, but I don’t know if translating and then translating back would yield the original proof. I wouldn’t be surprised if by default it doesn’t. It wouldn’t surprise me if there is a way to “make it the same” while still keeping other proofs distinct, though. I suppose one could make some sort of quotient type? Also, for (intuitionistic) existential statements, the proof can almost be seen as just the thing claimed to exist along with a witness that it is that thing. So, if you say, “for all x:X, there exists y:Y, such that P(x,y)” , then two proofs might differ by giving two different functions x:X->(y:Y,p:P(x,y)) which, could be regarded as different if the X->Y part is different without considering whether the p part is different. Maybe if one e.g. required equality types to be sub-singletons (i.e. if p,q : Eq(Nat,x,y) then p is q ) but allowed other propositions to have multiple distinct elements, that could be, something? You might know more about this than me.