Objective S/Semantics

The guiding motto of the semantic perspective on the GeTFun quest is to experiment with generalizations of the notion of truth-functionality, looking into different ways of controlling the amount of non-determinism allowed by each non-standard variety of semantics. An important and very natural semantics of this genus is the so-called non-deterministic semantics, introduced and studied by Avron and collaborators in the last decade. This variety of non-deterministic approach, when applied to ordinary multi-valued matrices, extends the notion of truth-functionality in producing the so-called Nmatrices, with the following behavior: in an Nmatrix, the truth-value of a complex formula is chosen non-deterministically from some non-empty set of options. A legal valuation in an Nmatrix is a mapping from formulas to logical values satisfying such constraints. Since their inception, Nmatrices have proven to be a truly powerful tool. Their use preserves all the advantages of ordinary many-valued matrices, but they are applicable to a much wider range of logics. A particularly useful feature of Nmatrices is its modularity: the semantics of a proof system based on an Nmatrix is often obtained by joining the semantics of its component rules, while the main effect of each of the rules is to reduce the degree of non-determinism of the underlying logical operations. This procedure has indeed been successfully applied, in recent years, to provide simple and modular semantics for a myriad of non-classical logics. Other analogous samples of the same non-deterministic genus, which have been studied by Marcos and collaborators, go in two different directions, being either more relaxed and inclusive (such as society semantics), thus less comprehensive, or more strict and restrictive (such as possible-translations semantics), thus more far-reaching, on what concerns the class of legal valuations. Particularly interesting is to notice that non-determinism also takes place when truth-functionality is abandoned in favor of more classic-like viewpoints, such as the one that construes logical systems, semantically, as well-defined non-truth-functional collections of two-valued mappings on the set of formulas. The so-called theory of valuations that underlies the latter stance has been extensively studied by Béziau and others, but many results that make these ideas more computationally treatable are only nowadays emerging, due to the work of Caleiro and others. Finally, the task of generalizing even the basic notion of a truth-value and the very approach to logical entailment thus, to the question of "what a logic is" has been recently proposed and investigated by Shramko and others. The foundational task of categorizing, in Universal Logic terms, the reach of each specific class of "broadly truth-functional logics" immediately imposes itself. The semantical track of the GeTFun project is connected to such foundational task and also, to a greater extent, to the fine development of the technical background to any related ulterior investigation.

Objective P/Proof-theoretic frameworks

The work on proof-theoretical generalizations of PoC falls into two main classes: work that generalizes Gentzen-type deductive systems by adding syntactical information to these systems, be them generic labels (labeled deductive systems of several stripes), different levels of sequents (e.g., hypersequents), terms (e.g., CHI), or a proof-search strategy (e.g., focusing); and work that constrains the deductive system via a strongly adequate semantics for it (as in the bivalent approach, or in the non-deterministic approach). To describe very succinctly our proof-theoretical subobjectives, a first thread is concerned with labeled deductive systems as an "enabling technology". Labeling creates a strong bridge between model theory and proof theory, as it is based on adding semantic information to the deductive systems in question. The bivalent approach, in particular, presupposes the simplest logically meaningful labeling strategy, and there are several competing recipes for lifting this approach so as to be applicable to multiple-valued semantics, including those of the non-deterministic stripe. A second thread is proposed to stay syntactically closer to the original structural Gentzen systems, being based on "focusing disciplines" for some of the logics that generalize the notion of truth-functionality. An overarching theme relating both threads is the idea of Curry-Howard correspondences, which, in one hand are "labeled deductive systems" where the labels are simply lambda-calculus terms, but on the other hand, try to stay closer to the original Gentzen systems for Natural Deduction and as such are amenable (as we claim and intend to prove) to focusing methods. These should also be investigated within the frameworks of hypersequents and n-sided sequents. A third thread to be investigated, generalized proof-theoretic properties, is more foundational and all-embracing. It concentrates on generalized proof-theoretic properties encompassing the approaches based on bivaluations and on Nmatrices as setting constraints not only on the classes of legal valuations but also on the deductive systems that characterize them. The semantic characterization of both syntactic and proof-theoretical properties of each non-standard variety of semantics of interest is intended to work as a bridge between proof and model theory. In particular, one of the main methods for developing Gentzen-type systems for non-classical logics is precisely to translate many-valued semantics (deterministic or non-deterministic) into a bivalent framework.

Objective W/Applications

Many of the logical systems that our project investigates came to the fore as meaningful generalizations of the work on applied logic. So it is not surprising that we keep a focus on applications of complex and interacting systems. We organized these applications here into three broad areas: investigating modal logics (with many uses, from security in computer science, specially of the reactive type, to modeling of quantum systems); investigating logics for reasoning under uncertainty and inconsistency (several of our WPs are concerned with paraconsistent and fuzzy logics, for instance, with applications to knowledge representation and databases, but also to probabilistic reasoning); and W3, where the attention is devoted to combinations of logical systems (e.g., fuzzy modal logics, where compositionality will profit the most from results stemming from objectives S and P).


Marie Curie project PIRSES-GA-2012-318986 funded by EU-FP7 (January 1, 2013 - December 31, 2016)