Abstract:
I will prove that the decision problem for finite mathematical statements, though recursive, is infeasible in seemingly any realistic model of computation. To this end, I will construct a set of finite mathematical statements which can only be feasibly solved by programs long enough to explicitly encode a decision for each statement.
This result was published in 1973, by Michael Makkai. In this talk I will show (1) his original proof and its connection to the Gödel incompleteness theorem and (2) a needed strengthening of his 1973 result.
As time permits, I will also highlight connections to computational complexity and to algorithmic information theory (Kolmogorov complexity).