7

**
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
**

**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)
*

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

An unfortunate attempt to build a structure with fast quantifier elimination

by

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

** On the structure of normal $\lambda$-terms having a certain type** (gzipped ps-file)

by

** Approximate Belief Revision: A Preliminary Report** (gzipped ps-file)

by

** A Model Theoretic Approach to Translations Between Logics** (gzipped ps-file)

by

** Elementary number theory in weak fragments of arithmetic** (gzipped ps-file)

by

** Infinite SLaKE Tableaux** (gzipped ps-file)

by

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

by

** Lambek Grammars as Combinatory Categorial Grammars** (gzipped ps-file)

by

** Judging Unresolved Utterances in Context** (gzipped ps-file)

by

** A Fibring Semantics for the Semantic-Morphological Interface in Natural Language** (gzipped ps-file)

by

** A New Spectrum of Recursive Models** (gzipped ps-file)

by

** Intuitionistic Finitely Many-Valued Sequent Calculi** (gzipped ps-file)

by

** The Largest Cartesian Closed Category of Domains, Considered Constructively** (gzipped ps-file)

by

** A Gradient-Based Boosting Algorithm for Regression Problems** (gzipped ps-file)

by

** Towards Decision of Testing Equivalence for Petri Nets with Dense Time** (gzipped ps-file)

by

** Towards the Mechanical Verification of Textbook Proofs** (gzipped ps-file)

by

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