• Calendar

July 16, Wednesday
12:00 – 13:30

I will present two results due to Hartmanis and Hopcroft.

Let F be any formal system for proving theorems. We assume that F is axiomatizable, that F is consistent, and that F is of sufficient power to prove basic theorems of set theory.

Theorem 1: For every F we can effectively construct an i such that $\phi_i$ is recursive and $P^{\phi_i}=NP^{\phi_i}$ can neither be proved nor disproved in F.

Theorem 2: There exist an algorithm which can be explicitly given whose running time is $n^2$ but there is no proof in F that it runs in time $<2^n$