Arnon Avron

Weyl’s “Das Kontinuum” 100 years later

Abstract:  Hermann Weyl was one of the greatest mathematicians of the 20th century, with contributions to many branches of mathematics and physics. In 1918 he wrote a famous book, “Das Kontinuum”, on the foundations of mathematics. In that book he described mathematical analysis (as it is still conceived today) as a “house built on sand” and tried to “replace this shifting foundation with pillars of enduring strength”. However, these pillars were not intended to “support everything which today is generally considered to be securely grounded”, and he was willing to give up the rest.
    In this talk I'll explain Weyl’s criticism of the mathematics of Weierstrass, Dirichlet, Dedekind, and Cantor, and the philosophical and mathematical ideas that underlie his own system. Then I provide a precise, completely faithful formalization of Weyl’s system in “Das Kontinuum”. Finally, I show that certain set-theoretical (type-free) systems, which are formulated in the usual language that mathematicians nowadays employ, reflect much better (at least in my opinion) Weyl’s ideas than the previous attempts (most notably by Feferman) to give it a modern form.

Matthias Baaz

On the benefit of unsound rules

Abstract:  In this lecture we present relaxed eigenvariable conditions. These eigenvariable conditions lead to a globally sound concept of proof, which may lack local soundeness, there may exist unsound subproofs. (This implies that soundness cannot be proven by induction on the steps of the proof.) As a consequence we show that minimal cut-free proofs my be non-elementary shorter in the new format than in the old format using the sequence of proofs introduced by Orevkov to proof that cut-elimination is non-elementary. Further we show that the use of Andrew’s Skolemization might lead to non-elemenatarily shorter resolution refutations that the usual Skolemization in resolution theorem proving.

Lev Beklemishev

Strictly positive provability logics: a survey

Abstract:  We deal with the fragment of propositional modal logic consisting of implications of formulas built up from the variables and the constant “true” by conjunction and diamonds only. We call such fragments strictly positive. Strictly positive logics recently attracted attention both in the description logic and in the provability logic communities for their combination of efficiency and sufficient expressivity. Moreover, strictly positive logics allow for alternative interpretations that are quite natural from a proof-theoretic point of view. We will present recent results and remaining open questions in this area.

Sam Buss

CDCL solvers, resolution, extension and DRAT proofs ¹

Abstract:  Modern propositional satisfiability solvers (SAT solvers) are remarkable successful, able to solve instances of satisfiability with 100 000’s of variables, or even millions of variables. This is due largely to the success of conflict driven clause learning. This talk will discuss the logical foundations of CDCL solvers and their connections to resolution. The DRAT proof system has been introduced as a proof system for verifying the correctness of CDCL refutations. The DRAT proof system is surprisingly powerful in that it simulates extended resolution. We introduce a stronger form of DRAT proofs, called Substitution Propagation. We discuss upper and lower bounds on the length of Substitution Propagation and DRAT proofs when they are not allowed to introduce new variables.

¹Joint work with Neil Thapen.

Melvin Fitting

The family of strict/tolerant logics

Abstract:  Strict/tolerant logic (not due to me) is a semantically defined 3 valued logic that has the same consequence relation as classical logic, though it differs from classical logic at the metaconsequence level. Specifically, it does not satisfy a local cut rule.   It has been used to call into question the identification of logics having the same consequence relations. That is not my immediate concern, though. Further, it has been recommended for use in work on theories of truth because it avoids some objectionable features arising from the application of classical logic. It also has clear uses in addressing vagueness issues.
    My interests are not in applications, but in the formal structures involved. I have been able to show that a wide range of many-valued logics have strict/tolerant counterparts, with the same consequence relations but differing at the metaconsequence level. Among these logics are Kleene’s \(K3\), Priest’s \(LP\), and first degree entailment, FDE. I have further shown that a broad range of many/valued modal and quantified logics likewise have strict/tolerant counterparts. So, this is not a rare phenomenon but a surprisingly common one.
    The primary tool used in my extensions of the strict/tolerant idea is the bilattice. But it is more than a tool, it seems to be the natural home for this kind of investigation. Questions remain about possible connections between this work and my work from many years ago generalizing Kripke’s fixed point theory of truth. This remains for the future.

Olga Kosheleva & Vladik Kreinovich

Orevkov, Khalfin, and quantum field theory: How constructive mathematics can help physics

Abstract:  After Vladimir Orevkov published his early-1970s paper on constructive complex analysis, Leonid Khalfin, his LOMI colleague interested in physics applications, expressed a hope that constructive mathematics can help resolve the following physics problem. Starting with Bogolybov, many researchers working in quantum field theory and in solid state theory use “macro” analyticity — mostly, the contour integrals — to compute the corresponding values of physical quantities. This“macro” analyticity has been confirmed by many experiments and makes perfect physical sense. However, in traditional mathematics, such “macro” analyticity is equivalent to “micro” one — that the corresponding dependencies can be expanded in Taylor series. In the opinion of physicists, this “micro” analyticity does not make direct physical sense — since on the micro level, quantum uncertainty makes exact measurements impossible. From this viewpoint, it is desirable to come up with a model in which physically meaningful macro analyticity is present, but physically meaningless micro analyticity is not.
    Khalfin hoped that this "thornless rose" effect can be achieved if we consider constructive mathematics instead of the traditional one. In the early 1970s, this hope did not materialize, since, as Errett Bishop has shown in his 1967 book (and as Vladimir Lifschitz pointed to Khalfin), the fact that macro analyticity implies micro one can be proven in constructive mathematics as well.
    Bishop's derivation is based on the traditional constructive mathematics, where existence of an object means, in effect, the existence of an algorithm producing more and more accurate approximations to this object — irrespective to how long this algorithm may take. What if we consider a more realistic version of constructive mathematics, in which only feasible (=polynomial-time) algorithms are allowed? It turns out that in this case, Khalfin’s dream can be materialized: indeed, while there exists a known algorithm computing, for each computable macro analytical function, all the terms in its Taylor series expansion, the computation time of this algorithm grows exponentially with the number n of the term.
    This result will probably be of interest to theoreticians like Khalfin interested to provide physical theories with physically meaningful mathematical foundations. This result may also have practical applications if we take into account that many times when we encountered a physical process whose properties are difficult to compute, it became possible to use this process to speed up computations. Successes of quantum computing are the latest example of this phenomenon. From this viewpoint, maybe measurement of the corresponding Taylor coefficients can lead to yet another efficient quantum computing scheme?

Vladimir Lifschitz

On the relationship between stable models and program completion ²

Abstract:  We generalize a theorem by Francois Fages that relates stable models of a logic program to models of its completion.

²Joint work with Jorge Fandinno.

Alexei Semenov

Definability theory. New trends and open problems ³

Abstract:  Definition belongs to the basic concepts of mathematical logic (and of mathematics) not less important as concepts of truth, proof and computation. This notion was considered as central in the very first works of logicians of XIX century.
    Tarski and Buchi were surprised by the fact that definability theory is a road much “less traveled” than other areas of our science. We consider as the main goal of our talk to attract our community attention to the subject and to start joint construction of a list of Open Problems of Definability Theory.
    The basic notion here is “a relation \(R\) can be defined through relations of a set \(S\) in a language \(L\)”. Let us fix a universe \(U\) and a language \(L\), say, first-order relational language (predicate without functional symbols). So, we have closed (under definability) sets of relations on \(U\) — definability spaces. These spaces constitute the definability lattice in a natural way. Starting with a given structure we consider the definability space of it and the definability lattice of its subspaces (called also reducts of the original structure). In the case of \(\omega\)-categorical structure the definability lattice of it is (anti)isomorphic to the lattice of closed supergroups of automorphism group of the original structure. It makes a nice “geometric” (in the sense of Felix Klein) framework for study. The simplest interesting structure here is the order of rational numbers. Claude Frasnay described in 1965 its definability lattice of 5 elements (those were discovered by Edward Huntington in 1935). More results were obtained in the following decades (references will be given in the talk), such as: isomorphic 5 element lattices are constituted by definability of the random graph, the random tournament, the random digraph. Not to make arithmetic here boring it appears that for ordered random graph the lattice is constituted by 44 elements and the lattice of rational order with 0 added has 116 elements.
    The number 1 in the List of Open Problems in Definability Theory can be assigned to proving Thomas Conjecture: Definability lattice of every finitely generated homogeneous structure is finite.
    Svenonius theorem of 1958 permits us to extend the “geometry of logic” study to any countable structure by adding “imaginaries” to it. Surprisingly much less is known up to now in the general (not \(\omega\)-categorical) case. The authors described infinite lattices of definability for integers with successor and additive group of rationals. Our approach exploits a class of structures that we call upper complete. For these structures we have the same anti isomorphism mapping as for \(\omega\)-categorical ones. The “geometrical” approach cannot be immediately extended to all structures, but we provide a version of it based on a different “Svenonius geometry”.
    And again — all this is primarily oriented to jointly posing and discussing Open Problems for future research.

³Joint work with Sergei Soprunov.

Helmut Schwichtenberg

Logic for exact real arithmetic

Abstract:  Continuing earlier work with U. Berger, K. Miyamoto and H. Tsuiki, it is shown how a division algorithm for real numbers given as a stream of signed digits can be extracted from an appropriate formal proof. The property of being a real number represented as a stream is formulated by means of coinductively defined predicates, and formal proofs involve coinduction. The proof assistant Minlog is used to generate the formal proofs and extract their computational content as terms of the underlying theory, a form of type theory for finite or infinite data. Some experiments with running the extracted term are described, after its translation to Haskell.
    Research leading to this work has benefited considerably from Vladimir Orevkov’s analysis of the complexity of normalization of typed \(\lambda\) terms with constants.

Daniyar Shamkanov

On algebraic and neighbourhood semantics of the modal logic of transitive closure

Abstract:  While various types of completions for Boolean algebras with operators have been thoroughly studied, we know little about the case of fixed-point Boolean algebras. In this talk, we consider the modal logic of transitive closure \(K+\), which is a member of the family of fixed-point logics, and identify the class of \(K+\)-algebras that can be embedded into complete algebras of the given variety. For such algebras called standard, we establish a Stone-type representation theorem and, in this way, provide any standard algebra with an explicit completion. Additionally, since the Lindenbaum-Tarski algebra of \(K+\) is standard, this representation result gives us a canonical neighbourhood frame construction for this fixed-point logic.

Anatol Slissenko

What is “There exists”?

Abstract:  The talk is a light and short discussion of the meaning of existence in logic and outside. Gödel’s Proof of the Existence of God is also used to illustrate some points.

Sergei Soloviev

Proofs and categories

Abstract:  The talk finds part of its inspiration in opposition (suggested by G. Kreisel) of the Theory of Proofs that studies individual proofs and their structural features and Proof Theory, mostly centered around validity. The contribution of V.P. Orevkov to the Theory of Proofs in this sense was very valuable. To illustrate this point, various applications of the Theory of Proofs to Category Theory (including one joint work with V.P. Orevkov) are considered (categorical equivalences of proofs, coherence problems, triple-dual conjecture etc.) as well as various proof-theoretical approaches and techniques that author learned from V. P. Orevkov and used in his own work.

Stanislav Speranski

A constructive interpretation of independence quantifiers ⁴

Abstract:  In his book “The Principles of Mathematics Revisited”, Jaakko Hintikka discussed independence-friendly first-order logic — IF-FOL for short — and how drastically different the situation in the philosophy of mathematics would be if classical FOL were replaced by IF-FOL. Inspired by Hintikka’s ideas, we are going to constructivize the game-theoretical semantics for IF-FOL, but in a somewhat different way than he did in the book. Along the way, we shall provide a constructive version of the so-called trump semantics for IF-FOL, which was discovered by Wilfrid Hodges. As might be expected, this version will generalize Nelson’s realizability interpretation for the implication-free first-order formulas.

⁴Joint work with Sergei Odintsov and Igor Shevchenko.

Thomas Studer

On the proof theory of modal logics with fixed points

Abstract:  Modal fixed point logics are extensions of modal logics with operators denoting least, respectively greatest, fixed points of certain positive formulas. Logics of this kind include temporal logics, logics of common knowledge, program logics, and most famously, the modal \(\mu\)-calculus. We present a survey of deductive systems for the logic of common knowledge as a typical example of a model fixed point logic. In particular, we present two different Hilbert-style axiomatizations and several infinitary cut-free sequent systems. Further we discuss the problem of syntactic cut-elimination for common knowledge and its generalization to the modal \(\mu\)-calculus.

Andreas Weiermann

Accessible independence results in terms of natural number addition and multiplication ⁵

Abstract:  We consider arithmetical terms built up from the natural number one, addition and multiplication. Via natural constraints we define a relation: term \(s\) is less than or equal to term \(t\) if this holds for \(s\) and \(t\) for immediate reasons. We show that a simple true assertion about this relation leads already to strong independence results. Even when arithmetical terms are considered modulo commutativity or associativity the assertion remains strong. We show that the restriction of the assertion to purely additive terms still leads to an independence result for first order Peano arithmetic. We discuss the situation when additional arithmetical terms enter and we also discuss the effect when the less than or equal to relation under consideration is modified.

⁵Joint work with Harvey M. Friedman.

Junhua Yu

Diagonal/circular extensions of a sequent calculus ⁶

Abstract:  For a sequent calculus \(X\) that enjoys a rule \(R\) that principally introduces positive occurrences of a key-note operator, the diagonal extension of \(X\) is gained via replacing rule \(R\) from \(X\) by rule \(D\), where \(D\) is just like \(R\), but has an extra negative copy of positive principals (from its conclusion) at each of its premises. To the contrast, the circular extension of \(X\) enjoys exact the same axioms and rules as \(X\), but employs instead a generalized notion of proof, called circular proof. In a circular proof, each leaf can either be a given axiom, or has a same sequent as another node on the unique path from that leaf to the root. Daniyar Shamkanov verified that the diagonal extension and the circular extension of a calculus for modal logic \(K4\) coincide in terms of provability (both are calculi for Gödel–Löb provability logic GL). In this talk, we will sketch our finding that this can also be achieved purely in terms of proof transformation, which also allows us to prove a parallel result for Visser’s BPL, where both extensions are calculi for his FPL.

⁶Joint work with Yinqiu Zhu and Xinxian Chen.