Hotel Barreira Roxa, Natal, Brazil

Scientific Sponsorship
Interest Group in Pure and Applied Logics (IGPL)
European Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
Sociedade Brasileira de Computação (SBC)
Sociedade Brasileira de Lógica (SBL)

Funding 
,
Fundação Norte-Rio-Grandense de Pesquisa e Cultura (FUNPEC)
Pró-Reitoria de Extensão, Univ. Fed. do Rio Grande do Norte (PROEX-UFRN)

Organisation
Centro de Informática, Universidade Federal de Pernambuco (CIn-UFPE) 
Departamento de Informática e Matemática Aplicada, Univ. Fed. do Rio Grande do Norte (DIMAP-UFRN)

Title and Abstract of Invited Talks

XML and the hypertextual electronic library of mathematics
by Andrea Asperti (Department of Computer Science, University of Bologna, Italy)

There is a compelling need of integration between the current tools for automation of formal reasoning and mechanization of mathematics (proof assistants and logical frameworks) and the most recent technologies for the development of web applications and electronic publishing. We explain the pivotal role that should be played by the Extensible Markup Language in this integration process, and how the many different pieces of technology under development at World Wide Web Consortium (W3C) should naturally fit together for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge.

Definability, Measure and Randomized Algorithm
by Angus Macintyre (Department of Mathematics, Edinburgh University, UK)

Some of the most important work in the Robinson tradition of model theory involves the connection between definitions and the geometric or topological structure of the sets thereby defined. The most notable examples involve real or p-adic structure, particularly in the recent work,initiated by Wilkie, on o-minimal structures. In those situations, not only are the sets defined locally closed, and so measurable, but they satisfy a very strong uniform Law of Large Numbers (Finiteness of Vapnik-Chervonenkis Dimension). In certain cases, this has implications for very fast randomized algorithms, and even for the mathematics of learning on sigmoidal neural networks. The tutorial will cover the basic theory, and the most notable examples.

Translations and Normalization Procedures
by Luiz Carlos Pereira (Department of Philosophy, Pontificial Catholic University of Rio de Janeiro, Brazil)

The aim of the present paper is to explore some interesting connections between translations among logics and different normalization procedures (A similar proof-theoretical approach to translations was used by Prawitz and Malmn\"{a}s in their seminal paper [PrawMal68]).

The traditional family of double-negation translations from Classical Logic into Intuitionistic Logic (Gentzen-Gödel-Kolmogorov) were defined and studied in the context of foundational matters. Gentzen, for example, explicitly considered as one of the main consequences of his translation procedure, the reduction of the consistency problem of classical arithmetic to that of intuitionistic arithmetic. The main ideas behind these translations are:

(1) Introduce a double negation in front of every atomic formula (in the Kolmogorov-variant, in front of every part of the formula);
(2) Replace some key logical operators by adequate classical equivalents (Gödel-Gentzen variants).

The crucial property that makes these translation work is stability. A for mula $A$ is called stable if and only if $(A \leftrightarrow \lnot \lnot A)$. The desired results about translations then follow from the fact that formulas in appropriate language fragments of intuitionistic logic are stable (negative formulas, for example).

It can be easily verified that this family of translations (sometimes called negative translations) is proof-theoretically justified by the normalization procedure for classical logic used by Prawitz (see [Prawitz65]). Prawitz shows, as a preliminary result to normalization, that every application of the classical absurd rule in the fragment $\{ \land , \rightarrow , \bot, \forall \}$ of the natural deduction system C can be reduced to an atomic application. Prawitz defines a set of operations (reductions) whose aim is to transform non-atomic applications of the classical absurd (in the fragment considered) into simpler ones. For example, the derivation

...

The two new applications of the classical absurd rule are obviously simpler than the original one.

The moral is: in the given fragment, classical reasoning can be restricted to atomic formulas. We can easily see now that everything is ready for the Gentzen-Gödel translations: we define disjunction and the existential quantifier (and implication in Gödel's translation), and double negation can be restricted to atomic formulas.

In 1989, J. Seldin presented a new normalization strategy where he showed that every derivation in the fragment $\{ \land , \lor , \rightarrow , \bot , \exists \}$ could be transformed into a derivation with at most one application of the classical absurd rule (see [Seldin89]). Moreover, if this application occurred, it would be the last rule in the resulting derivation. Seldin defined new reduction procedures that allow us to permute applications of the classical absurd rule downwards. For example, the derivation

...

The moral now is: in this new fragment, classical reasoning, if used at all, is used as the last step of an argument. Every classical derivation $\Pi$ in the fragment can now be put in this very special form constituted of two parts: an intuitionistic part and a classical part (possibly empty) constituted of a single application of the classical absurd rule. Normalization for Classical Logic is now reduced to normalization for Intuitionistic Logic.

This normalization procedure clearly gives rise (1) to a new translation from classical logic into intuitionistic logic, and (2) to an extension of Glivenko's theorem to first order logic. In the case of classical propositional logic, the translation function $Tr$ would be simply: $Tr(A) = \lnot \lnot A$ (Glivenko's theorem is a trivial consequence of Seldin's normalization strategy).

In the second part of the paper, we extend this proof-theoretical analysis to translations from intuitionistic logic into classical linear logic. We present a new single-conclusion Natural Deduction system \footnote{A similar system was independently defined and studied in [Maraist99]} for the $\{\otimes , \bot, \multimap, \oplus, \}$-fragment of classical linear logic, and we prove the normalization theorem for this system. The system is based on an involution rule defined as follows:

...

We also discuss the extension of semantical proofs of st rong normalizability (based on reducibility predicates) to the classical linear system based on the involution rule.

Although, as we have already said, traditional translations were introduced within the framework of foundational questions, it is certainly true that the interest on translations is not restricted to this kind of question. In the final part of the paper, we discuss the translation proposed by P. Krauss [Krauss95] and its relation to some general conceptual aspects of the concept of translation. In particular, we discuss the fact that translations that introduce double negations at the atomic level are not in general functorial, i.e., they do not commute with substitution (We would like to thank Per Martin-Löf for calling our attention to this fact).

References

[Dragalin88] Dragalin, A.G., Intuitionism - Introduction to Proof Theory, American Mathematical Society, 1988.
[Gentzen33] Gentzen, Gerhard, Über das Verhältnis zwischen intuitionistischer und klassischer Logik, in Archiv für Mathematische Logik und Grundlagenforschung 16 (1974).
[Gentzen35] Gentzen, Gerhard, Untersuchungen über das Logische Schliessen, in Matematische Zeitschrift, vol.39, pp.176-210, 405-431, 1935. English translation in Szabo [10].
[Girard71] Girard, J.Y., Une extension de l'Interpretation de Gödel a l'Analyse et son application a l'elimination des coupures dans l'analyse et la theorie des types, in Proccedings of the Second Scandinavian Logic Symposium, ed. by J.E.Fenstad, North-Holland, Amsterdam, 1971.
[Godel33a] Gödel, K., Eine Interpretation des Intuitionistischen Aussagenkalküs, in Ergebnisse eines mathematischen Kolloquiums, 4, 1933.
[Godel33b] Gödel, K., Zur intuitionistischen Arithmetik und Zahlentheorie, in Ergebnisse eines mathematischen Kolloquiums, 4, 1933.
[Kolmogorov25] Kolmogorov, R.A., On the Principle of the Excluded Middle, translation in van Heijenoort (1967).
[Krauss95] Krauss, P.H., Hypothetical Extensions of Constructive Mathematics, in The Foundational Studies, ed. by DePauli-Schimanovich et al., Kluwer, 1995.
[Maraist99] Maraist, J., Classical linear natural deduction and the linear $\lambda_{\triangle}$ calculus: a preliminary report, preliminary draft, 1999.
[Pereira99] Pereira, L.C., Translations and Normalization: applications to Linear Logic, abstract in Linear Logic and Applications - Seminar-report, Dagstuhl, 1999.
[Pottinger77] Pottinger, G., Normalization as a Homomorphic Image of Cut-Elimination, in Annals of Mathematical Logic, vol.12, n.3, 1977.
[Prawitz65] Prawitz, Dag, Natural Deduction, Almqvist and Wiksell, Stockholm, 1965.
[Prawitz71] Prawitz, Dag, Ideas and Results in Proof Theory, in Proccedings of the Second Scandinavian Logic Symposium, ed by J.E.Fenstad, North-Holland, Amsterdam, 1971.
[PrawMal68] Prawitz, Dag and Malmnäs, P.-E., A survey of some connections between classical, intuitionistic and minimal logic, in Contributions to Mathematical Logic, eds. A. Schmidt, K. Schütte and H.J. Thiele, North-Holland, 1968.
[Seldin86] Seldin, J. On the proof-theory of the intermediate logic MH, JSL 51, pp. 626-647, 1986.
[Seldin89] Seldin, J. Normalization and Excluded Middle I, in Studia Logica 48, pp. 193-217, 1989.
[Szabo69] Szabo, M.E., The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969.
[Troelstra96] Troelstra, A.S. and Schwichtemberg, H., Basic Proof Theory, CUP, Cambridge, 1996.
[vanHeijenoort67], van Heijenoort, J., From Frege to Gödel, Harvard University Press, 1967.

A New Proof of the Weak Pigeonhole Principle
by Toniann Pitassi (Department of Computer Science, University of Toronto, Canada)

The exact complexity of the weak pigeonhole principle is an old and fundamental problem in proof complexity. It is used in all areas of mathematics, and has been the primary hard example underlying lower bounds in propositional proof complexity.

Still, the exact complexity of the pigeonhole principle is not known, and is linked to several important problems in proof complexity and circuit complexity. Using a clever diagonalization argument, Paris, Wilkie and Woods present quasipolynomial-size bounded-depth proofs of the weak pigeonhole principle. Their argument was further refined by Krajicek. In this talk, we present a new proof: we show that the weak pigeonhole principle has quasipolynomial-size proofs where every formula consists of a single AND/OR of polylog fanin. Our proof is conceptually simpler than previous arguments and is optimal with respect to depth.

This is joint work with Alexis Maciel and Alan Woods.

Une tentative mmalheureuse de construction d'une structure eliminant rapidement les quanteurs /
An unfortunate attempt to build a structure with fast quantifier elimination
by Bruno Poizat (Institut Girard Desargues, Université Claude Bernard, Lyon-1, France)

Pour illustrer le court cours, je tenterai de construire une structure M éliminant rapidement les quanteurs, dans un langage fini : à toute formule existentielle (E y1,..yn) f(x1, ...xm,y1, ..yn), où f est sans quanteurs, doit être associée une formule g(x1,...,xm), également libre de quanteurs, qui lui soit equivalente dans M, la longueur de g étant polynomialement bornée en fonction de celle de f. Tant qu'à faire, j'aimerais aussi que g fut calculée par un algorithme polynomial à partir de f.
Pourquoi je veux faire ça? Parce que si c'etait vrai de la structure a deux elements M={0,1}, dans le langage reduit a la seule relation x=0, eh bien on repondrait positivement à deux questions ouvertes en complexité, NC1=P=NP; la même chose se produirait si la structure etait finie, hormis le cas trivial d'une structure a un element que nous excluons, ou bien si son langage fini ne comportait que des relations et pas de fonctions.
Cette relativisation quelque peu artificielle du problème P=?NP ne semble pas si aisée, et je n'arrive seulement qu'à construire une structure qui n'a cette propriété que pour les formules existentielles dans lesquelles ne survit qu'une seule variable libre. Celà vient de ce que je me restreins à un langage qui ne comporte que des fonctions et des predicats unaires, dont l'avantage est de présenter une théorie des modèles tres rudimentaire; il est possible que la méthode que j'emploie, qui consiste à introduire un predicat de verité, puisse se géneraliser pour emporter le morceau, mais ça devrait être substantiellement plus dur.

(In English)

As an illustration of the tutorial, I will make an attempt to build a structure M with fast quantifier elimination, in a finite language: to each existential formula (E y1,..yn) f(x1, ...xm,y1, ..yn) , where f is quantifier free, should be associated an equivalent in M free formula g(x1,...,xm), the length of g being polynomially bounded in function of the length f . It would even be better if g could be calculated from f by a polynomial algorithm. Why do that? Because if the thing were true of the two-element structure M={0,1}, in the language of the only relation x=0, this would give a positive answer to two open questions in Complexity theory, NC1=P=NP; the same would hold in the case of a finite M, except in the trivial case of a one-element structure, or if the language is purely relationnal. This somehow artificial relativisation of the P=?NP problem seems to be not totally straightforward, and all what I can do is to produce a structure which has this property only when there remains only one surviving free variable in the existential formula. This comes from the fact that I need an extremely rudimentary model-theoretic context, which is provided by a language containing only unary functions and predicates ; I see nothing forbiding the extension of the method, which consists in the introduction of a truth predicate, to settle the question, but I assume that it will be considerably harder.

Linearity in Distributed Computation
by Glynn Winskel (BRICS, Aarhaus University, Denmark)

Gian Luca Cattani and I have worked on a path-based domain theory for interacting processes, one aim being a general theory of bisimulation, also for higher-order process languages. The category of domains forms a model of Girard's linear logic. But what does the linearity mean in the context of interacting processes, and what are its consequences? This talk will explain, and indicate how widespread linearity is by showing that the operations of a range of process calculi can be expressed within a linear metalanguage, designed around the domain theory. Roughly, linearity is about how to manage without a presumed ability to copy. With hindsight it is not surprising that the copying of processes is limited in the context of distributed computation, either as a fact of life, often because remote networks are simply too complicated to have control over, or deliberately, as is the case in the design of cryptographic protocols. Of course, code can be sent explicitly to be copied and the domain theory allows for different possibilities for copying processes.

Last modified: July 19, 2000, 17:06:27 GMT-0300.