Francesco Ciraulo

Research field: Mathematical Logic    

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


Publications:

  • F. Ciraulo - T. Kawai - S. Maschio "Factorizing the Top-Loc adjunction through positive topologies" (submitted; preprint version here arXiv:1812.09190).
  • F. Ciraulo "σ-locales in Formal Topology" (submitted; preprint version here arXiv:1801.09644).
  • F. Ciraulo "Overlap Algebras as Almost Discrete Locales" (submitted; preprint version here arXiv:1601.04830).
  • S. Bredariol - F. Ciraulo "Educare al pensiero razionale nella scuola primaria: una proposta didattica", L'Insegnamento della Matematica e delle Scienza Integrate 42 (2019), pp. 139-158.
  • O. Gaggi - F. Ciraulo - M. Casagrande. 2018. "Eating Pizza to learn fractions". In International Conference on Smart Objects and Technologies for Social Good (Goodtechs ’18), November 28–30, 2018, Bologna, Italy. ACM, New York. DOI:10.1145/3284869.3284921
  • F. Ciraulo "Geometria fra immagini, immaginazione e... "magia"!", L'insegnamento della  matematica e delle scienze integrate 41 (2018), pp. 691-709.
  • F. Ciraulo - D. Rinaldi - P. Schuster "Lindenbaum's Lemma via Open Induction", in R. Kahle and T. Strahm and T.Studer (eds.) "Advances in Proof Theory", Progress in Computer Science and Applied Logic 28, Birkhäuser Basel (2016), pp. 65-77.
We begin the study of (not necessarily complete) partial orders with some notion of "overlap" or "positivity". We propose several kinds 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.
I show that the regular open subsets of a formal topology form an overlap algebra and that every (set-based) overlap algebra can be represented in this way.
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.
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).
  • 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:

  • "Equazioni booleane e matematizzazione... nell'isola di Smullyan", convegno "Educare alla razionalità", Torino, 22-23 maggio 2019.
  • "Overtness and density for σ-locales" at "CCC 2018", Faro, Portugal, September 24-28, 2018.
  • "Notions of Booleanization in pointfree Topology" at "Constructive Mathematics", Haudorff research Insitute for Mathematics, Bonn, Germany, August 6-10, 2018 (video).
  • "σ-locales and Booleanization in Formal Topology" at "CCC 2017", Nancy, France, June 26-30 2017.
  • "Boolean locales: a constructive analog" at the "Logic Colloquium 2013", Évora, Portugal, July 22-27 2013.
  • "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.