December 7, 2016, 16h c.t., Sand 1, A302, Tübingen:
Reinhard Kahle (Lisbon): Hilberts umfassendes Programm

Abstract: David Hilberts Name ist in den Grundlagen der Mathematik unter anderem mit der programmatischen Idee verbunden, Widerspruchsfreiheitsbeweise für formalisierte mathematische Theorien zu führen. Bekanntlich haben die Gödelschen Unvollständigkeitssätze diesem Programm gewisse Grenzen gesetzt, die nur durch Überschreitung des zwischenzeitlich von Hilbert vertretenen finiten Standpunkts überwunden werden können. In diesem Vortrag wollen wir dieses engere Hilbertsche Programm mit seinen ursprünglichen und sehr umfassenden mathematik-philosophischen Anliegen in Verbindung setzen. Dabei läßt sich ein umfassende(re)s Hilbertsches Programm identifiziern, das sowohl in den Anfängen der Beweistheorie als auch heute noch Erfolge aufzuweisen hat, die den philosophischen Status der mathematischen Logik als Begründungsdisziplin der Mathematik uneingeschränkt rechtfertigen.

December 6, 2016, 14h c.t., Sand 13, B116, Tübingen:
Reinhard Kahle (Lisbon): Hilberts 24. Problem

Abstract: Im Jahr 2000 wurde in David Hilberts Nachlaß eine Notiz gefunden, in der er ein ursprünglich geplantes 24. Problem für seinen berühmten Vortrag auf dem Internationalen Mathematikerkongreß 1900 in Paris skizziert. In diesem Problem sollte es um "Kriterien für die Einfachheit bez. Beweis der grössten Einfachheit von gewissen Beweisen" gehen. In unserem Vortrag stellen wir Hilberts Gedanken kurz vor, gehen einigen historischen Spuren in der Entwicklung der Beweistheorie nach und diskutieren schließlich die philosophischen und mathematischen Herausforderungen, die sich auch heute noch aus Hilberts Fragestellung ergeben.

August 11, 2016, 16h c.t., Sand 1, A104, Tübingen:
Kosta Došen (Belgrade): Isomorphism in Intensional Logic

Abstract: Isomorphism of formulae is an equivalence relation stronger than mutual implication, based on identity of deductions in categorial proof theory, or identity of deductions coming from reductions in natural deduction, coded by typed lambda terms as in the Curry-Howard correspondence. Two formulae are isomorphic when one can replace the other either as a premise or as a conclusion so that nothing is lost nor gained---by composing further with a canonical deduction from one of these formulae to the other one returns to the original deduction, i.e. one obtains a deduction equal to it. Isomorphism may be taken in the spirit of proof-theoretic semantics as a plausible technical reconstruction of propositional identity, i.e. identity of meaning for propositions. This is properly a notion of intensional logic. A survey will be given of interesting known results for isomorphism of formulae in intuitionistic and classical propositional logic, and interesting unknown matters will be considered.

July 19, 2016, 17h s.t., Sand 13, B110, Tübingen:
Arnd Kulow (Herrenberg), Logic and Law Meeting

July 5, 2016, 18h c.t., Sand 1, A104, Tübingen:
Miloš Adžić (Belgrade): Gödel on the intensional logic of concepts

Abstract: In the course of his conversations with Hao Wang [Wang, 1996], Kurt Gödel discussed, among others, two very interesting and related topics. One is the notion of absolute proof and the other one is his intensional theory of concepts, which should, when developed, secure further his conceptual realism.

Although these remarks were made during the early 1970s, the ideas were in Gödel's mind for a long time already. His work on Russell's logic [Gödel, 1944] can be seen as considering various proposals for the realistic theory of concepts, finding them at the end all unsatisfactory. On the other hand, in [Gödel, 1946], he suggests that we look for the definitions of the notions of definability and provability, which are absolute in the sense of Turing's definition of the notion of computability. Unfortunately, what he says there about the notion of absolute provability is very brief and mostly limited to the case of provability in set theory. It seems that although Gödel paid a great deal of attention to these issues, he did not reach a conclusion that he would find completely satisfactory.

Some of the remarks Gödel made about these topics are taken as an inspiration, and a way to interpret them is proposed from the standpoint of contemporary logic.

[Gödel, 1944] Gödel, K. Russell's mathematical logic. In Kurt Gödel. Collected Works. Volume II. The Clarendon Press, Oxford University Press, New York, 1990.

[Gödel, 1946] Gödel, K. Remarks before the Princeton bicentennial conference on problems in mathematics. In Kurt Gödel. Collected Works. Volume II. The Clarendon Press, Oxford University Press, New York, 1990.

[Wang, 1996] Wang, H. A logical journey: from Gödel to philosophy. MIT Press, Cambridge, MA, 1996.

May 10, 2016, 18h c.t., Forum Scientiarum, Seminarraum 1.3, Tübingen:
Salvatore Florio (Kansas): Metalogic and the Overgeneration Arguments

Abstract: The so-called overgeneration argument has figured prominently in the debate over the logicality of second-order logic. However, what the argument is supposed to establish is far from clear. In the first part of the article, we examine the argument and locate its main source, namely the alleged entanglement of second-order logic and mathematics. We then identify various reasons why the entanglement may be thought to be problematic. In the second part of the article, we take a metatheoretic perspective on the matter. We prove a number of results establishing that the entanglement is sensitive to the kind of semantics used for second-order logic. These results provide evidence that, by moving from the standard set-theoretic semantics for second-order logic to a semantics that makes use of higher-order resources, the entanglement either disappears or may no longer be in conflict with the logicality of second-order logic.

January 26, 2016, 10h c.t., Sand 14, C118, Tübingen:
Lew Gordeew: On Proof Compressions in Sequent Calculi and Natural Deductions

Abstract: In traditional Proof Theory finite proofs/derivations/deductions are presented as rooted trees whose nodes are labeled with proof objects (e.g. sequents or formulas). A more general approach allows more liberal dag-like presentation ('dag' = directed acyclic graph). This opens up several size reducing tree-to-dag proof compression opportunities. The most natural proof compression idea is to merge distinct nodes labeled with identical proof objects.

Theorem 1. In a given sequent calculus S, any tree-like deduction d of a given sequent s is constructively compressible to a dag-like deduction d' of s in which sequents occur at most once. Thus, in d', distinct nodes are supplied with distinct sequents (that also occur in d).

Consequently, the size of d' can't exceed the total number of distinct sequents occurring in d, which in several cases can exponentially reduce the size of d. Moreover, if S is cutfree, then by the subformula property we conclude that sequents occurring in d' contain only subformulas of s. Analogous dag-like compressions of Prawitz-style tree-like natural deductions are more involved. This is due to the assumption's discharging operation. On the other hand, since natural deductions' nodes are labeled with single formulas, there is hope to get polynomial control over the size of d', provided that the subformula property holds.

Theorem 2. A natural embedding of Hudelmaier's sequent calculus for purely implicational logic into analogous Prawitz-style tree-like natural deduction calculus followed by appropriate dag-like "horizontal compression" allows us to obtain polynomial-size dag-like natural deductions d' of arbitrary tree-like inputs d.

A suitable formalization of the last theorem should prove the conjecture NP = PSPACE.



November 25, 2015, 16h c.t., Sand 13, B110, Tübingen:
Kosta Došen (Belgrade): Problems and results in general proof theory

July 23, 2015, 11h c.t., Sand 6, F116, Tübingen:
Paolo Pistone (Rome): Parametric polymorphism and completeness

Abstract: The standard technique to prove normalization for type theories is by means of a reducibility interpretation: one proves that typable terms are reducible (a soundness result), hence (strongly) normalizing. In this talk we focus on the converse direction (i.e. completeness): when are reducible terms typable? In (Girard 2006) it was conjectured that completeness holds for Pi_1 types (remark that it cannot hold for more complex types, due to incompleteness). We establish a lower and upper bound for completeness with respect to reducibility interpretations, by proving a completeness theorem for Pi_1 types (the universal closure of simple types). The proof of our theorem relies on two interpretations of polymorphism: a reformulation of the parametric interpretation within reducibility theory and a syntactic reformulation of the dinatural condition for (closed and normal) simply typed lambda-terms. A corollary of our result is that completeness holds for an untyped version of proof-theoretic validity (in the sense of Prawitz 1971).

July 14, 2015, 18h c.t., Forum Scientiarum, Seminarraum 2.3, Tübingen:
Vlasta Sikimic (Belgrade): Structurally enriched sequent systems

Abstract: Sequent systems that allow for more structural rules than the standard Gentzen one are particularly suitable for capturing a wider array of non-classical logics. In the talk we will focus on the potentials of Belnap's display calculus and it's extension with various types for capturing dynamic logics. However, the constrains of display calculus from the perspective of proof-theoretic semantics will also be presented. Finally, the discussion will be concluded by pointing to hypersequent and higher-level sequent calculi as those with more expressive power and smoother proof-theoretic behaviour than display calculi.

May 20, 2015, 18h c.t., Forum Scientiarum, Seminarraum 2.3, Tübingen:
Elia Zardini (Lisbon): Against the World

Abstract: In previous works, I've developed naive theories of truth and vagueness which validate the law of excluded middle (LEM) and the law of non-contradiction (LNC), and which solve the semantic paradoxes and the paradoxes of vagueness by restricting instead the structural properties of contraction and transitivity respectively. Moreover, the principle of distributivity of conjunction over disjunction (D) fails in the theories – in fact, even the weaker principle of modularity (M) fails. However, since neither kind of paradox seems to involve the last two principles in the first place, it might seem that the solutions I've proposed feature logics that are unnecessarily weak. I'll first argue that these appearances are deceiving: if the broad naive approaches I've proposed are on anything like the right track – in particular, if they are correct in upholding LEM and LNC – D and M just cannot be had. I'll then offer a philosophical diagnosis of the failures of D and M, arguing that the fundamental problem with D and M is that they allow one to go from the disjunctions of facts licenced by LEM to a disjunction of complete ways things are (aka worlds) each of which violates LNC. D and M fail because they transform the former, acceptable, "local" determinacy into the latter, unacceptable, "global" determinacy.