PhD position in proof theory at the University of Bath

[Annatala Wolf]

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/fe62b951/attachment.html>