Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs

2018/12/14 by Powell, Thomas
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1812.05851

Abstract

The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem - the epsilon calculus, modified realizability and the dialectica interpretation - and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.

Related

• Logic in Mathematics and Computer Science
• The Sources of Certainty in Computation and Formal Systems
• Sequential algorithms and the computational content of classical proofs
• Programs as the Language of Science
• μλεδ-Calculus: A Self Optimizing Language that Seems to Exhibit Paradoxical Transfinite Cognitive Capabilities