A non-expert view on Turing machines, Proof Verifiers, and Mental reasoning

TL;DR

This paper explains the connections between Turing machines, proof verifiers, and the process of reasoning about program termination, emphasizing the role of Turing progressions and ordinal numbers from a non-expert perspective.

Contribution

It provides an accessible overview of complex concepts like Turing progressions and their relation to proof verification and program termination for non-experts.

Findings

Termination verification involves a hierarchy of axiomatic theories.

Turing progressions are connected to ordinal numbers.

The paper offers an accessible explanation of complex logical ideas.

Abstract

The paper explores known results related to the problem of identifying if a given program terminates on all inputs -- this is a simple generalization of the halting problem. We will see how this problem is related and the notion of proof verifiers. We also see how verifying if a program is terminating involves reasoning through a tower of axiomatic theories -- such a tower of theories is known as Turing progressions and was first studied by Alan Turing in the 1930's. We will see that this process has a natural connection to ordinal numbers. The paper is presented from the perspective of a non-expert in the field of logic and proof theory.