Titles and Abstracts

Miloš Adžić: Gödel on the absolute proof and the logic of concepts

Abstract: TBA

Federico Aschieri: On Classical Natural Deduction: Reduction Rules, Strong Normalization, Herbrand's Theorem

Abstract: The goal of this talk is to endow classical first-order natural deduction with a natural set of reduction rules that also allows a natural proof of Herbrand's Theorem. Instead of using the double negation elimination principle as primitive axiom, the law of the excluded middle will be used. Treating the excluded middle as primitive, rather than deriving it from the double negation elimination, has a key consequence: classical proofs can be described as programs that make hypotheses, test and correct them when they are learned to be wrong. As a corollary, one obtains a simple and meaningful computational interpretation of classical logic.

Kosta Došen: Adjunction and Normalization in Categories of Logic

Abstract: Logic inspired by category theory is usually given by "the logic of a category", which is tied to the subobjects in a category of mathematical objects. In categorial proof theory we deal instead with "the category of a logic", where the objects are logical formulae and the arrows are deductions. Logical constants are tied to operations on arrows given by functors. These deductive categories, which are of kinds found important for category theory and mathematics independently of logic, are interesting when they are not preorders, i.e. when it is not the case that there is at most one arrow with the same source and the same target; in other words, when there can be more than one deduction with the same premise and the same conclusion. The same requirement is implied by the BHK interpretation of intuitionistic logic, though it is usually not explicitly mentioned.
Lawvere's characterization of intuitionistic logical constants through adjoint functors, which has a central place in categorial proof theory, is closely related to normalization of deductions in the style of Gentzen and Prawitz. This relationship with one of the central notions of category theory, and of mathematics in general, sheds much light on normalization. Classical deductive logic can also be understood in an interesting way in terms of categorial proof theory, but for it the relationship with adjunction is not to be found to the same extent.

Roy Dyckhoff: TBC

Abstract: TBA

Nissim Francez: On distinguishing proof-theoretic consequence from derivability


Norbert Gratzl & Eugenio Orlandelli: Harmony, Logicality, and Double-line Rules

Abstract: The inversion principle, and the related notion of harmony, has been extensively discussed in proof-theoretic semantics at least since (Prawitz, 1965). In our paper we make use of multi-conclusion sequent-style calculi to provide a harmonious proof-theoretic analysis of modal logics, and we concentrate on Standard Deontic Logic (SDL) as a running example. Our approach is based on combining display calculi (DSDL) with Došen's characterization of logicality in purely structural terms. We present a genuinely new double-line version of DSDL, i.e. DdlSDL, and we show that DSDL and DdlSDL are deductively equivalent. This equivalence allows us to show that the rules of DSDL are harmonious: the left introduction rules are inverse of the right one inasmuch as they are deductively equivalent to the bottom-up elimination rule of DdlSDL.

Guilio Guerrieri & Alberto Naibo: Postponement of RAA and a new form of Glivenko's theorem

Abstract: In the mid-Eighties, Seldin established a normalization strategy for classical logic, which can be considered as a kind of "dual" of the standard normalization strategy given by Prawitz in the mid-Sixties: if a sequent Γ ⊢ A is derivable in NK ∖ {∀i}, then there exists a derivation π in NK ∖ {∀i} using at most one instance of the reductio ad absurdum rule – namely, the last one – and where the remaining part of π corresponds to a derivation π in NJ ∖ {∀i}. We give here a new and simpler proof of Seldin’s result showing that if π is →i-free, then the derivation π' is in NM ∖ {∀i}. As a consequence, we prove a strengthened and more general form of Glivenko’s theorem embedding first-order classical logic not only into the fragment {¬, ∧, ∨, ⊥, →, ∃} of intutionistic logic, but also into the fragment {¬, ∧, ∨, ⊥, ∃} of minimal logic.

Danko Ilik: High-school sequent calculus and an intuitionistic formula hierarchy preserving identity of proofs

Abstract: We propose to revisit intuitionistic proof systems from the point of view of formula isomorphism and high-school identities. We first isolate a fragment of the intuitionistic propositional sequent calculus (LJ), which we name high-school sequent calculus (HS), such that any proof of LJ can be mapped to one in HS that does not use invertible proof rules. This defines one precise criterion for identity of proofs, a problem open since the early days of intuitionistic proof theory. Second, we extend HS for first-order quantifiers and show how it gives rise to an arithmetical hierarchy for intuitionistic logic. An even neater hierarchy can be obtained if one allows higher types and the intuitionistic axiom of choice.

Reinhard Kahle: Is there a "Hilbert thesis"?

Abstract: In his introductory paper to first-order logic, Jon Barwise writes in the Handbook of Mathematical Logic (1977):

... the informal notion of provable used in mathematics is made precise by the formal notion provable in first-order logic. Following a sug[g]estion of Martin Davis, we refer to this view as Hilbert's Thesis.

The relation of informal and formal notion(s) of proof is currently under discussion due to the challenges which modern computer provers issue to mathematics, and one can assume that some kind of "Hilbert's Thesis" is widely accepted by the scientific community.
In the first part of our talk we discuss the nature of the thesis advocated by Barwise (including its attribution to Hilbert). We will compare it, in particular, with Church's Thesis about computability. While Church's Thesis refers to one particular model of computation, Hilbert's Thesis is open to arbitrary axiomatic implementations. We will draw some first conclusions from this difference, in particular, concerning the question, how a "Hilbert thesis" could be formulated more specifically.
Church's Thesis receives some evidence from the fact that it blocks any diagonalization argument by the use of partial functions. In the second part of the talk, we pose the question whether there could be something like a partial proof, giving a formal counterpart to a partial function. The relation would arise from an extension of the Curry-Howard isomorphism to untyped λ terms. In this perspective, the question fits squarely in the tradition of General Proof Theory.

Angeliki Koutsoukou-Argyraki: New Applications of Proof Mining to Nonlinear Analysis

Abstract: Proof mining is a research program in applied proof theory, originally introduced by Kreisel in the 1950's under the name "Unwinding of Proofs", that involves the extraction of new quantitative, constructive information by logical analysis of mathematical proofs that appear to be nonconstructive. The information is "hidden" behind an implicit use of quantifiers in the proof, and its extraction is guaranteed by certain logical metatheorems, if the statement proved is of a certain logical form. In this talk we will very briefly present two recent applications of proof mining to nonlinear analysis, both involving the study of one-parameter nonexpansive semigroups. Both papers are joint work with Ulrich Kohlenbach; the first work is also the first application of proof mining to the theory of partial differential equations; the second is another contribution of proof mining to fixed point theory.

Paolo Maffezioli, Mario Piazza & Gabriele Pulcini: On the maximality of classical logic


Per Martin-Löf: TBA

Abstract: TBA

Luiz Carlos Pereira: TBA

Abstract: TBA

Clayton Peterson: Monoidal logics: De Morgan negations and classical systems

Abstract: TBA

Zoran Petrić: The natural deduction normal form and coherence

Abstract: Coherence results serve to describe the canonical arrows of categories of a particular kind. Some of these results are obtained by using proof-theoretical techniques, in particular Gentzen's cut elimination. The aim of this talk is to show how the expanded normal form of natural deduction derivations is useful for coherence proofs.

Dag Prawitz: TBA

Abstract: TBA

Heinrich Wansing: TBA

Abstract: TBA