1,721,001 research outputs found
Relative formal topology, namely, the binary positivity predicate comes first
No full textIn this paper we introduce relative formal topology in order to deal constructively with
the closed subsets of a topological space as well as with the open ones.
In fact, within standard formal topology the cover relation allows for the definition of the
formal opens, namely, what is supposed to be the formal counterpart of the open
subsets, and within balanced formal topology the binary positivity predicate allows
for the definition of the formal closed subsets, namely, what is supposed to be the
formal counterpart of the closed subsets.
However, these approaches are fully satisfactory (according to the criterion introduced
by the author in "The problem of the formalization of constructive topology", Archive for Mathematical Logic (44/1), pp.115--129) only if an adequate formalization of the
cover relation and the positivity predicate can be provided.
But the present formalizations fail in this respect since some intuitionistically valid
relations between the open and the closed subsets of a concrete topological space
can not be expressed.
Our central result is that a generalization of the standard cover relation together with
a binary positivity predicate enjoying the positivity axiom solve the problem
Constructive characterizations of bar subsets
No full textWe provide some constructive characterizations of the notion of bar subset for
the complete binary tree, alias Cantor space, for the complete countable spreading tree, alias Baire Space, and, more generally, for an inductively generated formal topology.
Moreover, by using a completeness theorem for inductively generated formal topologies,
we prove that such characterizations are classically equivalent to the standard one
A proof of the normal form theorem for the closed terms of Girard's System F
No full textIn this paper a proof of the normal form theorem for the closed terms of Girard's system F is given by using a computability method A la Tait. It is worth noting that most of the standard consequences of the normal form theorem can be obtained using this version of the theorem as well. From the proof-theoretical point of view the interest of the proof is that the definition of computable derivation here used does not seem to be well founded
A note on a straightforward proof of normal form theorem for symply typed lambda-calculi
No full textExtensionality versus Constructivity
No full textWe analyze some extensions of Martin-Löf's constructive type theory by means of extensional set constructors and we show that often the most natural requirements over them lead to classical logic or even to inconsistency
On the formal points of the formal topology of the binary tree
No full textFormal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology have been obtained by using this approach. Here we analyze one of the main concepts in formal topology, namely, the notion of formal point. We will contrast two classically equivalent definitions of formal points and we will see that from a constructive point of view they are completely different. Indeed, according to the first definition the formal points of the formal topology of the real numbers can be indexed by a set whereas this is not possible according to the second one
The problem of the formalization of constructive topology
No full textFormal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in "Inductively generated formal topologies" by T.Coquand, G.Sambin, J.Smith and S.Valentini, Annals of Pure and Applied Logic (124). However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to this framework the method used to generate inductively formal topologies with a unary positivity predicate; the main problem that one has to face in such a new setting is that, as a consequence of the lack of a complete formalization, both the cover relation and the positivity predicate can have proper axioms
- …
