In constructive logic, a sentence is true if it has a proof. This paradigm led to the well-known 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 first-order case and present a formalization of the first-order BHK semantics based on recently discovered (jointly with Tatiana Yavorskaya) first-order logic of proofs. This provides a comprehensive view of the constructive first-order semantics and offers a resolution of some well-known problems with the latter.

[Slides]

Topological semantics of provability logic is well-known 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 proof-theoretic 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 poly-topological space (X; τ₀; τ₁; …). We call such a space GLP-space 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. GLP-spaces exactly the spaces validating all the axioms of GLP. We show that GLP is complete w.r.t. the class of GLP-spaces (joint work with David Gabelaia).

On the other hand, the question of completeness of GLP w.r.t. natural ordinal GLP-spaces 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  Π¹_n-indescribable cardinals).

[Slides]

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?

[Slides]

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 multi-agent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripke-style semantics that is similar to Fitting's semantics for the Logic of Proofs LP. Soundness and completeness with respect to this Kripke-style 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 multi-agent 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.

[Slides]

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 non-extensional operations (or rules) alongside extensional constructive sets. Operations are in general partial and a limited form of self-application is permitted.

A number of systems of constructive operational set theory have been introduced so far and their proof theoretic strength has been investigated.

[Slides]

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.

[Slides]

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 safe-normal 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.

[Slides]

Propositional Justification Logics are modal-like 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 first-order extension of the logic of proofs, FOLP. The original results on propositional LP were shown to extend to the first-order 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 first-order 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 first-order version of LP. Simple modifications adapt the results to several other first-order logics, and we discuss this briefly too. The work appeared in a Tech Report. The current presentation is much simpler, and hopefully more intuitive.

[Slides]

The answer to the title question seems to be "Not much." Even sorting n items takes n times log(n) swaps. 3-SAT 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 linear-time algorithm, like parsing. Then we sketch the Gurevich–Neeman linear-time 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 linear-time multiple derivability problem.

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 well-known algebras under certain additional recursion schemata.

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 truth-functional 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 "single-use" restriction on the nu-rule in prefixed tableaus for K.

[Slides]

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 recursion-theoretic characterization of Pspace.

[Slides]

[Slides]

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.

[Slides]

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.

[Slides]

There exists a general method of axiomatizing products two of Horn-type 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 two-element frame) and by proving the local tabularity (an analogue of Segerberg's theorem on transitive logics of finite depth).

This talk is about the first order version of Artemov's logic of proofs LP. The first-order logic of proofs FOLP (S. Artemov, T. Yavorskaya, 2011) is proven to realize first-order modal logic S4 and, therefore, the first-order 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 first-order S4 and intuitionistic logic compliant with Brouwer–Heyting–Kolmogorov requirements.

[Slides]