Francesco Ciraulo

Research field: Mathematical Logic    

Main topics: intuitionistic logic, constructive mathematics, formal topology.    


Publications:

  • F. Ciraulo - G. Sambin "A constructive Galois connection between closure and interior", Journal of Symbolic Logic, to appear (preprint version arXiv:1101.5896v2).
In this paper we study what are the links between closure and interior operators from an intuitionistic point of view. In particular, we are interested in understanding whether a closure operator can determine an interior operator or not; and vice versa. Classically, the picture is very clear: closure and interior are determined by each other via complement. Intuitionistically, all is more complex, as usual. We describe a way to construct the largest interior ``compatible'' with a given closure and, dually, the largest closure ``compatible'' with a given interior. Here ``compatible'' stands for a suitable link between interior and closure which is valid intuitionistically. In contrast with the classical picture, these two constructions are not inverse one to another. In fact, they form a Galois connection.
  • F. Ciraulo "Regular opens in Formal Topology and a representation theorem for overlap algebras", Annals of Pure and Applied Logic, to appear (preprint version .pdf).
I show that the regular open subsets of a formal topology form an overlap algbera and that every (set-based) overlap algebra can be represented in this way.
  • F. Ciraulo - M. E. Maietti - P. Toto "Constructive version of Boolean algebra", Logic Journal of the IGPL, to appear (preprint version arXiv:1203.4997v1).
We begin the study of (not necessarily complete) partial orders with some notion of "overlap" or "positivity". We propose several kind of structures which, classically, turn out to be Boolean algebras. For instance, it is well-known that the collection of all finite and cofinite subsets of a given set form a Boolean algebra, classically. Intuitionistcally, on the contrary, we are able to describe it as a partial order with overlap.
  • F. Ciraulo "Sull'algebra degli insiemi in matematica intuizionista" in E. Ballo and C. Cellucci (eds.), "La ricerca logica in Italia. Studi in onore di Corrado Mangione", Quaderni di Acme 124, pp. 261-274, Cisalpino, Milano (2011).
We develop a piece of constructive Topology within the language of overlap algebras. In particular, we show how to express the notion of regular open set and that of regular space in such an algebraic framework. This approach is fully intuitionistic and so we can avoid any use of set-theoretic complement. We succeed in characterize the link between the interior operator and the closure operator in an intuitionistic way. The main result of the paper is that the regular open sets of a regular space form an overlap algebra which, in general, is atom-less.
  • F. Ciraulo "Soddisfacibilità costruttiva", La Matematica nella Società e nella Cultura, Rivista dell'Unione Matematica Italiana, Serie I, Vol. I, pp. 275-278 (2008).

Preprints:

  • F. Ciraulo - M. E. Maietti - G. Sambin "Convergence in Formal Topology", Preprint n. 342, Dipartimento di Matematica ed Applicazioni, Università degli Studi di Palermo (2008).
  • F. Ciraulo - G. Sambin "Tense logic within a constructive metatheory", Preprint n. 341, Dipartimento di Matematica ed Applicazioni, Università degli Studi di Palermo (2008).

My Ph.D. thesis: Constructive Satisfiability (.pdf)

A constructive (i.e. intuitionistic and predicative) analysis of the logical notion of satisfiability (and also non-deducibility) for first-order intuitionistic logic. From a semantic point of view, the main tool is formal topology theory and, in particular, the notion of (binary) positivity. Co-inductive methods are used in many proofs.


Conference Presentations:

  • "The overlap relation in intuitionistic lattice theory" at the "XXIV Incontro di Logica", Bologna, Italy, 2-4 February 2011.
  • "Satisfiability and Consistency from a constructive point of view" at the "XXIII Incontro di Logica", Genova, Italy, 20-23 February 2008.
  • “A constructive treatment of satisfiability (with an application to tense logic)” at the “3rd Workshop on Formal Topology”, Padua, Italy, 7-12 May 2007.