II Workshop da Sociedade Brasileira de Lógica

Important information

Where: Departamento de Computação - Campus do PICI, UFC (Fortaleza-CE)
When: September 28, 2018, 14:00h

About the Workshop

The II Workshop of the Brazilian Society of Logic is an initiative of the Brazilian Society of Logic - SBL. It consists of lectures and invited communications, with the aim of presenting a panel of the research in Logic in Brazil (and in particular, in the Northeast), in all its aspects: Philosophy, Computer Science, Mathematics.

The keynote speakers of the Workshop will be Yiannis Moschovakis (UCLA, California) and Luiz Carlos Pereira (PUC-Rio and UERJ).

The Workshop will be held in the Department of Computer Science, Campus do Pici, the same week in which an edition of the traditional LSFA event - Logical and Semantic Frameworks, with Applications (September 26 to 28) takes place in Fortaleza.

All presentations of the Workshop will be given in English.

Workshop programming

14h00-14h25 Mário Benevides (COPPE-UFRJ)
14h30-14h55 Umberto Rivieccio (UFRN)
15h00-15h25 Maurício Ayala-Rincón (UnB)
15h30-16h10 Luiz Carlos Pereira (PUC-Rio e UERJ) (keynote speaker)\\

16h10-16h30 Coffee break

16h30-16h55 Carlos Brito (UFC)
17h00-17h25 Marcos Silva (UFAL)
17h30-17h55 Samuel G. da Silva (UFBA e SBL)
18h00-18h40 Yiannis Moschovakis (UCLA e Univ.Athens) (keynote speaker).Athens) (keynote speaker)

Abstracts of the talks

Mario Benevides (COPPE-URFJ) - Propositional Dynamic Logic for Bisimilar programs with Parallel Operator and Test

Abstract: In standard Propositional Dynamic Logic (PDL) literature, the semantics is given by Labeled Transition Systems, where for each program π we associate a binary relation Rπ. Process Algebras also give semantics to process (terms) by means of Labeled Transition Systems. In both formalisms, PDL and Process Algebra, the key notion to compare processes is bisimulation. In PDL, we also have the notion of logic equivalence, that can be used to prove that π1 and π2 are logically equivalent ⊢ ⟨π1⟩φ ↔ ⟨π2⟩φ. Unfortunately, logic equivalence and bisimulation do not match in PDL. Bisimilar programs are logic equivalent but the converse does not hold. In this talk we present a semantics and an axiomatization for PDL that makes logically equivalent programs also bisimilar. This allows for developing Dynamic Logics to reasoning about process algebra specifications, in particular about CCS (Calculus for Communicating Systems). As in CCS, bisimulation is the main tool to establish equivalence of programs, it is very important that these two relations coincide. We propose a new Propositional Dynamic Logic with a new non-deterministic choice operator, PDL+. We prove its soundness, completeness, finite model property and EXPTIME-completeness for the satisfiability problem. We also add to PDL+ the parallel composition operator (PPDL+) and prove its soundness and completeness. We establish that the satisfiability problem for PPDL+ is in 2-EXPTIME. Finally, we define some fragments of PPDL+, prove its EXPTIME-completeness and discuss some issues concerning test operator and point out some direction on how it can be handled.

Umberto Rivieccio - Dualities for two-sorted lattices

Abstract: Duality theory is an attempt at understanding algebras (of logic) via topological methods. For algebras related to logic, the earliest and most important result in this field is M. Stone’s representation of Boolean algebras via certain compact Hausdorff spaces today known as Stone spaces. A new perspective was brought into duality theory by H. Priestley, who introduced ordered topological spaces (Priestley spaces) to give an elegant representation of distributive lattices and related structures. Nowadays the results of Stone and Priestley have been extended in several directions, obtaining dualities for many classes of algebras related to logic: modal algebras, Heyting algebras (algebras of intuitionistic logic), MV-algebras (Lukasiewicz many-valued logic) as well as more esoteric algebras of non-classical logic. As I will show, some of these can be presented as many-sorted structures in a way that has proved quite insightful. In particular, it makes it possible to adapt straightforwardly the results of Stone and Priestley to obtain neat dualities for a variety of non-classical algebras.

Luiz Carlos Pereira - Gödel's Koan (Full abstract)

"A koan is a story, dialogue, question, or statement, which is used in Zen practice to provoke the 'great doubt' and test a student's progress in Zen practice." (Wikipedia)

Abstract: In 1968 William Howard proposed an assignment of ordinals less than epsilon zero to terms for primitive recursive functionals of finite type with the property that the reduction of a term always lowers its ordinal measure. In a certain sense, it was Howard’s assignment that motivated the appearance in 2014 of problem 26 (submitted by Henk Barendregt) in the TLCA list of open problems, the so-called Gödel's Koan.

The aim of this paper is to explore three different routes to the solution of Gödel's Koan:

 * Disatrous derivations;
 * Mimpgraphs; and
 * Gentzen's reduction.

(joint work with Edward Hermann Haeusler, PUC-Rio, e Daniel Durante, UFRN)

Mauricio Ayala-Rincón - Termination of Rewriting Systems and Recursive Functions

Abstract: Termination is a fundamental logical property of great interest in computability that despite the well-known fact of being undecidable has given rise to the development of several semi-decision technologies, by its relevance in specification, verification and programming. The talk will focus in the adaptation of the criterion known as Dependency Pairs, originally developed to check termination of term rewriting systems, to the formal verification of this property for functional specifications.

Joint work with Ariane Alves, César Muñoz and Mariano Moscato.

Carlos Brito - Languages, Tools and Machines

Abstract: The representationalist paradigm, as well as the pragmatist paradigm of the philosophy of language are based on some notion of knowledge: the first on the notion of "know that" and the second on the notion of "know how". In this talk, we are going to investigate situation where the use of language does not rely on any notion of structured knowledge whatsoever --- which lead us to a new paradigm for the philosophy of language based on the idea of "not knowing".

Marcos Silva - Revision of logic: a pragmatist proposal

Abstract: How can we rationally justify our logical principles if the very possibility of rational justification presupposes them? How can we use reason to ground a set of basic principles of reason as the correct one without circularity or any infinite regress? My proposal aims at developing some tenets presented in Wittgenstein’s On Certainty by offering an integrated pragmatist view about the possibility of non-classical logics and logical pluralism. I then apply Wittgenstein’s hinge epistemology and his anti-realism into the discussion about rival logics. Accordingly, I reject a realist approach to logic and propose a view in which the nature of logical principles is related to Moorean propositions. I aim to show that, if logical principles are to be taken as Moorean propositions, we have to acknowledge the role that education, institution, and conversion play in our inferential practices.

Samuel G. da Silva - The Axiom of Choice and the Partition Principle from Dialectica Categories

Abstract: The method of morphisms is a well-known application of Dialectica categories to Set Theory (more precisely, to the theory of cardinal invariants of the continuum). In a previous work, Valeria de Paiva and the author have asked how much of the Axiom of Choice is needed in order to carry out the referred applications of such method. In this paper we show that, when considered in their full generality, those applications of Dialectica categories give rise to equivalents (within ZF) of either the Axiom of Choice (AC) or of the Partition Principle (PP) – which is a consequence of AC whose precise status of its relationship with AC itself is an open problem for more than a hundred years.

Yiannis Moschovakis - A survey of the origins and development of Descriptive Set Theory

Abstract: The central problem of Descriptive Set Theory was posed by Henri Lebesgue in a classic 1905 article: to identify and study the properties of those sets and functions on the real numbers which are "analytically definable". Today we recognize Lebesgue's paper as one of the first important contributions to the "theory of definability", especially as it led in time into a broa study of "first order definability over the real numbers".

My aim in this expository talk is to outline the history of this field which has important applications (especially to analysis) but also interacts substantially with the general theory of sets, logic and even computability theory; I will assume some basic knowledge of these fields but no special knowledge of Descriptive Set Theory.

Organising Committee

Samuel Gomes da Silva (UFBA e SBL) - Co-chair
Francicleber Martins Ferreira (UFC) - Co-chair
Márcia Roberta Falcão de Farias (UNILAB)

Note: The first two editions of the SBL Workshop (2017 and 2018) took place in Northeast Brazil. The SBL is open to proposals for the organization of Workshops in other regions of the country, always seeking to take advantage of the presence of Logic researchers in a given city due to the accomplishment of some major event.

SBL - Brazilian Logic Society