scientific article; zbMATH DE number 1302067
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 a paper of Sambin and the author in the same volume [\textit{G. Sambin} and \textit{S. Valentini}, ibid. 221-244 (1998; Zbl 0930.03091)]. 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 \dots{} 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 \dots{} our principle is that an abstraction is constructive \dots{} when information \dots{} 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). 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 \textit{A~set}, the form of judgement \textit{A~true}. The meaning of \textit{A~true} is that there exists an element \(a\) such that \(a\in A\) but it does not matter which particular element \(a\) is. Thus to pass from the judgement \(a\in A\) to the judgement \textit{A~true} is a 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 \textit{A~true}, an element \(a\) such that \(a\in A\) can be reconstructed. Of course the simple solution of adding only the rule \[ \frac{a\in A}{A\;true} \] allows us to obtain such a result but is completely useless in practice. In fact, it does not allow us to operate with judgements of the form \textit{A~true} and, in our experience, judgements of this form are essential in developing constructive mathematics, as for instance in formal topology, and in developing metamathematical arguments. To obtain the same result, but avoiding this limitation, we provide a general calculus for expressions, directly inspired by Martin-Löf's Siena lectures in April 1983 [see \textit{A. Bossi} and \textit{S. Valentini}, ``The expressions with arity, Internal Report, Dip. Sci. Inf., Univ. Milano N. 61/89 (1989)]. This calculus was first published by the author [\textit{S. Valentini}, ``Another introduction to Martin-Löf's type theory, in: R. Albrecht et al. (eds.), Trends in theoretical informatics (Schriftenreihe der Österreichischen Computer-Gesellschaft, Bd. 89, München) (1996)] and is similar for instance to that of \textit{B. Nordström, K. Petersson} and \textit{J. M. Smith} [Programming in Martin-Löf's type theory. An introduction (Oxford Univ. Press, Oxford) (1990; Zbl 0744.03029)]. The advantage of our calculus with respect to the other ones present in the literature is that its rules not only allow us to express all of the judgements of basic type theory, but also permit a rigorous treatment of judgements of the form \textit{A~true}. For the entire collection see [Zbl 0899.00026].
- Recovering Consistency by Forgetting Inconsistency
- Forgetting under the well-founded semantics
- Reasoning under inconsistency: a forgetting-based approach
- Principles of remembering and forgetting
- Retroactive interference model of forgetting
- Component properties of forgetting and progression in the situation calculus
- scientific article; zbMATH DE number 807470
- Knowledge forgetting: properties and applications
- The form of the forgetting curve and the fate of memories
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247312)
