Invited Papers

Some Applications of Explicit Provability
by Sergei Artemov (Moscow University, Russia, and Cornell University, USA)

Within explicit tradition in logic (Skolem, Herbrand, Henkin, Kowalski, and others) quantifiers are replaced by functions. This makes a difference in proof theory: the desired reflection principle

``there exists a proof of F '' -> F

is not provable, unlike its explicit version

``p is a proof of F'' -> F.

Needs of applications led to well known efforts to incorporate explicit proofs into logic (Curry, Kolmogorov, Gödel, Kreisel, Howard) and resulted recently in a coherent logic of propositions and proofs where the reflection principle is internally provable. In this talk we will present some fresh applications.

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 (gzipped ps-file)
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.

Completeness of an Action Logic Featuring a delta-Operator for Timed Transition Systems(gzipped ps-file)
by Fernando Náufel do Amaral and Edward Hermann Haeusler (Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro, Brazil)

On the structure of normal $\lambda$-terms having a certain type (gzipped ps-file)
by Sabine Broda and Luis Damas (Departamento de Ciência dos Computadores, Universidade do Porto, Portugal)

Approximate Belief Revision: A Preliminary Report (gzipped ps-file)
by Samir Chopra (CUNY Graduate Center and New York University, New York, USA),
  Rohit Parikh (Brooklyn College of CUNY and CUNY Graduate Center, New York, USA), and
  Renata Wassermann (Departamento de Ciência da Computação, Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)

A Model Theoretic Approach to Translations Between Logics (gzipped ps-file)
by Marcelo Coniglio and Walter Carnielli (Centro de Lógica, Epistemologia e História da Ciência, Universidade Estadual de Campinas, Brazil)

Elementary number theory in weak fragments of arithmetic (gzipped ps-file)
by Paola D'Aquino (Dipartimento di Matematica, Seconda Università degli Studi di Napoli, Italy)

Infinite SLaKE Tableaux (gzipped ps-file)
by Marcelo Finger (Departamento de Ciência da Computação, Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)

Reasoning About Dynamic Databases: Tableaux for Single-Step-Update Models (gzipped ps-file)

by Christian Fermüller (Institut für Computersprachen, Technische Universität Wien, Austria)

Lambek Grammars as Combinatory Categorial Grammars (gzipped ps-file)
by Gerhard Jäger (Zentrum für Allgemeine Sprachwissenschaft, Berlin, Germany)

Judging Unresolved Utterances in Context (gzipped ps-file)
by Peter Krause (Institut für Maschinelle Sprachverarbeitung, Universität Stuttgart, Germany)

A Fibring Semantics for the Semantic-Morphological Interface in Natural Language (gzipped ps-file)
by Ralf Naumann and Anja Latrouite (Seminar für Allgemeine Sprachwissenschaft, Universität Düsseldorf, Germany)

A New Spectrum of Recursive Models (gzipped ps-file)
by Andre Nies (Department of Mathematics, The University of Chicago, USA)

Intuitionistic Finitely Many-Valued Sequent Calculi (gzipped ps-file)
by Eugénia Reznik (Institut Supérieur d'Electronique de Paris, France), and
  Philippe Curmin (Groupe Cyber Informatique, Paris, France)

The Largest Cartesian Closed Category of Domains, Considered Constructively (gzipped ps-file)
by Dieter Spreen (Fachbereich Mathematik, Theoretische Informatik, Universität Siegen, Germany)

A Gradient-Based Boosting Algorithm for Regression Problems (gzipped ps-file)
by Richard Zemel and Toniann Pitassi (Department of Computer Science, University of Toronto, Canada)

Towards Decision of Testing Equivalence for Petri Nets with Dense Time (gzipped ps-file)
by Irina Virbitskaite (Institute of Informatics Systems, Siberian Division of the Russian Academy of Sciences, Novosibirsk, Russia)

Towards the Mechanical Verification of Textbook Proofs (gzipped ps-file)
by Claus Zinn (Division of Informatics, University of Edinburgh, Scotland)

Last modified: December 6, 2000, 06:14:27 GMT-0300.