Author: Stefano Berardi
Title: Continuations, Backtracking and Limits: A Notion of Construction for Classical Logic
Abstract:
We give an overview of a research line started in cooperation with
Prof. Hayashi Proof Animation group. Aim of this research is to describe
Classical Principle in term of ``constructions'', of a general kind,
learning a value by trial-and-error, rather than computing it exactly.
This notion of ``construction'' may be equivalently described in many
ways. We may use notions from programming: continuations and
backtracking. We may use notion from game theory: Coquand's game
interpretation. We may use notions from topology: Hayashi's limit
interpretation.
Using this notion of construction, we may define, without using
Excluded Middle, models of Classical Arithmetic and non-recursive maps.
These models are algebraic structures, in the ordinary sense: a set of
individual equipped with maps and a notion of equality.