Titles and Abstracts
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 & Sara Negri: Idempotent coherentisation for first-order logic
Abstract: Skolem showed in 1920 that, by use of new relation symbols, every first-order sentence is in some sense replaceable by a single ∀∃-sentence; the precise sense can easily be seen as the construction of something slightly stronger than a conservative extension. A variation on the argument shows that the new sentence can be ensured to be a finite conjunction of "special coherent implications", i.e. sentences that are universally quantified implications with, as antecedent, a conjunction of atoms and, as succedent, a positive formula, i.e. wlog a disjunction of existentially quantified conjunctions of atoms. [Such sentences are also called "geometric axioms".] Thus, every first-order theory has a coherent conservative relational extension. We survey some of the history of this folklore result, including what seems to be its first appearance in the unpublished Montréal Master's thesis of Antonius (1975), and present a new coherentisation algorithm with the idempotence property, i.e. there is no use of normal form (e.g. NNF or PNF) and sentences that are [almost] of the right form are left [almost] unchanged. Examples and applications will be presented if time permits. The proof theory of theories axiomatised by sentences of the described form is well-known to be particularly simple (using "dynamical proofs"); the result shows that, modulo some extra relation symbols, all first-order theories are of this form.
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.
Giulio Guerrieri & Alberto Naibo: Postponement of RAA and Glivenko's theorem, revisited
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 intuitionistic 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.
Per Martin-Löf: The two interpretations of natural deduction: how do they fit together?
Abstract: Natural deduction admits of two different interpretations, which it is natural to refer to as the ancient and the modern one. According to the ancient interpretation, which goes back to Aristotle, a natural deduction, or syllogism, in his terminology, is interpreted as a demonstration that the truth of the final proposition follows from the truth of the initial propositions, which is to say, the hypotheses, or assumptions. According to the modern interpretation, a natural deduction is seen as a complex logical object, a proof object, which depends on arbitrary proofs of the assumptions, named by variables, and itself is a proof of the final proposition of the deduction. Conceptual priority is with the modern interpretation. This will be substantiated by showing how the ancient interpretation is derived from the modern interpretation by the special abbreviative device of suppressing proof objects.
Luiz Carlos Pereira: The Russell-Prawitz translation and schematic rules: a view from proof-theory
Clayton Peterson: Monoidal logics: De Morgan negations and classical systems
Abstract: Monoidal logics (cf. Peterson 2014a,b, 2015) assume category theory as a foundation and define logical systems using specific rules and axiom schemata in order to make explicit their categorical (monoidal) structure. Monoidal logics can be compared to substructural logics (cf. Restall 2000) and, more generally, to display logics (cf. Goré 1998). It is possible to define a translation t from the language of monoidal logics to the language of display logics such that a proof φ → ψ is derivable within specific monoidal deductive systems if and only if t(φ) ⊢ t(ψ) is derivable within their respective display counterparts. One upshot of this comparison is that monoidal logics can be proven to be weaker and more flexible than substructural logics. For example, in substructural logics, the elimination of double negation(s) is generally thought to be accompanied by the satisfaction of the de Morgan dualities. In contrast, the elimination of double negation(s) can be proven to be independent from the de Morgan dualities in monoidal logics. In this talk, we show how this result can be understood in light of the relationship between the notions of weak distributivity (a.k.a. linear distributivity) and classical deductive systems.
Extended abstract (including references)
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.
Mario Piazza & Gabriele Pulcini: On the maximality of classical logic
Dag Prawitz: Gentzen's justification of inferences
Helmut Schwichtenberg: Decorating natural deduction
Abstract: Natural deduction provides a perfect link between logic and computation, in its purest form of Church's lambda-calculus: introduction and elimination rules correspond to abstraction and application, and formulas to types. Following Kolmogorov we can view a formula A as a problem, and a constructive proof of A as a solution. Such a solution is a computable function of a certain type determined by A. Computable content arises where the formula A contains inductively defined predicates. The clauses of the inductive definition determine the data type of the solution (or "realizer"). We address the delicate question of how to "decorate" natural deduction proofs in order to optimize their computational content. It is shown that a unique optimal such decoration exists, and some examples are discussed.
Heinrich Wansing: A more general general proof theory
Abstract: In the early 1970s Dag Prawitz introduced general proof theory, now often also called "structural proof theory," as "a study of proofs in their own right where one is interested in general questions about the nature and structure of proofs." (Prawitz 1974, p. 66) At about the same time, Georg Kreisel used the term "theory of proofs."
In this talk I will suggest to broaden Prawitz's understanding of structural proof theory. The idea is to consider in addition to verifications also falsifications, so as to obtain a theory of proofs and dual proofs. I will motivate this more comprehensive view by taking up some remarks Prawitz has made on falsificationist theories of meaning in (Prawitz 2007) and by considering the natural deduction proof systems for Nelson's constructive proposition logic from his dissertation (Prawitz 1965). In that context, I will discuss the notion of co-implication within Heyting-Brouwer Logic (Rauszer 1980) and the bi-intuitionistic logic 2Int from (Wansing 2013, 2015).
References:
- Dag Prawitz, Natural Deduction. A Proof-theoretical Study, Almqvist and Wiksell, Stockholm, 1965.
- Dag Prawitz, "On the idea of a general proof theory", Synthese 27 (1974), 63-77.
- Dag Prawitz, "Pragmatist and verificationist theories of meaning", in: R.E. Auxier and L.E. Hahn (eds), The Philosophy of Michael Dummett, Open Court, Chicago, 2007, 455-481.
- Cecylia Rauszer, "An algebraic and Kripke-style approach to a certain extension of intuitionistic logic", Dissertationes Mathematicae 167, Institute of Mathematics, Polish Academy of Sciences, Warsaw 1980, 62 pp.
- Heinrich Wansing, "Falsification, natural deduction and bi-intuitionistic logic", Journal of Logic and Computation, doi: 10.1093/logcom/ext035, first published online: July 17, 2013.
- Heinrich Wansing, 2015, "On split negation, strong negation, information, falsification, and verification", to appear in: K. Bimbó (ed.), J. Michael Dunn on Information Based Logics, Outstanding Contributions to Logic Series, Springer.