Schedule Prague Vienna Workshop 2006

Wednesday 11-1-2006 | Thursday 12-1-2006 |

10:00-10:40 Pavel Pudlák | 10:00-10:40 Mathias Baaz |

10:40-11:20 Joost J. Joosten | 10:40-11:20 Arnold Beckmann |

11:20-11:35 Tea and Coffee |
11:20-11:35 Tea and Coffee |

11:35-12:15 Markus Latte | 11:35-12:15 Rosalie Iemhoff |

12:15-14:00 Lunch |
12:15-14:00 Lunch |

14:00-14:40 Alan Skelley | 14:00-14:40 Petr Hájek |

14:40-15:20 Marta Bilkova | 14:40-15:20 George Metcalfe |

15:20-15:40 Tea and Coffee | 15:20-15:40 Tea and Coffee |

15:40-16:20 Vitezslav Svejdar | 15:40-16:20 Evan Goris |

16:20-17:00 Pavel Hrubes | 16:20-17:00 Jan Krajicek |

**COORDINATES** are as follows. The workshop takes place at Zitna 25 on Wednesday January 11 and
Thursday January 12. The conference room shall be indicated with signs to find it. If you are at Zitna 25, there is big door which looks like a little "archway". You can recognize this by the flowershop on the lefthand side. You go through the archway across the courtyard and the institute is through the glass doors at the end.

To find your way around in Prague it is very good to use www.mapy.cz.

**SOCIAL EVENTS** will comprise a dinner party and possibly something else. The dinner party will
be on thursday January 12 at Pivovarsky Dum
starting at 18:30. We are thinking of ordering a GOOSE for dinner. Those who want to participate in
the goose should contact Joost J. Joosten (jjoosten "include here at" phil.uu.nl) know asap, as the goose has to be
ordered and specially prepared in advance.

Wednesday 11-1-2006

10:00-10:40 Speaker: Pavel Pudlák; Title: On search problems and \forall\Sigma_1^b theorems of bounded arithmetic

Abstract: \forall\Sigma_1^b theorems can be viewed as total search problems (total = every instance is solvable). Search problems have been studied in computational complexity theory and the corresponding theorems in bounded arithmetic. The problems of characterizing such consequences of bounded arithmetic and proving that they form an increasing hierarchy are among the most interesting open problems in bounded arithmetic. Solving these problems may help us also classify (exponential) algorithms for solving search problems.

I shall discuss some attempts to solve these two problems.

10:40-11:20 Speaker: Joost J. Joosten; Title: Large objects in modal logics

Abstract: The main topic of this talk will be on things related to lower bounds for PSPACE complete modal logics. Together with Pavel Hrubes and Pavel Pudlák we have had some brainstorm session over the last two months. I shall communicate on our findings. The work is still very much in process and I shall present hardly any theorems. In particular we still have no strategy that seems promising for obtaining lower bounds. If time allows, I shall briefly mention some results I have obtained on optimal proof systems, a topic not related to the title of this talk.

11:35-12:15 Speaker: Markus Latte; Title: On a method towards a lower bound for intuitionistic logic

Abstract: Normalization is an essential tool for analyzing proofs in natural

deduction style. We combine this technique with the well known

superpolynomial lower bound for the size of a monotone circuit

deciding the k-clique problem. For this purpose we construct

a sequence of formulas. Any normal derivation of anyone of them

specifies a monotone circuit for the clique problem. To assign

a circuit to a such derivation we consider the normalization process

in reverse order. This process allows us to backtrack essential

information visible in the normal form back to an arbitrary

derivation. Finally we show how a small monotone circuit for the

clique problem can be extracted from derivations satisfying some

technical conditions.

14:00-14:40 Speaker: Alan Skelley; Title: Third-order computation and bounded arithmetic, and strong propositional proof systems

Abstract: Several authors have used higher-order theories of bounded arithmetic as a more elegant way of reasoning about some complexity classes. I will discuss one way to extend this to PSPACE and classes from the EXP-time hierarchy, and a reasonable generalization of ordinary computation that fits in nicely. I will then talk about some strong propositional proof systems designed to translate these theories.

14:40-15:20 Speaker: Marta Bilkova; Title: Feasible interpolation in modal logic

Abstract: We shall present a simple proof of feasible disjunction property for modal

logics K, T, K4, S4, GL, and S4Grz. The main advantage of the argument

which is based on modal sequent calculi is that it does not require full

cut elimination.

As a corollary we obtain feasible interpolation theorem and discuss its

complexity consequences.

15:40-16:20 Speaker: Vitezslav Svejdar; Title: On Systems with Rosser Symbols

Abstract: We review some properties and aspects of modal

propositional logic with symbols for witness comparison.

16:20-17:00 Speaker: Pavel Hrubes; Title: A propositional system with a non-trivial upper bound on the number of proof-lines

Abstract: We show that in a propositional proof system SFI the number of proof lines

of a tautology A depends only on the number of propositional variables in A and

not on the size of A. In particular, there is a constant c s.t. every tautology

with no propositional variables (i.e., containing only the atoms 0 and 1) has a

SFI-proof with c proof-lines.

Thursday 12-1-2006

10:00-10:40 Speaker: Mathias Baaz; Title: Herbrand's Theorem and Skolem Functions

Abstract: In this lecture we discuss the connection between Herbrand's Theorem and the

admissability of Skolem Functions both for nonclassical logics and nonstandard

classes of skolem functions. We derive for classical logic a correspondence

between admitted properties of Skolem functions and bounds for the length of

the herbrand disjunction.

10:40-11:20 Speaker: Arnold Beckmann; Title: Continuous cut-elimination and bounded arithmetic

Abstract: This will be an informal talk reporting about some

work in progress. Continuous cut-elimination is a method

introduced by Mints into Schuette's infinitary cut-elimination

which allows to extract finitary information from infinitary

proofs. One main use is to extract informations about provable

total functions of theories by infinitary methods. In the talk

we will try to explain how continuous cut-elimination can be

adapted to proof systems related to bounded arithmetic theories.

One application of this is to extract definable functions in

bounded arithmetic.

11:35-12:15 Speaker: Rosalie Iemhoff; Title: Skolemization, existence and equality

Abstract: Like in classical logic, Skolemization is sound and complete for

prenex formulas in intuitionistic logic. This no longer holds for

infix formulas. We define an alternative Skolemization method that

makes use of an existence predicate and that is sound and complete

for a large class of formulas. It even is so in the presence of

equality, for which Skolemization in intuitionistic is not even

sound and complete for implications between prenex formulas. This

is joint work with Matthias Baaz.

14:00-14:40 Speaker: Petr Hájek; Title: On Grzegorczyk’s weak essentially undecidable theory

Abstract: Grzegorczyk has suggested to study the theory (call it Q−) which results from Robinson’s arithmetic Q by replacing the operations of addition and multiplication by ternary predicates A and M and rewriting the axioms postulating only that A and M are possibly partial functions. He conjectured that the theory is essentially undecidable. I sketch a proof of the positive answer.

14:40-15:20 Speaker: George Metcalfe; Title: Proof Systems for Admissibility

Abstract: The admissible rules of a logic are the rules under which a logic is

closed. In classical logic all admissible rules are also derivable, but in

intuitionistic and many other non-classical logics this is not the case.

Sets of rules (called bases) that added to a logic characterize the set of

admissible rules of that logic have been found for intuitionistic and

various modal and intermediate logics. In this talk we introduce

Gentzen-style proof systems for admissiblility in these logics; the key

idea being that we consider collections (called r-hypersequents) of both

sequents and negated sequents.

15:40-16:20 Speaker: Evan Goris; Title: Logic of Proofs

Abstract: Artemov's Logic of Proofs (LP) is a propositional modal logic, syntactically in the spirit of PDL in the sense that it has a recursively generated set of modalities. LP has many applications of which I will discuss two. First LP can be seen as an explicit version of the modal logic S4. Second LP has an arithmetical interpretation in the spirit of provability logic but where Skolem functions for the existential quantifiers (over proof codes) are brought into the modal language. Combing the above gives an arithmetical interpretation to the modal logic S4. Additionally LP is known to be arithmetically complete for a wider range of theories (most notably Buss' S12) than GL.

16:20-17:00 Speaker: Jan Krajicek; Title: Proof complexity and cryptography

Abstract: I shall discuss to which extend it might be

possible to base security of cryptosystems on

proof complexity hardness. It is an application of

proof complexity generators.

Previous postings

**A Preliminary schedule** can be found here.

**VISITORS: HOTEL** arrangements are being taken care of.
In case of questions or changes, contact
Pavel Hrubes.
(pahrubes "include here at" centrum.cz)

**VISITORS: COMPUTER FACILITIES** will consist of using the machines of one of the "locals". It is also
possible to have the Mac or IP address of your laptop registered. Like this, you will have access
with limited permissions with your laptop on the local network. If you want to register your
laptop, send your Mac and/or IP address to Pavel Pudlák (pudlak "include here at" math.cas.cz) asap.

**SPEAKERS:** please send asap title + little abstract to Joost J. Joosten (jjoosten "include here at" phil.uu.nl). We
will schedule 40 minutes per talk including discussion. So, either prepare a 30 or a 35 minutes
presentation.

**ALL: FURTHER INFORMATION** about the workshop will be posted on this page.

Joost Joosten Last modified: Wed Jan 11 00:52:24 MET 2006