Colloquium

(no abstract)

Abstract: Consider the purely minimal implicational logic (M⊃). It is well-known that NP=PSPACE is equivalent to the existence of short (polynomially sized) and easy (verifiable in polynomial time) proofs for every M⊃ tautology. In [1], we show that such tautologies can be proved in Natural Deduction (for M⊃) with proofs linearly bounded on the height, by translation from Hudelmaier’s Sequent Calculus. Besides that we proved that such tree-like Natural Deduction proofs can be, in a certain way, horizontally compressed into Dag-like structures of polynomial size. These dag-like structures cannot be taken as certificates for validity of their conclusions yet. An additional information on the correct traversal of the dag-like structure is need. By some considerations on these additional information we reported a sequence of NP approximations for PSPACE-complete problems.

In this talk, we discuss some facts observed from our ongoing research finding facts to believe that NP=PSPACE. Firstly, we show that any exponentially sized linearly bounded height tree-like proof (huge proof) Pi of alpha in M⊃ is highly redundant. This is expressed by the fact that for such Pi, proof of alpha, there is at least one derivation Pi* that occurs exponentially many times as sub derivation of Pi. This is a combinatorial consequence of the fact that the tree-like proof is labelled with linearly many formulas (the set of subformulas from alpha) and the tree is linearly height-bounded too. In general there can be more than one (different) derivation that occur exponentially many times as sub-derivations of a tree-like proof. This sub-derivations and the way that they glue in each other to form the proof itself raises a kind of combinatorial analysis of proofs, which components are the occurring derivations and the analysis is the way they combine, by means of repetitions in the whole proof. We decompose any exponentially linearly height-bounded proof into a, somehow, combination of polynomially sized derivations. Each derivation is easily verifiable (polynomial time) and the combination seems to be verifiable in polytime too. In fact, this combination of the components resembles very much the horizontal compression method presented in [1]. Based on this facts, we propose a new horizontal compression algorithm, based on rewriting rules, that provides as upper-bound O(size^5(alpha)) on the size of the dag-like compressed proof Pi^c of alpha. Besides that, we provide an algorithm for verification of the validity of dag-like proofs that has upper-bound O(size^3(Pi^c)) in time.

[1] Gordeev, L. & Haeusler, E.H. Proof Compression and NP versus PSPACE, Studia Logica, Dec. 2017.

Abstract

Abstract: Logic is usually thought to be a normative discipline but it is not clear what this means exactly, especially in view of the plurality of logical systems, and it is no wonder that the ongoing debate on the normativity of logic has met the issue of pluralism in contemporary philosophy of logic. In this talk, I will first propose a critical review of this debate before discussing the idea of logical commitment as the basis of a correct understanding of the normativity of logic.

Abstract: Modal predicates are a reasonable alternative to modal operators. In the talk I sketch a method to develop systems for modal predicates that avoid semantic paradoxes. I start with a semantical construction in the spirit of Kripke´s fixed point construction, generalized to possible world models as Halbach and Welch developed. In the next step I introduce infinitary proof systems to capture the minimal fixed-points in a more constructive fashion. In the last step I consider finitary proof system that approximate the semantic construction. With this at hand I look at a possible application: Löb's theorem.

Abstract: The notion of assertion plays an inferential role in logic. It is a key ingredient in most logical systems, either implicitly or explicitly. For instance, Frege’s ideographical language of the Begriffsschrift introduced a specific sign designating assertion, ‘⊢’, which expresses the acknowledgement of the truth of the content of the assertion. In Peirce’s graphical logic of Existential Graphs (EGs), there is no specific sign for assertion, although the notion of assertion is used virtually everywhere in his logical writings. The reason is that making an assertion signals the responsibility that the utterer of the logical statement bears on the truth of the proposition. Indeed Peirce has assertion as a sign that is embedded in the Sheet of Assertion (SA), while SA represents both the logical truth as well as the assertoric nature of those graphical logical formulas that are scribed upon it. In intuitionistic logic, on the other hand, an explicit notion of assertion has been used in order to analyse inference and proof, to explicate the meaning of logical constants, and so on.

The idea of the notion of assertion thus appears robustly invariant across a range of logical theories, logical methods, and logical notations. In the light of the existence of such a common and shared character of assertions, we present a new system of graphs that makes the embedded or implicit nature of assertions in logical graphs explicit. We develop a graphical logic of assertions (called “Assertive Graphs”, (AGs)). We will show that it is possible to extend this constructive logic of AGs into a classical graphical logic ClAG without a need to introduce polarities in the graphs. We compare the advantages of these two approaches and point out the nature of a deep inference of their transformation rules. Finally, we discuss implications of AGs to logical inference.

Abstract: Negation in FOL operates on whole formulae. We extend FOL with negation operators whose scope is more narrow than an atomic formula. We define a subatomic natural deduction system for the extension, discuss the proof-theoretic properties of the system, and apply it to reasoning with predicate term negation (e.g., gradable adjectives with negative affixes).

Abstract: A typical argument in favour of substructural approaches to semantic paradoxes is the observation that restrictions to the operational rules for connectives are not sufficient to eliminate all versions of these paradoxes. In the talk I will introduce different substructural options to motivate a cluster of systems that restrict the structural rule of reflexivity. I will then show that infinitary proof systems based on a restriction of reflexivity amount to a surprisingly natural way of capturing proof-theoretically the reasoning internal to the standard picture of semantic groundedness given by familiar inductive constructions.

Abstract: The talk introduces a new type of rules into Natural Deduction, elimination rules by composition. These rules replace usual elimination rules in the style of disjunction elimination and give a more direct treatment of additive disjunction, multiplicative conjunction, existence and modalities. Elimination rules by composition have an enormous impact on proof-structures of deductions: they do not produce segments, deduction trees remain mostly binary branching, there is no vacuous discharge, there is no need of permutative or commutative reductions in most cases. The new type of rules fits especially to substructural issues, so it is shown for Lambek Calculus, i.e. intuitionistic non-commutative linear logic and other logics. Natural deduction formulated with elimination rules by composition from a complexity perspective is superior to other calculi like sequent calculi or proof-nets.

Abstract: In this talk I will argue for a revision of the usual rules for second order quantification (and of their proof-theoretic interpretation). In categorial semantics, formulas are interpreted as multivariant functors and proofs as dinatural (or, more precisely, extranatural) transformations between such functors. In this context the correct notion of universal quantification is not the usual one (intersection) but the notion of "end".
From a proof-theoretic viewpoint, dinaturality and extranaturality correspond to permutative principles (i.e. the fact that closed proofs are invariant, modulo normalization, with respect to a class of permutations). However this fact, which holds at the propositional and first-order level, fails for second order logic (i.e. System F), due to the fact that the rules of second order quantification do not correspond to the right notion of end. In a word, System F is not fully dinatural.
In order to explore a notion of proof invariant with respect to all permutations arising from dinaturality/extranaturality I first consider proof-nets, for two main reasons: first, proof-nets were invented to obtain proofs invariant with respect to permutation of rules; second, cut-elimination in proof-nets closely corresponds to composition of dinatural/extranatural transformations (as it appears clearly in Eilenberg-MacLane coherence theorems for monoidal categories, proved more than twenty years before Girard invented proof-nets!).
I will describe a new definition of proof-nets for second order logic which are invariant with respect to all permutations arising from dinaturality. Finally, I will provide some hints at a natural deduction definition of quantifiers as ends/co-ends, leading to a fully dinatural version of System F.

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.

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.

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.

(no abstract)

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.

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.

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.

(no abstract)

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).

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.

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.