PhD position in proof theory at the University of Bath

[Joe Shipman]

I don’t think the notion of algorithms “being the same” that was intended was “calculates the same function”. It is clear that one can have essentially different algorithms calculating the same function, where the proof that they calculate the same function may be much more complicated than the algorithms themselves.

Whether two proofs are “the same“ maybe a bit harder to address satisfactorily, because the inter-translatability of different formalisms for algorithms is better developed than for proofs. However, reverse mathematics provides one way to address this. Conway and I suggested another in our paper “Extreme Proofs”, in which we distinguished between seven different proofs of the irrationality of the square root of 2 by a “scope test”: each proof had a different domain of generalizability (which other irrational numbers the proof could be applied to).

— JS

Sent from my iPhone

> On Mar 3, 2020, at 7:02 PM, Annatala Wolf <a.lupine at gmail.com> wrote:
> 
> 
>> On Tue, Mar 3, 2020 at 12:30 PM Alessio Guglielmi <web.alessio.guglielmi at gmail.com> wrote:
> 
>> 
>> Suffice to say that we are currently unable to decide whether two given proofs or two given algorithms are the same; this is an old problem that dates back to Hilbert.
> 
> Just a picky note which is probably obvious (and perhaps the above was intended as a joke), this problem is not just "currently" inaccessible to us. The general problem is NRNC (both it and its complement are undecidable), which is easy to show: assume a program exists that tells you if two algorithms are the same, then pass it 1) an algorithm that outputs true iff some undecidable process terminates (there must be some algorithm for which this is true even if we don't know which), and 2) an algorithm that always outputs true. This contradicts the undecidability of an undecidable algorithm, which means the assumption must be false. The same idea works for the complement.
> 
> -- 
> /* Annatala Wolf, Lecturer
>  * Department of Computer Science and Engineering
>  * The Ohio State University
>  */
> enum E{A;System s;String t="/* Annatala Wolf, Lecturer%n * Department of Computer Science and Engineering%n * The Ohio State University%n */%nenum E{A;System s;String t=%c%s%1$c;{s.out.printf(t,34,t);s.exit(0);}}";{s.out.printf(t,34,t);s.exit(0);}}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200303/acb61e8f/attachment-0001.html>