When are two proofs essentially the same? (2007)

Sum(i=1..n, i)

= Sum(i=1..n/2, i) + Sum(i=1..n/2, n+1-i)

= Sum(i=1..n/2, n+1)

I'm still interested in the general question, of whether some proofs have big gaps between them. The more complex the proofs, the more obvious this would be; my examples are unfortunately simple. Something like proving the fundamental theorem of algebra using Rouche's Theorem (complex analysis) vs. field theory. But I don't know enough math to compare those.

It is usually both, but I meant time, because to be able to address your stack frame you need* a stack pointer that can take as many distinct values as your nesting depth, so it must have o(log n) width.

It is easy to dismiss this as irrelevant because your integers are usually fixed-width, but then you'd need to parameterize your algorithm on the size of input you're willing to handle (at which point you're no longer doing asymptotic analysis), since arbitrary-precision arithmetic really does just work this way normally.

> Also, regarding "without tail calls", your example already has tail calls. What do you mean by that?

I mean "without tail call optimization", or if you're particularly keen on getting into a pedant-off, "with the function call in the tail position not implemented as a tail call".

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

You say: "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."

OK, so let's say we have an agreement, that your representation for the type of natural numbers is practically - from a typing viewpoint - identical to my representation for the type of natural numbers. So then we don't have to worry about the encoding. And it makes sense to do this for all the primitive types we are using.

But then consider your proposition "for all x:X, there exists y:Y, such that P(x,y)". This proposition is itself a type, which is constructed from primitive types. So why would you here, all of sudden, want to distinguish between different proofs, or rather, representations of this particular type?

I think, if we both accept proposition-as-types paradigm, then I am reasoning backwards from it. If the structure of two different proofs of the same (propositional) type matters (whatever the reason), not just existence of these proofs, why shouldn't it matter with the primitive types? It implies that we need to come to an agreement what primitive types we are using, because their structure might matter, too.

And that's why I said - you effectively want your "universal proof equivalence" to be the beta-equivalence of underlying lambda terms, because lambda calculus is a mechanism how we construct the complex types from primitive ones (not all constructions are valid though, there are typing constraints). But, as I already explained, it doesn't really give you a grounding, because there are multiple ways to define primitives in lambda calculus which cause the terms not to be beta-equivalent. So you have to care about having such agreement how you implement these primitives. Hopefully this clears up where it comes from.

But having that agreement in itself then limits what you can prove (in particular, you cannot prove equivalence of different representations, since you're already taking it as an axiom), so you don't really want to have such an agreement. That's why I believe the only sensible way out is to propagate the proof indifference "upwards" - even for complicated types (practically usable propositions), the actual representation shouldn't matter.

No worries, though. If you want the representation to matter, you would do the same thing you do in lambda calculus - you choose some encoding of lambda terms, and take an interpreter for this encoding which implements beta-reduction. When interpreting an encoded lambda term, you can discern different implementations (for example, their complexity properties) of otherwise beta-equivalent lambda terms. Mathematically, this gives a different theory. (Also note there is no reason for your encoding to be working with just lambda abstraction and application as primitives, you can encode different lambda terms in different ways, if you need to. That's what combinatory logic does, it lets you use an arbitrary basis of primitives.)