# II Workshop on Logic and Semantics

Ilha Grande, Rio de Janeiro-RJ, Brazil, August, 26 - 30, 2013

The workshop will be placed at CEADS - UERJ

Contents

## Practical Information

- We will depart at 06:00am from UERJ at door #4 by bus to Mangaratiba. The bus can not wait for late people due to a connexion with the boat. So we propose that at 05:50am everybody should be on the door.
- At Mangaratiba we will take a boat to Ilha grande (between 10:00am and 11:00am).
At Vila do Abraão, arrival of the boat, we will take another busthat will take us to Vila do Presídio, where CEADS-UERJ is located.

**Warning:***anyone who tries to go by himself must walk 20km in a non-regular ground.*- We will be hosted at Vila do Presídio.
- For non-affiliateds with UERJ there is a fee of R$125.00/day including hosting and food. There are no hotels there.
- We will depart from Vila do Presídio on 30/08 at 08:00am to Rio de Janeiro in a transport provided by UERJ.

## Talks

### Edward Hermann Haeusler (PUC-Rio)

*A short discussion on non-standard finite computation*

This short-talk will discuss how computational models defined in toposes may lead to non-standard computational models. A possible comparison with hyper-computation is lightly motivated.

### Gilles Dowek (INRIA)

*On the definition of the classical connectives and quantifiers*

In this talk, a logic with a single notion of judgement, but mixing classical and constructive connectors and quantifiers, will be defined. In this logic, classical connectors and quantifiers are not primitive, but are defined from the constructive ones. Although a single notion of judgement is used, two notions of entailment are required.

### Jean-Baptiste Joinet (Université de Lyon)

*On Naturalness in Logic*

JY Girard's conception of logic originates in the critique of logical naturality made by G. Gentzen around 1930. Recently, Girard radicalized this critique and proposed a program for new foundations for logic, as a product of a general theory of interaction. In this talk, I will attempt to show that this program tends to reunify the idea of natural logic and the idea of a logic of nature, via the notion of computation.

### Lew Gordeew (Universität Tübingen)

*Toward optimal encoding of terms and proofs*

Traditional tree-like description of basic objects in algebra, logic and proof theory is very often unnecessarily voluminous, as compared to dag-like representations thereof. It is possible to formalize a natural idea of general tree-to-dag compressing functions and consider the corresponding minimal-size dag-like representations (abbr.: mdr). It turns out that mdr's can in some cases exponentially reduce the size of tree-like inputs. Generally the size of the mdr is bounded by the number of diff erent objects occurring (as labels) in the underlying tree. Moreover in the case of term algebra the mdr's are uniquely determined; in the proof theoretic case this uniqueness fails in general. Furhermore, in the latter case, in order to preserve the size under cut elimination it seems reasonable to upgrade dags to more sophisticated semidags, which leads to even more economical methods of proof encoding.

### Petrucio Vianna (UFF)

*Relational Algebra throughout Galois Connection*

We propose an alternative axiomatic system to relation algebra (RA), called Relational Algebra throughout Galois Connection (RAGC), that has some particular features: (1) the subjacent formalism of RAGC is the logic of order, instead of equational logic; (2) the set of primitive operations is not the same as the usual set of primitive operations of RA; (3) for each operation, there is a corresponding axiom establishing, a Galois connection between posets defined on binary relations. We illustrate how the use of Galois connections in RAGC make some steps "more deterministic" in the building of proofs.

### Renata de Freitas (UFF)

*Venn diagrams to Boolean algebra*

Venn diagrams were formalized as a deductive system, Venn II, by Sun Joo Shin (1994). Since the main motivation of this diagrammatic system is to test validity of syllogisms, the focus of the system is on a set of rules to establish consequence from a set of hypotheses. The user has no aid in proving validities, using the rules of the system. We present a diagrammatic deductive system for Boolean algebra that extends the system Venn II, in order to obtain a proper diagrammatic treatment of validity, not only of consequence.

### Rodolfo Ertola (UNICAMP)

*On Four Operations in Meet Complemented Distributive Lattices*

We study operations relating to Boolean and regular elements. The corresponding connectives may be interesting for fuzzy, modal and paraconsistent logic.

### Valeria de Paiva (Nuance Communications)

*Intuitionistic Modal Logic and Applications (IMLA): trying to cross the borders since 1999*

I want to review the programme of intuitionistic modal logic in its two original sources: modal logicians interested in Intuitionism and functional programmers/type theorists interested in (computational) modalities. I will discuss some trends of this kind of work since the first IMLA in Trento in 1999 and the tendencies that we can see in this line of work today.

### Wagner Sanz (UFG)

*Counterfactuals and "Argument"-Theoretic Semantics*

The famous dictum by Gentzen concerning introduction rules as a definition can be interpreted in a slight different way from those common in proof-theoretic semantics literature. Basically, introduction and elimination rules can be closely tied to the concepts of sufficient and necessary conditions, respectively. These two concepts afford a theoretical basis for considering the problem of how to characterize in a canonical way the semantics of many expressions, in particular logical constants. The proposal reveals its fecundity when the same concepts are used to provide an elucidation of counterfactuals in which the justification of correctness for counterfactuals is based on arguments taking as premisses sufficient and necessary conditions. Also, we hope to provide tools for semantical analysis which urges a revision of fregean theory of logical forms.