Collegium Logicum: proofs and structures
Paris, November 8-10 2010
Room 1C18 (first floor, part C)
175, rue Chevaleret, Paris
Metro Chevaleret, line 6
Supported by: Kurt Gödel Society
Organized by: Matthias Baaz, Stefan Hetzl, Michel Parigot
Talks
Programme
Venue
Talks :
Programme:
Monday, November 8
Tuesday, November 9
Wednesday, November 10
Abstracts:
Matthias Baaz: The epsilon-calculus in non-classical logics (joint work with Richard Zach)
Abstract: We demonstrate that the epsilon theorems are usually false for nonclassical
logics as the critical formulas induce all classically valid quantifier
shift laws. The epsilon theorems are however valid for proofs with certain
predicativity restrictions in presence of the schema of lineariy..
Kaustuv Chaudhuri: Towards a negative existential using epsilon terms
Abstract: .
Consider this statement: there is a Parisian syndicate such that, if
it calls for a strike, then every Parisian syndicate calls for a
strike. It is provable in Gentzen's LK, but it requires an appeal to
contraction. However, it can also be "proved" as follows: the outer
existential distributes over the implication, then is eliminated in
the succedent because the quantified variable isn't free, and the
resulting rewritten formula is, essentially, (A or not A). Many
theorem proving systems perform this kind of _miniscoping_ of
quantifiers to reduce the search space.
In this talk, I will consider the question of an intensional
proof-theoretic treatment of existentials that has similar properties.
This is a work in progress, but the gist is: the contraction-free
existential rule in one-sided LK is invertible---that is, the
existential has negative polarity---if we use Hilbert's epsilon terms
as witnesses. The price is that initial sequents are no longer
axiomatic. Indeed, the premises of initial sequents are the residual
obligations of providing actual terms to replace the epsilon terms. I
will discuss one design for these initial sequents that has some
interesting search properties.
Olivier Danvy: From reduction-based to reduction-free evaluation
Thomas Ehrhard: Differential linear logic and its models
Oliver Fasching: Gödel logics with unary operators acting on truth values
Abstract: .
We consider extensions of [0,1]-Gödel logic by a
unary operator $o$ under two different semantics.
When we require $I(o(A))=min\{1,r+I(A)\}$, $r$ fixed,
we show that the formulas of propositional logic
valid for all $r$ are finitely axiomatizable by a Hilbert-Frege system
although entailment in this logic is not compact.
We prove that the corresponding first-order logic is
not r.e. by adapting Scarpellini's result on Lukasiewicz
logic. When we require $I(o(A))=f(I(A))$, where
$f\colon$ $[0,1] \to [0,1]$ such that $f(1)=1,$ $x \le f(x)$ and
$x < y \supset (f(x) < f(y) \vee f(y)=1)$, we can show
similar results. In both variants, a modal logic like
axiom $o(A \supset B) \leftrightarrow (o A \supset o B)$
occurs.
Tom Gundersen: Breaking Paths in Atomic Flows for Classical Logic
Abstract:
This work belongs to a wider effort aimed at eliminating syntactic
bureaucracy from proof systems. In this paper, we present a novel cut
elimination procedure for classical propositional logic. It is based
on the recently introduced `atomic flows': they are purely graphical
devices that abstract away from much of the typical bureaucracy of
proofs. We make crucial use of the `path breaker', an atomic flow
construction that avoids some nasty termination problems, and that can
be used in any proof system with sufficient symmetry. This paper
contains an original 2-dimensional-diagram exposition of atomic flows,
which helps us to connect atomic flows with other known formalisms.
.
Hugo Herbelin: Intuitionistically proving Markov's principle using exceptions
Abstract:
It has been shown by Kreisel that Markov's principle is not provable
in ordinary intuitionistic logic but proved by Friedman and Dragalin
that it is admissible as a rule.
Markov's principle is realisable by unbounded search for Kleene's
realisability and by the identity function for Gödel's functional
interpretation. We show that it also has a direct computational
content as a constructive proof by interpreting it as a mechanism of
exceptions. Several flavours are possible: call-by-name or
call-by-value, statically-scoped (like longjump in C) or
dynamically-scoped (like the standard exceptions of the programming
languages C++, Java or ML are). The call-by-name statically-scoped can
be seen as a "direct style" computational interpretation of
Coquand-Hofmann's extension of Friedman-Dragalin's admissibility
proof, in the same way as control operators computationally interpret
in "direct style" the double-negation translations of classical logic
to intuitionistic logic.
As a consequence, we can freely extend intuitionistic logic with
Markov's principle and still get a logic for which witnesses of
existential statements are extractable by proof
computation.
Our investigation is carried through in predicate logic where the
natural formulation of Markov's principle is ¬¬A → A for A
hereditarily positive (no implication and no universal
quantification).
Miki Hermann: How To Assign Papers To Referees
Abstract:
The problem to assign papers to referees gained a considerable
interest in the recent years, especially in the scope of conference
management systems. These systems need to achieve a fair and balanced
distribution of papers among referees, where the conditions of
fairness and balance may be defined in several ways. We present two
algorithms to distribute a possibly large number of papers among a
smaller number of referees, each paper requiring k reports. The first
one is an approximation algorithm, using an iteration of weighted
maximum matching in bipartite graphs. The second one is an exact
algorithm based on b-matching. The optimality criterion for the
assignment is not based on a local view of each referee, but on a
global performance of the whole k-assignment satisfying a fairness
criterion. We introduce an objective function for the k-assignment
problem ensuring a specific notion of fairness when it is maximized.
We show how a few precisely defined fairness criteria can be achieved
that way. This includes a particularly notable extension of
rank-maximality, a notion introduced by Irving et al. Our algorithm
computes in polynomial time optimal k-assignments with respect to the
aforementioned fairness function.
Stefan Hetzl: On the Structure of Herbrand-Disjunctions
Abstract:
Herbrand-disjunctions correspond closely to cut-free proofs. A proof with cuts
can therefore be viewed as a compressed representation of an Herbrand-
disjunction with cut-elimination being the decompression mechanism. This talk
will be about the question which Herbrand-disjunctions can be obtained from a
proof with cuts in this way and which cannot. While it is obvious that, for
resulting from a proof with cuts, it is necessary that the Herbrand-
disjunction contains some kind of regularity, it is not clear what kind of
regularity that is. I shall present some results (and work in progress)
towards a combinatorial charaterization of the structure of Herbrand-
disjunctions arising from cut-elimination.
Rosalie Iemhof: Unification in nonclassical theories
Abstract:There are many problems in mathematics that can be cast in terms of unification, meaning that a solution of the problem is a substitution that identifies two terms, either literally, or against a background theory of equivalence.
In the context of logics, unification becomes the study of unifiers, which are the substitutions under which a formula becomes true in the logic.
In many classical theories, all unifiable formulas have a most general unifier, which is a unifier that generates all other unifiers of a formula, but nonclassical theories in general do not have this useful property.
In this talk I will discuss unification in modal and intermediate logics and fragments thereof.
Ulrich Kohlenbach: Proof Mining and Nonlinear Ergodic Theorems
Abstract:
Recent work in the "proof mining" program of extracting effective uniform
bounds from proofs in nonlinear analysis has started to address proofs that
are based on uses of weak sequential compactness in Hilbert space in an
abstract setting without any use of separability.
In this talk we extract from such proofs
1) an explicit uniform rate of metastability (in the sense of T. Tao)
for a theorem due R. Wittmann on the strong convergence of Halpern
iterations of nonexpansive mappings in Hilbert space. In the linear
case these iterations coincide with the ergodic averages and so
Wittmann's theorem is an important nonlinear extension of the
von Neumann Mean Ergodic Theorem.
2) a uniform rate of metastability for J.B. Baillon's famous nonlinear
ergodic theorem in Hilbert space. This time the theorem states
only the weak convergence of the ergodic averages as strong convergence
in general fails in the absence of linearity.
Jean-Louis Krivine: New models of ZF
Abstract:
There are essentially two methods to build models of ZF and
to get relative consistency results in set theory:
constructibility (more generally inner models) and forcing.
Now, the technology of classical realizability gives completely
different models of set theory: for instance, the integers are changed.
We can get, in this way, the consistency of ZF + DC +
some strange properties of R, which cannot be obtained by forcing.
Alexander Leitsch: CERES in higher-order logic
Abstract:
We define a generalization ${\rm CERES}^\omega$ of the first-order
cut-elimination method CERES to higher-order logic. At the core of
${\rm CERES}^\omega$ lies the computation of an (unsatisfiable) set
of sequents ${\it CL}(\pi)$ (the {\em characteristic sequent set})
from a proof $\pi$ of a sequent $S$. A refutation of ${\it CL}(\pi)$
in a higher-order resolution calculus can be used to transform
cut-free parts of $\pi$ (the so-called {\em proof projections}) into
a cut-free proof of $S$. We illustrate the method by an example and
show that ${\rm CERES}^\omega$ is capable of producing meaningful
cut-free proofs in mathematics that traditional cut-elimination
methods cannot reach.
Richard McKinley: Herbrand Nets
Abstract:
Herbrand's theorem can be seen as a statement about the completeness
of a certain proof system for first-order logic. In this talk, I will
show how to regard this as an analytic proof system with a notion of
cut and cut elimination.
Michel Parigot: A very natural deduction
Abstract:
Having a Natural Deduction system where the rules for disjunction are simply the dual of the rules for conjunction, is an old dream of structural proof theorists. We show that the Open Deduction formalism for Deep Inference provides a way of constructing such a system.
Lutz Strassburger: Proof Nets, Atomic Flows, and Correctness Criteria
Abstract:
In this talk I will discuss some problems of current versions of proof nets and atomic flows for classical logic.
Daniel Weller: On the complexity of proof deskolemization (with M. Baaz and S.
Hetzl)
Abstract:
We consider the following problem: Given a proof of the
Skolemization of a formula F, what is the length of the shortest proof of
F? For the restriction of this question to cut-free proofs we prove
corresponding exponential upper and lower bounds. We also consider a more
efficient Skolemization and show a non-elementary lower bound.