The forget-restore principle: a paradigmatic Example
Silvio Valentini · Oxford University Press eBooks · 1998
The aim of this paper is to give a simple but instructive example of the forget-restore principle, conceived by Giovanni Sambin as a discipline for a constructive development of mathematics and which first appeared in print in the introduction of Sambin and Valentini 1998. The best way to explain such a philosophical position is to quote from that paper: “To build up an abstract concept from a raw flow of data, one must disregard inessential details ... this is obtained by forgetting some information. To forget information is the same as to destroy something, in particular if there is no possibility of restoring that information ... our principle is that an abstraction is constructive ... when information ... is forgotten in such a way that it can be restored at will in any moment.” The example we want to show here refers to Martin-Löf’s intuitionistic type theory (just type theory from now on). We assume knowledge of the main peculiarities of type theory, as formulated in Martin-Löf 1984 or Nordström et al. 1990. Type theory is a logical calculus which adopts those notions and rules which keep total control of the amount of information contained in the different forms of judgement. However, type theory offers a way of “forgetting” information: that is, supposing A set, the form of judgement A true. The meaning of A true is that there exists an element a such that a ∈ A but it does not matter which particular element a is (see also the notion of proof irrelevance in de Bruijn 1980). Thus to pass from the judgement a ∈ A to the judgement A true is а clear example of the forgetting process. We will show that it is a constructive way to forget since, provided that there is a proof of the judgement A true, an element a such that a ∈ A can be reconstructed.