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)
Some Applications of Explicit Provability
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
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);
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.
A New Proof of the Weak Pigeonhole Principle
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 /
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.
(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
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)
On the structure of normal $\lambda$-terms having a certain type (gzipped ps-file)
Approximate Belief Revision: A Preliminary Report (gzipped ps-file)
A Model Theoretic Approach to Translations Between Logics (gzipped ps-file)
Elementary number theory in weak fragments of arithmetic (gzipped ps-file)
Infinite SLaKE Tableaux (gzipped ps-file)
Reasoning About Dynamic Databases: Tableaux for Single-Step-Update Models (gzipped ps-file)
Lambek Grammars as Combinatory Categorial Grammars (gzipped ps-file)
Judging Unresolved Utterances in Context (gzipped ps-file)
A Fibring Semantics for the Semantic-Morphological Interface in Natural Language (gzipped ps-file)
A New Spectrum of Recursive Models (gzipped ps-file)
Intuitionistic Finitely Many-Valued Sequent Calculi (gzipped ps-file)
The Largest Cartesian Closed Category of Domains, Considered Constructively (gzipped ps-file)
A Gradient-Based Boosting Algorithm for Regression Problems (gzipped ps-file)
Towards Decision of Testing Equivalence for Petri Nets with Dense Time (gzipped ps-file)
Towards the Mechanical Verification of Textbook Proofs (gzipped ps-file)
Last modified: December 6, 2000, 06:14:27 GMT-0300.
Invited Papers
by Sergei Artemov (Moscow University, Russia, and Cornell University, USA)
by Luiz Carlos Pereira (Department of Philosophy, Pontificial Catholic University of Rio de Janeiro, Brazil)
(2) Replace some key logical operators by adequate classical equivalents
(Gödel-Gentzen variants).
[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.
by Toniann Pitassi (Department of Computer Science, University of Toronto, Canada)
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)
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.
by Glynn Winskel (BRICS, Aarhaus University, Denmark)
Contributed Papers
by Fernando Náufel do Amaral and Edward Hermann Haeusler (Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro, Brazil)
by Sabine Broda and Luis Damas (Departamento de Ciência dos Computadores, Universidade do Porto, Portugal)
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)
by Marcelo Coniglio and Walter Carnielli (Centro de Lógica, Epistemologia e História da Ciência, Universidade Estadual de Campinas, Brazil)
by Paola D'Aquino (Dipartimento di Matematica, Seconda Università degli Studi di Napoli, Italy)
by Marcelo Finger (Departamento de Ciência da Computação, Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)
by Christian Fermüller (Institut für Computersprachen, Technische Universität Wien, Austria)
by Gerhard Jäger (Zentrum für Allgemeine Sprachwissenschaft, Berlin, Germany)
by Peter Krause (Institut für Maschinelle Sprachverarbeitung, Universität Stuttgart, Germany)
by Ralf Naumann and Anja Latrouite (Seminar für Allgemeine Sprachwissenschaft, Universität Düsseldorf, Germany)
by Andre Nies (Department of Mathematics, The University of Chicago, USA)
by Eugénia Reznik (Institut Supérieur d'Electronique de Paris, France), and
Philippe Curmin (Groupe Cyber Informatique, Paris, France)
by Dieter Spreen (Fachbereich Mathematik, Theoretische Informatik, Universität Siegen, Germany)
by Richard Zemel and Toniann Pitassi (Department of Computer Science, University of Toronto, Canada)
by Irina Virbitskaite (Institute of Informatics Systems, Siberian Division of the Russian Academy of Sciences, Novosibirsk, Russia)
by Claus Zinn (Division of Informatics, University of Edinburgh, Scotland)