The usage of diagrams is widespread in sciences. They are commonly viewed as pedagogical tools that do not play a non-redundant role in proofs. However, recent years witnessed the development of formal diagrammatic systems with strict rules of construction and manipulation. This `formalization' of diagrams makes them suitable for settings where formal proofs are required, notably in mathematics. This tradition of research received a mixed reception; it was praised for its rigor but was criticized for its `unnaturalness'. In this work, I address formalization from the standpoint of scientific instrumentation since diagrams may be regarded as scientific instruments. In particular, I explore the idea of epistemological strategies that consists in techniques that are used by scientists to reduce uncertainty and error in the manipulation of their instruments (here: diagrams). For the purpose, I provide a concrete historical case where formal rules are used as a scaffolding to ease the manipulation of the diagrams. Yet, with a little practice, rules can be subsequently dropped. Finally, I argue that this interpretation of formalization as an epistemological strategy suggests a modified, more acceptable, version of the much disputed `derivation-indicator view' in the philosophy of mathematical practice.
According to the so-called "Kant-Frege view" (Bennett 1966, 1974), existence is a quantifier. This view on existence is more or less explicitly endorsed by many philosophers and logicians who believe that Kant anticipated Frege's take on existence. However, the exact nature of the connection between Frege's claim that existence is a quantifier and Kant’s claim that existence is not a real predicate remains mysterious. The goal of my presentation is to explore the connection between these two claims, and to argue that Frege's idea that existence is a quantifier logically follows from Kant's idea that existence is not a real predicate.
There is no obvious and natural fit for classical first-order logic with inconsistencies, numeric confidences and discrete exceptions. However, mechanisms like these are apparently used in commonsense reasoning. We will briefly discuss the existing approaches and describe the principles and performance of our first order automated reasoner incorporating the beforementioned capabilities. We will also give a small demo of our pilot system able to understand and answer statements and questions posed in English, using mainly symbolic reasoning.
To verify the correctness of programs one often uses so-called Hoare logics. To verify quantum programs, we need quantum Hoare logics (QHL). I will give a short overview how QHLs work, and then present an extension of QHL, QHL with ghosts variables.
Grigori Mints (1939-2014) is without doubt the most renowned mathematical and philosophical logician connected to Estonia. Before becoming a Stanford professor in 1991 and after having spent the first two decades of his career in Leningrad, he worked in Tallinn in the lab of Enn Tõugu during the 1980s. Grisha was above all a proof theorist and theorem prover with a special interest in intuitionistic and modal logic. I will tell a bit about his work related to Estonia, in particular about resolution for intuitionistic propositional logic and some modal logics.
Symmetric monoidal closed categories are standard models of multiplicative intuitionistic linear logic (MILL). Symmetric skew monoidal closed categories are weaker versions of non-skew ones where the three natural isomorphisms, corresponding to left and right unitality and associativity, are merely natural transformations and symmetry acts on three objects rather than two. In this talk, I will discuss (i) the syntactic correspondents of aforementioned skew categories, which are semi-associative variants of MILL; (ii) a normalization process for these calculi, which is inspired by Jean-Marc Andreoli's focusing but equipped with tag annotations to track new formulae in context. The normalization process is not only a proof of coherence of these skew structured categories but also a hint toward a possible algorithm to compute normal forms of derivations in non-skew MILL.
We present an overview of the semantics of first-order temporal logics based on the counterpart paradigm in the sense of Lewis: we start by introducing a standard set-based semantics for our logic QLTL, and then we define a categorical semantics based on relational presheaves. The constructions are formalized using the dependently typed programming language and proof assistant Agda, and we employ the agda-categories library to adequately capture the notions of category theory required in our setting. After introducing the logic and its models, we will present some results on the positive normal form of QLTL and then conclude with some remarks on the formalization of the logic in a proof assistant and our experience with it.