Abstracts and Slides

Sergei Artemov
A classical view of constructive semantics
In constructive logic, a sentence is true if it has a proof. This paradigm led to the wellknown Brouwer–Heyting–Kolmogorov (BHK) semantics of proofs, which can be viewed as a means of defining constructive semantics within the framework of classical mathematics. This approach was explicit in Kolmogorov's works and similar ideas were expressed by Gödel, who in the 1930s initiated studies in provability logic in order to find a classical specification of constructive reasoning. Gödel's work was concerned with the propositional case and his project was completed by the logic of proofs in 1995.
In our talk, we extend this analysis to the firstorder case and present a formalization of the firstorder BHK semantics based on recently discovered (jointly with Tatiana Yavorskaya) firstorder logic of proofs. This provides a comprehensive view of the constructive firstorder semantics and offers a resolution of some wellknown problems with the latter.

Lev Beklemishev
Topological semantics of provability logic
Topological semantics of provability logic is wellknown since the work of Harold Simmons and Leo Esakia in the 1970s. The diamond modality can be interpreted as a topological derivative operator acting on a scattered topological space. Although quite natural and complete, this semantics has not been much used in the study of provability logics because of the more convenient Kripke semantics. The situation turns out to be different for the polymodal provability logic GLP that has been applied to prooftheoretic analysis of Peano arithmetic. GLP is known to be incomplete w.r.t. any class of Kripke frames.
We study natural topological models of GLP where modalities correspond to derived set operators on a polytopological space (X; τ_{0}; τ_{1}; …). We call such a space GLPspace if, for all n, topologies τ_{n} are scattered, τ_{n}⊆τ_{n+1}, and d_{n}(A) is open in τ_{n+1}, for any A⊆X. Here d_{n}(A) denotes the set of limit points of A w.r.t. topology τ_{n}. GLPspaces exactly the spaces validating all the axioms of GLP. We show that GLP is complete w.r.t. the class of GLPspaces (joint work with David Gabelaia).
On the other hand, the question of completeness of GLP w.r.t. natural ordinal GLPspaces turns out to be dependent on large cardinal axioms of set theory and various facts on reflecting stationary sets. In particular, by the results of Andreas Blass (1990) it is consistent relative to ZFC that GLP is incomplete. However, under the assumption of large cardinal axioms one can establish at least some partial completeness results. Under the assumption V=L we show that the bimodal fragment of GLP is complete w.r.t. the cardinal ℵ_{ω} taken with the interval topology and the club topology (corresponding to the club filter). It is open if this result can be extended to the language with more than two modalities (under V=L and some natural large cardinal assumptions such as the existence of Π^{1}_{n}indescribable cardinals).

Andreas Blass
Logical justification in distributed authorization
I plan to describe the Distributed Knowledge Authorization Language (DKAL), which is being developed at Microsoft Research. Justification logics play an important role in this project, because distributed agents are expected not only to reason but to convince other agents of the correctness of their assertions. The logical issues involved span a wide range, from ensuring adequate expressiveness for real applications to providing efficient algorithms for determining deducibility. In my talk, I plan to concentrate on matters of formal logic that have arisen in this work. For example, what would remain of a natural deduction system if one cannot introduce and discharge temporary hypotheses?

Samuel Bucheli
A justification logic with common knowledge
(joint work with Roman Kuznets and Thomas Studer)
Justification logics are a family of epistemic logics that originate from the Logic of Proofs and that explicitly include justifications for the agents' knowledge. We develop a multiagent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripkestyle semantics that is similar to Fitting's semantics for the Logic of Proofs LP. Soundness and completeness with respect to this Kripkestyle semantics is shown. As a corollary of the completeness theorem we obtain the finite model property and, in turn, we can use this to obtain decidability. We discuss the relationship of our logic to the multiagent modal logic S4 with common knowledge, especially the open problem of realization and possible approaches. Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.

Laura Crosilla
Operations and sets, constructively
(joint work with Andrea Cantini)
This will be a survey talk on constructive operational set theory.
Constructive set theory à la Myhill–Aczel has been extended by the authors to incorporate a notion of operation. Constructive operational set theory is a constructive and predicative analogue of Beeson's Inuitionistic set theory with rules and of Feferman's Operational set theory. One motivation behind constructive operational set theory is to merge CZF's constructive notion of set with some aspects which are typical of explicit mathematics. In particular, we have nonextensional operations (or rules) alongside extensional constructive sets. Operations are in general partial and a limited form of selfapplication is permitted.
A number of systems of constructive operational set theory have been introduced so far and their proof theoretic strength has been investigated.

Walter Dean
Gödel, Kreisel, and the origin of the Logic of Proofs
In this talk I will trace some antecedents to the development of the Logic of Proofs in the work of Gödel and Kreisel. In 1933 Gödel suggested that no definite sense could be assigned to quantification over all constructive proofs. In 1938, however, he then famously sketched a system similar to LP in which such quantification is allowed. Independently of this, Kreisel (1962, 1965) described a system by which he attempted to directly axiomatize the relationship between formulas and constructive proofs, a variant of which was later shown to be inconsistent by Goodman (1970). I'll discuss how the reasoning which leads to the contradiction in Kreisel's system can be reconstructed in a variant of Fitting's Quantified Logic of Proofs, how this bears on the availability of arithmetical semantics for such systems, and the generality of Constructive Necessitation.

Sebastian Eberhard
Applicative theories for logarithmic complexity classes
Applicative systems are a formalisation of the lambda calculus and form the base theory of Feferman's explicit mathematics. For many linear and polynomial complexity classes corresponding applicative systems have already been developed by authors as Kahle, Oitavem, and Strahm. In contrast to the setting of bounded arithmetic, this setting allows very explicit and straightforward lower bound proofs because no coding of graphs of functions is necessary. We present natural applicative theories for the logarithmic hierarchy, alternating logarithmical time, and logarithmic space. For the first two algebras, we formalize function algebras having concatenation recursion as main principle. For logarithmical space, we formalize an algebra with safe and normal inputs and outputs. This algebra allows to shift small safe inputs to the normal side which is against the safenormal paradigm but helps to describe logarithmical space in an elegant way. The theories corresponding to the mentioned complexity classes all contain the predicates W for normal and V for safe words, and are similar in spirit to Cantini's theory for polytime. t∈V intuitively expresses that t is a stored but not fully accessible content. The interplay between W which formalizes fully accessible content and V allows an easy formulation of induction principles justifying concatenation—and sharply bounded recursion.

Melvin Fitting
Possible world semantics for first order LP
Propositional Justification Logics are modallike logics in which the usual necessity operator is split into a family of more complex terms called justifications. Instead of ܀A one finds t : A, which can be read "t is a justification for A." The structure of t embodies, in a straightforward way, how we come to know A or verify A. Many standard propositional modal logics have justification logic counterparts, where the notion of counterpart has a precise definition via what are called Realization Theorems. One can think of justification logics as explicit versions of modal logics, with conventional modal operators embodying justifications in an implicit way. The first propositional justification logic was LP, the Logic of Proofs, an explicit version of propositional S4. It was introduced by Artemov as part of a project to provide an arithmetic semantics for propositional intuitionistic logic. Since this initial work there has been much study of propositional justification logics. But to reiterate, all this was at the propositional level.
Recently Artemov and Yavorskaya defined a firstorder extension of the logic of proofs, FOLP. The original results on propositional LP were shown to extend to the firstorder case as well. This completed the arithmetic semantics project for intuitionistic logic, but it also introduced a new family of interesting explicit logics to study.
In an earlier article we introduced a possible world semantics for LP, and for a few other propositional justification logics. On the one hand this semantics elaborates the familiar Kripke semantics for modal logics by adding machinery to model the behavior of explicit reasons, and on the other hand it extends, in a direct way, an earlier LP semantics of Mkrtychev. The purpose of the present work is to extend this propositional semantics to a firstorder version. The resulting possible world semantics obeys a monotonicity condition, familiar from propositional modal logics. This is natural because of the intended application to intuitionistic logic. We postpone to future work the study of constant domain versions. The current work is specifically for the firstorder version of LP. Simple modifications adapt the results to several other firstorder logics, and we discuss this briefly too. The work appeared in a Tech Report. The current presentation is much simpler, and hopefully more intuitive.

Yuri Gurevich
What, if anything, can be done in linear time?
(joint work with Carlos Cotrini)
The answer to the title question seems to be "Not much." Even sorting n items takes n times log(n) swaps. 3SAT is NP complete, and propositional linear logic is not even decidable. It turns out, however, that quite a bit can be done in linear time. We start with some useful lineartime algorithm, like parsing. Then we sketch the Gurevich–Neeman lineartime algorithm for the multiple derivability problem (given a list of hypotheses and a list Q of queries, decide which of the queries follow from the hypotheses) for propositional primal infon logic (PPIL). Then we present new results: extensions of PPIL with lineartime multiple derivability problem.

Reinhard Kahle
Induction schemata for classes of computational complexity
In this talk, we discuss induction principles for classes of computational complexity in applicative theories. Starting from the conceptional parallelism of induction and recursion, it is known that we can introduce induction schemata corresponding to several restricted recursion schemata. We look, however, at the question how one can characterize classes of computational complexity and, at the same time, use strong mathematical means to prove properties for functions in these classes. The proposed solution should also help to treat function algebras which result from considering the closure of wellknown algebras under certain additional recursion schemata.

Pierluigi Minari
Labelled sequent calculi for modal logics: getting rid of hidden contractions
We deal with the labelled sequent calculi for modal logic introduced by Sara Negri (2005). In these proof systems the structural rule of contraction is not primitive, and is shown to be height preserving admissible. However, this is due to the fact that a restricted form of contraction is hidden not only in the logical rules governing the truthfunctional connectives (which cannot be avoided), but also in the modal rules. As a consequence, proof search termination is not automatically ensured. Can we get rid of such hidden contractions? This is easily seen to be impossible, e.g., for the labelled sequent calculi for K4 and extensions. We show that, on the contrary, this is possible at least for the basic system K. The result also provides an answer to the related issue of the admissibility of a "singleuse" restriction on the nurule in prefixed tableaus for K.

Isabel Oitavem
The class NP
We give a characterization of NP using a recursion scheme with tier 0 pointers. This extends the Bellantoni–Cook characterization of Ptime and, simultaneously, it is a restriction of a recursiontheoretic characterization of Pspace.

Wolfram Pohlers
Some applications of semiformal systems

Michael Rathjen
The existence property and ordinal analysis
A hallmark of many an intuitionistic theory is the existence property, EP, i.e., if the theory proves an existential statement then there is a provably definable witness for it. However, there are well known exceptions. Full intuitionistic Zermelo–Fraenkel set theory, IZF, formulated with Collection does not have the EP. Beeson in 1985 ask whether any reasonable set theory with collection has the EP. Recently it was shown that there are several well known intuitionistic set theories with Collection which possess the existence property. Intriguingly, proving these results uses the technique of ordinal analysis applied to set theories with exponentiation and powerset.

Anton Setzer
Inductiveinductive definitions
(joint work with Fredrik Forsberg)
Inductive inductive definitions is a concept of forming a set inductively while defining a second set depending on it inductively. Variants of it occur frequently in ordinary mathematics. For instance the typical definition of an ordinal notation system defines a set of ordinals inductively while defining a binary relation (<) inductively. Another example are Conway's surreal numbers. A standard version occurs when defining the syntax of type theory inside type theory. We introduce this concept, look at how to formalise it using finitely many rules, and discuss what is known about its proof theoretic strength.

Valentin Shehtman
On axiomatizing products of some transitive modal logics with S5
There exists a general method of axiomatizing products two of Horntype modal logics—by taking the fusion plus commutation and confluence axioms. However, in many cases this does not work—for example, for products of logics above GL or Grz. We propose a solution of the problem in some of these cases by identifying a special extra axiom (an analogue of Fine–Jankov formula for a twoelement frame) and by proving the local tabularity (an analogue of Segerberg's theorem on transitive logics of finite depth).

Tatiana Yavorskaya
Arithmetical semantics for the first order logic of proofs
(joint work with Sergei Artemov)
This talk is about the first order version of Artemov's logic of proofs LP. The firstorder logic of proofs FOLP (S. Artemov, T. Yavorskaya, 2011) is proven to realize firstorder modal logic S4 and, therefore, the firstorder intuitionistic logic. The subject of my talk is arithmetical interpretation of FOLP in terms of arithmetical proofs with parameters; in combination with the realizability result, this provides a semantics of explicit proofs for firstorder S4 and intuitionistic logic compliant with Brouwer–Heyting–Kolmogorov requirements.