Past talks

Handout: click here

Video: click here

Abstract: This paper develops a semantic theory of redundancy by positing a redundancy operator R that can be inserted locally and optionally into logical form. Rp says that p is true and that p is not redundant in its local context, i.e., p is true somewhere but not everywhere in its local context. This operator explains a variety of phenomena, including diversity constraints, ignorance inferences, and free choice.

Handout: click here

Video: click here

Abstract: Philosophers of science often assume that logically equivalent theories are in fact theoretically equivalent; in fact, this is an implicit commitment in most accounts of theoretical equivalence. I argue that (a) one version of anti-exceptionalism about logic raises a serious epistemic worry for this commitment, and that (b) logical realism (which says, roughly, that differences in logic reflect genuine metaphysical differences in the world) raises a serious metaphysical worry for it. It might be thought that we can contain these problems—or at least those raised by logical realism—by treating theoretical equivalence as domain-specific: theoretical equivalence, on this view, does not entail metaphysical equivalence, since metaphysics makes more fine-grained distinctions between theories than science does. I do not think this move works.

Video: click here

Abstract: Rudolf Carnap is often thought to be a prototype of a logical pluralist. That is, Carnap is thought to hold that more than one logic is correct. I will show in this paper that he cannot be a logical pluralist. I will also show that he cannot be a logical monist or nihilist. In effect, he must think that the question of whether logical pluralism, monism or nihilism is true is illegitimate.

Video: click here

Abstract: Proof-theoretic validity offers a justification for the logical laws. However, it has recently been shown that proof-theoretic validity does not offer a semantics for intuitionistic logic, but rather it provides a semantics for intermediate logics which aren’t harmonious. This is worrying as baked into the philosophical justification for proof-theoretic validity is the idea that it results in a logic with harmonious rules. I show that the lack of harmony stems from the treatment of atomic sentences, not from the treatment of logical connectives. I propose a modification to proof-theoretic validity that could remove the undue impact of atomic formulas sentences.

Video: click here

Abstract: Theories of self-applicable truth have been motivated in two main ways. First, if truth-conditions provide the meaning of (many kinds of) natural language expressions, then self-applicable truth is instrumental to develop the semantics of natural languages. Second, a self-applicable truth predicate is required to express generalizations that would not be otherwise expressible in natural languages. In order to fulfill its semantic and expressive role, we argue, the truth predicate has to be studied in its interaction with constructs that are actually found in natural languages and extend beyond first-order logic — modals, indicative conditionals, arbitrary quantifiers, and more. Here, we focus on truth and quantification. We develop a Kripkean theory of self-applicable truth (strong Kleene-style) for the language of Generalized Quantifier Theory. More precisely, we show how to interpret a self-applicable truth predicate for the full class of type ⟨1, 1⟩ (and type ⟨1⟩) quantifiers to be found in natural languages. As a result, we can model sentences which are not expressible in theories of truth for first-order languages (such as ‘Most of what Jane’s said is true’, or ‘infinitely many theorems of T are untrue’, and several others), thus expanding the scope of existing approaches to truth, both as a semantic and as an expressive device. Along the way, we will point at the relations between our work and recent works in similar directions (by Hartry Field, Bruno Whittle, and others).

Joint work with Michael Glanzberg (Rutgers).

Video: click here

Abstract: We are considering the basic intuitionistic first-order logic without equality, together with some of its standard companions which include the intuitionistic logic of constant domains and the extensions of intuitionistic logic (both with and without the constant domain restriction) with either extensional or intensional equality predicate. In other words, we single out the family of six logical systems which we call the standard intuitionistic logics.

We show how these logics can be approached within the framework of abstract model theory, and in doing so, we show that every standard intuitionistic logic is the maximal logic among the class of its own abstract extensions that displays the combination of the following three properties: (1) intuitionistic compactness or star-compactness, (2) Tarski Union Property, and (3) preservation w.r.t. an appropriate simulation notion.

This is a joint work with Reihane Zoghifard (Institute for Research in Fundamental Sciences, Iran)

Video: click here

Abstract: Free logics is a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that (i) the domain of interpretation is not empty, (ii) every name denotes exactly one object in the domain and (iii) the quantifiers have existential import. Free logics usually reject the claim that names need to denote in (ii), and of the systems considered in this paper, the positive free logic concedes that some atomic formulas containing non-denoting names (including self-identity) are true, while negative free logic rejects even the latter claim.

These logics have complex and varied axiomatizations and semantics, and the goal of the present work is to offer an orderly examination of the various systems and their mutual relations. This is done by first offering a formalization, using sequent calculi which possess all the desired structural properties of a good proof system, including admissibility of contraction and cut, while streamlining free logics in a way no other approach has. We then present a simple and unified system of generalized semantics, which allows for a straightforward demonstration of the meta-theoretical properties, while also offering insights into the relationship between different logics (free and classical). Finally, we extend the system with modalities by using a labeled sequent calculus, and here we are again able to map out the different approaches and their mutual relations using the same framework.

This is a joint work with Norbert Gratzl of MCMP, Munich.

Video: click here

Abstract: Algebraic logic and probability theory have had a deep connection from the start: in fact, in the work of George Boole, what we now call Boolean algebras provided a first common abstraction of the notions of logical statement as well as of probabilistic event. In this talk we will see how a notion of probability map has been defined on well-known ordered structures, such as lattice ordered groups, MV-algebras and other residuated structures connected to substructural logics. In particular, we are interested in the probability theory of so-called “many-valued events”: events that can result to be neither true nor false, but true to some degree. The algebraic approach has proven to be powerful in this context, and it has shown interesting connections to measure theory. In this framework, we will also see how Łukasiewicz logic can be used to define a logic for probabilistic reasoning on both classical and many-valued events.

Video: click here

Abstract: In this project, I axiomatize the two dimensional deontic logic in Fusco (2015), which validates a form of free choice permission (von Wright, 1969; Kamp, 1973); (1) below) and witnesses the nonentailment known as Ross’s Puzzle (Ross, 1941; (2) below).

(1) You may have an apple or a pear => You may have an apple, and you may have a pear.

(2) You ought to post the letter =/=> You ought to post the letter or burn it.

Since ♢(p or q) = (♢p v ♢q) and □(p) => □(p v q) are valid in any normal modal logic—including standard deontic logic—the negations of (1)-(2) are entrenched in modal proof systems. To reverse them without explosion will entail excavating the foundations of the propositional tautologies. The resulting system pursues the intuition that classical tautologies involving disjunction are truths of meaning rather than propositional necessities. Technical results include joint work with Arc Kocurek (Cornell).

Video: click here

Abstract: It is natural to view belief as based on evidence. Namely, belief of an agent can be based on information confirmed by a source the agent considers reliable. When it comes to information, its potential incompleteness, uncertainty, and contradictoriness needs to be dealt with adequately. Separately, these characteristics has been taken into account by various appropriate logical formalisms and (classical) probability theory. While the first two are often accommodated within one formalism (e.g. various models of imprecise probability), the second two less so. Conflict or contradictoriness of information is rather to be resolved or gotten rid of than to be reasoned with. In this talk I will describe a logical framework in which belief is based on potentially contradictory information. The confirmation comes from multiple, possibly conflicting, sources, and is of a probabilistic nature.

We will adopt a two-layer modal logical framework to account for evidence and belief separately. On the lower layer, we will use Belnap-Dunn four-valued logic and its probabilistic extensions to account for potentially contradictory information coming from the sources on which belief is grounded. To do so, positive and negative support (evidence in favour and evidence against) a statement is taken separately in the semantics, and this two-dimensionality is carried over to the layer of agent’s belief. On the upper layer, we will combine it with a many-valued logic to account for belief. Examples of upper-layer logics, which are interpreted over (bi-lattice) product algebras based on the [0,1] real interval to account for the two-dimensionality of positive and negative component of belief, include extensions of Łukasiewicz or Gödel logic with a de-Morgan bi-lattice negation, or bi-lattice Łukasiewicz or Gödel logics.

Joint work with Sabine Fritella, Daniil Kozhemiachenko, Ondrej Majer, and Sajad Nazari.

Video: click here

Abstract: Considerable attention has been payed recently to a position known as anti-exceptionalism about logic (AEL), which attempts to downplay in some sense the exceptional nature of logic as a discipline and subject. What is not so apparent, however, is the regard in which logic is supposed to be unexceptional. While it has become common in the literature to simply define AEL as the claim that logic is continuous with the sciences, we argue here that this is a mistake for several reasons. Instead, rather than explicitly drawing a close connection between logic and the sciences, AEL is best understood as rejecting traditional properties of logic which were putatively taken to distinguish logic from the sciences. Further, it’s shown that rather than there being one anti-exceptionalist tradition requiring us to reject all of these traditional properties, as is sometimes assumed, there are in fact at least two distinct types of AEL—metaphysical and epistemological AEL—with differing motivations, which require the rejection of distinct subsets of these traditional properties. To further emphasise this point, we show that what we take to be the most detailed anti-exceptionalist account of logic’s methodology, logical predictivism, requires us to make no commitment to a form of metaphysical AEL. Neither form of AEL, therefore, necessary stand or fall together.

Video: coming soon

Abstract: Benacerraf (1973) posed the following challenge for mathematical realism: how can we have knowledge of mathematical objects, given that they lie outside the causal realm? Balaguer (1995) famously argued that full-blown Platonism, the view that every consistent mathematical theory truly describes a part of the mathematical realm, can offer a successful naturalistic response to the challenge. Pluralist views such as Balaguer's have attracted much interest but have also been the subject of significant criticism, most saliently from Putnam (1979) and Koellner (2009). These critics argue that, due to the possibility of arithmetizing the syntax of mathematical languages, one cannot coherently say that mathematics is a matter of convention whilst consistency is a matter of fact. In response, Warren (2015) argued that Putnam's and Koellner's argument relies on a misunderstanding, and that it is in fact coherent to maintain a pluralist conception of mathematical truth while supposing that consistency is a matter of fact. In this paper we argue that it is not. We put forward a modified version of Putnam's and Koellner's argument that isn't subject to Warren's criticisms.

Video: click here

Abstract: Philosophers and linguistics have recently shown a growing amount of interest in truthmaker semantics (van Fraassen 1969; Yablo 2014; Fine 2016, 2017), a new family of approaches to logical semantics oriented around the notion of ‘exact’ verification with a broad range of applications in philosophical logic and formal linguistics, including to the study of partial content, subject matter, logical subtraction, ground, confirmation, verisimilitude, counterfactuals, imperatives, attitude verbs and modals. In this talk, I develop a compositional generalization of the standard theory of “recursive” truthmaking (as opposed to the “reductive” truthmaking in Yablo 2014), which allows for a unified cross-categorial treatment of negation, conjunction, disjunction, and quantification in a pluralized partial setting.

The standard truthmaker semantics is bicamera in that sentences are both positively and negatively interpreted through a bilateral system of recursive clauses that bottom out in the assignment of truthmakers and falsemakers to atomic sentences. Following some informal remarks in Fine (2017), I extend this double-entry approach to expressions of all syntactic categories, including quantificational and non-quantificational DPs which are assigned both denotations and “anti-denotations” from a rich entity space containing both positive and negative individuals and their sums. In this framework, certain non-upward entailing quantifiers and coordinated DPs can be analyzed as denoting “mixed polarity” pluralities with both positive and negative parts, and I can thereby deal with the main challenges facing the collective treatment of conjunction as fusion raised in Champollion (2015).

Video: coming soon

Abstract: In this talk, I will focus on a logical analysis of the decision processes of individuals that lead to the social herding phenomenon known as informational cascades. In particular, I will focus on the question whether rational agents who use their higher-order reasoning powers and who can reflect on the fact that they are part of an informational cascade, can ultimately stop the cascade from happening. To answer this question I use dynamic epistemic logic to give a complete analysis of the information flow in an informational cascade, capturing the agents' observations, their communication and their higher-order reasoning power. I will follow the results presented in [1], which show that individual rationality isn't always a cure that can help us stop a cascade. However, other factors that deal with the underlying communication protocol or that focus on the reliability of agents in the group, give rise to conditions that can be imposed to prevent or stop an informational cascade from happening in certain scenarios.

[1] A. Baltag, Z. Christoff, J. Ulrik Hansen, and S. Smets. Logical models of informational cascades. In J. van Benthem and F. Lui (eds). Logic across the University: Foundations and Applications, Studies in Logic, pp. 405–32. College Publications, 2013.

Video: click here

Abstract: The background for this work includes Freyd's Theorem, in which the unit interval is viewed as a final coalgebra of a certain endofunctor in the category of bipointed sets. Leinster generalized this to a broad class of self-similar spaces in categories of sets, also characterizing them as topological spaces. Bhattacharya, Moss, Ratnayake, and Rose went in a different direction, working in categories of metric spaces, obtaining the unit interval and the Sierpinski Gasket as a final colagebras in the categories of bipointed and tripointed metric spaces respectively. To achieve this they used a Cauchy completion of an initial algebra to obtain the required final coalgebra. In their examples, the iterations of the fractals can be viewed as gluing together a finite number of scaled copies of some set at some finite set of points (e.g. corners of triangles). Here we will expand these ideas to apply to a broader class of fractals, in which copies of some set are glued along segments (e.g. sides of a square). We use the method of completing an initial algebra to obtain a final coalgebra which is Bilipschitz equivalent to the Sierpinski Carpet, and additionally use the fact that we can view this object as the limit of an appropriately chosen chain. We will explore some ways in whichthese results may be further generalized to a broader class of fractals.

Abstract: Despite some notorious defenders, most philosophers reject the view that knowledge is closed under (metaphysical) entailment. The main reason for this involves familiar and seemingly absurd consequences this view has concerning necessary truths. I will go over arguments to the end of showing that similar consequences follow with respect to contingent truths: if one’s knowledge is closed under entailment, one can know any true proposition whatsoever. In the end I will apply those arguments to extant views in the philosophy of religion, views which take God to be less than omniscient, and I will argue that such views must impose a further restriction on divine knowledge according to which God’s knowledge fails to be closed under entailment.

Video: click here

Abstract: In the field of axiomatic theories of truth, conservativity properties of theories are much investigated. Conservativity can be used to argue that, despite the well-known undefinability of truth, there is a sense in which a primitive truth predicate can be reduced to the resources of an underlying mathematical theory that provides basic syntactic structure to truth ascriptions. Conservativity is typically proved model-theoretically (by suitable model-expansion arguments), or proof-theoretically via the elimination of cuts on formulae containing truth (Tr-cuts). The existing Tr-cut-elimination arguments are both extremely complex and applicable only to typed axiomatizations of the truth predicate. In the talk we will prove the following: let B a suitable base theory and T[B] an extension of B obtained by adding compositional axioms for truth (Tarskian-, Kripke-Feferman-, Friedman-Sheard-style) to it without extending non-logical schemata of B to the truth predicate. Then every Tr-cut in T[B] can be eliminated. This entails a simple and uniform proof of the conservativity of T[B] over B. A novel aspect of the result is the use of a suitably modified version of the Free-Cut Elimination Theorem by Takeuti (further developed by Sam Buss). This is joint work with Luca Castaldo.

Video: click here

Abstract: The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.

Reference
Daniel Găină, 2020, Forcing and Calculi for Hybrid Logics, Journal of the ACM 67(4): 1-55.

Video: click here

Abstract: Kolmogorov, in 1923, proposed a model for intuitionistic propositional logic called the Calculus of Problems. Although simple and natural, this model was non-rigorous. A rigorous version of this was given by Medvedev and Muchnik in the 1950s and '60s using the concept of Turing oracles. Thus started the study of mass problems and the reducibility notions between these. Sheaves over topological spaces as models for higher-order intuitionistic logic were studied independently. These models are also examples of elementary topoi. In this work, we have extended the Kolmogorov/Medvedev/Muchnik line of work to a model of intuitionistic higher-order logic that we call the Muchnik topos. The Muchnik topos may be described in brief as the category of sheaves of sets over the topological space consisting of the Turing degrees, where the Turing cones form a base for the topology. We have also introduced, within the Muchnik topos, a class of intuitionistic real numbers, different from the Dedekind and Cauchy reals. We call these the Muchnik reals.

Video: click here

Abstract: Sometimes philosophers change their beliefs regarding which logical principles are correct. For example, one might come to abandon the law of excluded middle out of constructivist inclinations or reject the material conditional on grounds of irrelevance. Yet mainstream belief revision systems (such as those of the AGM and DDL traditions) cannot handle this kind of belief revision because such systems only model belief revision within logical frameworks, not between them. In my talk, I present an AGM-style belief revision system that can accommodate change in belief about logical principles. I propose various postulates that we should expect to hold of belief revision about logical principles and then show how to construct formal operators that comply with these postulates. Special attention is given to operators that guarantee the non-triviality of new belief sets. Triviality-avoiding revision is not always possible without modifying the non-logical content of one’s beliefs, which generates interesting challenges regarding the relationship between logical and non-logical information. I propose several revision operators that each address these challenges in different ways.

Video: click here

Abstract: The Four-Color Theorem (4CT, delivered in Appel and Haken (1977) and Appel, Haken, and Koch (1977)) is the first case of an original mathematical result obtained through the massive use of computing devices. Despite having been the subject of exceptional amounts of advertising and philosophical commentary, this notorious mathematical result is still relevant as a case study in the philosophy of mathematical practice and, more broadly, in the history of mathematics, for two reasons. On the one hand, given the existence of (at least) two other versions of the proof, the case suggests a discussion about the criteria for establishing the identity of computer-assisted proofs (with a corollary question about the identity of computer programs, proof assistants, etc.). On the other hand, a vital dimension of the proof has not yet been analysed: the interplay between its computational and the diagrammatical elements. Building on the methodological guidelines suggested in Chemla (2018), I offer a partial description of Appel and Haken (1977) and Appel, Haken, and Koch (1977), showing how computing devices interact with diagrams in these texts. With such a description, I offer a new way of tackling the question about the identity of proofs, articulating both reasons for defending the relevance of the 4CT for the history and the philosophy of mathematical practice.

Video: click here

Abstract: How can we know which inferences are valid and which ones are not? In particular, how can we know that ex contradictione quodlibet (ECQ) (A, ¬A ⊨ B for every A and B) is invalid as paraconsistent logicians claim? A popular view to answer these questions in recent years is abductivism. According to this view, we should accept a logical theory which best explains the relevant data. One central tenet of abductivism as it is used by paraconsistent logicians is a broadly empirical methodology. Paraconsistent logicians consider empirically observable data and use this to argue that ECQ is invalid. In this paper, I will defend this empirical methodology. First, I will show that some paraconsistent logicians employ an empirical methodology in arguing for the paraconsistent nature of logic. Second, I will present a view of normativity that is compatible with an empirical methodology. Third, I will develop an anti-exceptionalist view that takes logic to be normative, yet continuous with empirical sciences. Fourth, I will argue against the a priori conception of logic. My conclusion will be that the empirical methodology employed by some paraconsistent logicians is defensible.

Abstract: Multialgebras (or hyperalgebras) are algebras which at least one of the operations (called multioperations) returns a subset instead of a single element of the domain. Multialgebras have been very much studied in the literature and in the realm of Logic, they were considered by Avron and his collaborators, under the name of non-deterministic matrices (or Nmatrices), as a useful semantics tool for characterizing some logics of formal inconsistency (LFIs). In particular, these logics of formal inconsistency are not algebraizable by any method, including Blok and Pigozzi general theory. Carnielli and Coniglio introduced a semantics of swap structures for LFIs, which are Nmatrices constructed over triples in a Boolean algebra, generalizing Avron’s non-deterministic matrices. In this work we develop the first steps towards an algebraic theory of swap structures for LFIs. The logic mbC is the weakest system in the hierarchy of LFIs and the system QmbC is the extension of mbC to first-order language. The goal of this talk is to present the first steps towards a theory of non-deterministic algebraization of logics by swap structures. Specifically, a formal study of swap structures for logics of formal inconsistency is developed, by adapting concepts of universal algebra to multialgebras in a suitable way and we introduce also an algebraic semantics for QmbC. From the algebraic point of view these structures enable us to obtain properties of first-order logic QmbC and in the proof of the Soundness Theorem we can see interesting particularities of the first-order swap structures, especially with respect to the Substitution Lemma. This study opens new avenues for dealing with non-algebraizable logics through by the more general methodology of multialgebraic semantics.

Video: click here

Abstract: Kreisel's squeezing argument (1967) shows that there is an informal notion of validity which is irreducible to both model-theoretic and proof-theoretic validity of First-Order Logic (FOL), but coextensive with both formal notions. His definition of informal validity as truth in all structures received some criticisms in the literature for being heavily model-theoretical (Smith (2011) and Halbach (2020)). However, because of its simple and schematic form, variants squeezing argument has been presented for capturing other intuitive notions of validity closer to our pre-theoretical notion of validity (Shapiro, 2005). Therefore, the different squeezing arguments we find in the literature show that there are other informal notions of logical validity, which are coextensive with their corresponding formal definition of logical validity. In this talk, we argue for an even form of pluralism, showing that squeezing arguments cannot squeeze in the uniqueness of the corresponding informal notion. Indeed, we maintain that a complete logical system can be compatible with different notions of informal validity.

Joint work with Giorgio Venturi.

Video: click here

Abstract: Recursive functions on the natural numbers can be characterized as the class of functions generated from a specified list of initial functions and inductive conditions. In “Undecidability without Arithmetization”, Andrzej Grzegorczyk constructed a class GD of relations on the set of words with 2 letters, which is characterized in a similar way (as the class of relations generated from a specified list of initial relations and inductive conditions). We want to show that GD is precisely the class of relations on the set of words with 2 letters that are also recursive sets.

Video: click here

Abstract: This talk is about the fragment of Classical Logic that respects the Variable-Sharing Principle.

Video: click here

Abstract: In this work, I present a variant of so-called ‘informational semantics’, a technique elaborated by E. Voishvillo, for two quatervalent infectious logics, Deutsch’s Sfde and Szmuc’s dSfde in order to illuminate how incompleteness and inconsistency (understood in the ‘infectious’ way) effect on the truth and falsity conditions for conjunction and disjunction. In a nutshell, I suggest two kinds of semantical conditions: ‘affirmative’ one for logics with infected gaps and ‘rejective’ one for those where gluts are infected only. With regard to the technical part, I formalize these logics in the form of natural deduction calculi, thereby solving several problems: to fill the corresponding gap in the study of a proof- theoretical aspect of infectious logics; to revise Petrukhin’s result for Sfde; to provide simple natural deduction systems for Sfde and dSfde, representing a fundamental symmetry between them and forming a convenient basis for further extensions.

Video: click here

Abstract: SST is a small intuitionistic set theory governing the hereditarily finite sets. It is based upon set induction. Simple as SST is, it seems remarkably strong: it deduces--within intuitionistic formal logic--all the axioms of ZF + AC, less the Axiom of Infinity, except that Separation is limited to decidable predicates. It is relatively straightforward to prove that SST has the usual Goedelian incompleteness properties. SST is definitionally equivalent to full, first-order intuitionistic arithmetic, aka Heyting Arithmetic. And SST manifests the attractive metamathematical properties of many intuitionistic mathematical theories--it supports a number of different realizability and topological interpretations and can be assumed to be categorical.

Video: click here

Abstract: When properly arithmetized, Yablo's paradox results in a set of formulas which (with local disquotation in the background) turns out to be consistent, but $\omega$-inconsistent. Adding either uniform disquotation or the $\omega$-rule results in inconsistency. Since the paradox involves an infinite sequence of sentences, one might think that it doesn't arise in finitary contexts. We study whether it does. It turns out that the issue depends on how the finitistic approach is formalized. On one of them, proposed by M. Mostowski, all the paradoxical sentences simply fail to hold. This happens at a price: the underlying finitistic arithmetic itself is $\omega$-inconsistent. Finally, when studied in the context of a finitistic approach which preserves the truth of standard arithmetic, the paradox strikes back --- it does so with double force, for now the inconsistency can be obtained without the use of uniform disquotation or the $\omega$-rule. Joint work with Rafał Urbaniak (Gdańsk).

Video: click here

Abstract: Christine Ladd-Franklin is often hailed as a guiding star in the history of women in logic—not only did she study under C.S. Peirce and was one of the first women to receive a PhD from Johns Hopkins, she also, according to many modern commentators, solved a logical problem which had plagued the field of syllogisms since Aristotle. In this paper, we revisit this claim, posing and answering two distinct questions: Which logical problem did Ladd-Franklin solve in her thesis, and which problem did she think she solved? We show that in neither case is the answer "a long-standing problem due to Aristotle". Instead, what Ladd-Franklin solved was a problem due to Jevons that was first articulated in the 19th century.

Video: click here

Abstract: There is a great deal of work on logics for games in multi-agent systems. These logics are concerned with formally defining statements like "If Alice and Bob cooperate, they can follow a strategy so that they are certain to achieve their goal," or "no matter what Cath does, she cannot be sure of achieving her goal," or "Alice can ensure that either Bob is certain not to reach his goal, no matter what he does, or Cath is cerain to reach her goal if she follows the right strategy." My talk will be focused on how to include imperfect information in these systems: if the agents do not have full information about the current state of the system, how does this change their power to act strategically in order to achieve their goals? In particular, I will discuss my current work with Bastien Maubert on some approaches to the formal expression of agents' knowledge and strategic abilities in multi-agent systems with imperfect information.

I will begin by presenting Alternating-time Temporal Logic (ATL), a logic describing the abilities of coalitions of agents in concurrent game structures. I will describe some difficulties with adapting variants of ATL to imperfect information settings. Next I will introduce Strategy Logic (SL), a logic with a similar purpose to ATL, which differs in that it takes strategies to be explicit objects in the logic, making it more powerful but less decidable than ATL. For example, SL can state the existence of Nash equilibria, whereas ATL cannot. I will describe our current work on an imperfect information variant of SL, the addition of epistemic operators, the difficulties in restricting SL to only consider uniform strategies, and a solution to this difficulty.

Video: click here

Abstract: We estimate the size of a labelled tree by comparing the amount of (labelled) nodes with the size of the set of labels. Roughly speaking, a exponentially big labelled tree, is any labelled tree that has an exponential gap between its size, number of nodes, and the size of its labelling set. The number of sub-formulas of any formula is linear on the size of it, and hence any exponentially big proof has a size $a^n$, where $a>1$ and $n$ is the size of its conclusion. In this article, we show that the linearly height labelled trees whose sizes have an exponential gap with the size of their labelling sets posses at least one sub-tree that occurs exponentially many times in them. Natural Deduction normal proofs and derivations in minimal implicational logic ($M_\supset$) are essentially labelled trees. By the sub-formula principle any normal derivation of a formula $\alpha$ from a set of formulas $\Gamma=\{\gamma_1,\ldots,\gamma_n\}$ in $M_\supset$, establishing $\Gamma\vdash_{M_\supset}\alpha$, has only sub-formulas of the formulas $\alpha,\gamma_1,\ldots,\gamma_n$ occurring in it. By this relationship between labelled trees and normal derivations in $M_\supset$, we show that any normal proof of a tautology in $M_\supset$ that is exponential on the size of its conclusion has a sub-proof that occurs exponentially many times in it. Thus, any normal and linearly height bounded proof in $M_\supset$ is inherently redundant. Finally, we show how this redundancy provides us with a highly efficient compression method for propositional proofs. We also provide some examples that serve to convince us that exponentially big proofs are more frequent than one can imagine. We conclude by providing reasons to believe that the compression method discussed here can be applied to super-polynomial proofs.

Video: click here

Abstract: When scholars try to compare Dignāga’s Buddhist logic with Western logic, most of them take Aristotle’s syllogism as the paradigm―since they propose that the canonical argument for Dignāga is a deductive argument. However, some scholars argue against this interpretation, they claim that the canonical argument cannot be a deductive one because of exclude pakṣa. This paper argues for the opposite. I suggest that exclude pakṣa of Dignāga’s Buddhist logic is compatible with deduction from the contextual point of view. By demonstrating how to formalize Buddhist logic with the use of symbolic logic, particularly predicate logic, I explain why some scholars claim that exclude pakṣa would keep the canonical argument out of deduction. To solve the problem, I reveal the similarity between Buddhist logic and Stalnaker’s assertion theory, in which exclude pakṣa relates to the domain of discourse. Finally, I provide more detail about the role of exclude pakṣa and explain why it does not compromise the deductive power of the canonical argument.

Video: click here

Abstract: Much of modern logic originates in work on the foundations of mathematics. My talk reports on work in logic that has a different goal, the study of inference in language. This study leads to what I will call “natural logic”, the enterprise of studying logical inference in languages that look more like natural language than standard logical systems. The talk should appeal to several communities: mathematical logicians interested in completeness and complexity results, including results for logical systems that are not first-order. (The talk also includes the simplest completeness theorem in all of logic.) It also should interest philosophers of logic curious about syllogistic reasoning and its many modern extensions, and also about taking inference seriously in natural language semantics. And it has something to say to people in natural language processing, since there are now several working systems based on natural logic which can perform simple inference on text in the wild, and our community is engaged in a dialog with the machine learning NLI community, since machine learners now outperform the logical tradition.

Video: click here

Abstract: Higher-order likes and desires sometimes lead agents to have ungrounded or paradoxical preferences. This situation is particularly problematic in the context of games. If payoffs are interdependent, the overall assessment of particular courses of action becomes ungrounded; in such cases the matrix of the game is radically under-determined. In this talk I propose a dynamic doxastic and preference logic that can mimic the search for a suitable matrix. Upgrades are triggered by conjectures on other players’ utilities, which can in turn be based on behavioral or verbal cues. We can prove that, under certain conditions, pairs of agents with paradoxical preferences eventually come to believe that they are not able to interact in a game. As a result I hope to provide a better understanding of game-theoretic ungroundedness, and, more generally, of the structure of higher-order preferences and desires.

Video: click here

Abstract: In his Quadratura, Paul of Venice (1369-1429) considers a sophism involving time and tense which appears to show that there is a valid inference which is also invalid. His argument runs as follows: consider the inference concerning some proposition A: A will signify only that everything true will be false, so A will be false. Call this inference B. Then B is valid because the opposite of its conclusion is incompatible with its premise. In accordance with the standard medieval doctrine of ampliation, Paul takes A to be equivalent to ‘Everything that is or will be true will be false’. But he proceeds to argue that it is possible that B’s premise (‘A will signify only that everything true will be false’) could be true and its conclusion false, so B is not only valid but also invalid. Thus A is the basis of a logical paradox, aka an insoluble. In his Logica Parva, a self-confessedly elementary texts aimed at students and not necessarily representing his own view, and in the Quadratura, Paul follows the solution found in the Logica Oxoniensis, which posits an implicit assertion of its own truth in insolubles like B. However, in the treatise on insolubles in his Logica Magna, Paul develops and endorses Roger Swyneshed’s solution, which stood out against this “multiple-meanings” approach in offering a solution that took insolubles at face value, meaning no more than is explicit in what they say. On this account, insolubles imply their own falsity, and that is why, in so falsifying themselves, they are false. We consider how both types of solution apply to B and how they complement each other. On both, B is valid. But on one (following Swyneshed), B has true premises and false conclusion, and contradictories can be false together; on the other (following the Logica Oxoniensis), the counterexample is rejected.

Video: click here

Abstract: Saul Kripke's work on the semantics of non-normal modal logics introduced the idea of non-normal worlds, worlds where logically impossible things may hold. Such worlds can naturally be thought of as impossible worlds. Since Kripke's invention, the notion of an impossible world has undergone much fruitful development and application. Impossible worlds may be of different kinds—or maybe different degrees of impossibility; and these worlds have found application in many areas where hyperintensionality appears to play a significant role: intentional mental states, counterfactuals, meaning, property theory, to name but a few areas. But what, exactly, is an impossible world? How is it best to characterise the notion? To date, the notion is used more by example than by definition. In this paper I will investigate the question and propose a general characterisation, suitable for all standard purposes and tastes. In particular, it can be deployed whatever one takes the correct logic to be.

Video: click here

Abstract: In the meta-theory of classical first order logic, the Completeness, Löwenheim-Skolem and Compactness theorems stand out as the "Big Three" among the results of the subject. The best known proofs of these facts are due to Henkin and, although very transparent, they require a fair bit of classicality for their reasoning to go through. To circumvent this problem in the context of an inconsistent meta-theory it makes sense to look for alternative approaches. In this talk, we take a "low-tech" argument originally due to Löwenheim (but later perfected by Gödel in his PhD thesis) and reconstruct it in the context of a substructural meta-theory with the naive comprehension schema. In particular, we establish by non-classical means the Big Three in their original formulation involving material implication. Our object logic will be a non-contractive variant of the quantificational logic of paradox (LPQ) with the Church constant (falsum). This is joint work with Zach Weber and Patrick Girard.

Video: click here

Abstract: This talk is based on the following claim: The connexive logic axiomatized in Nelson's Intensional Relations (NL) can be provided with a relational semantics in the style of the ones described by Jarmużek and Malinowski in their Boolean Connexive Logics. I will offer an overview of both relational semantics for Boolean connexive logics, and the intensional vocabulary included in NL. Then I will go over the process behind obtaining a relational semantics for NL, with an emphasis on the proof for the only contraclassical axiom in the logic. Finally, I will compare the resulting semantics with two connexive logics considered by Jarmużek and Malinowski.

Video: click here

Abstract: Anti-exceptionalism about logic is the thesis that logical theories have no special epistemological status. Logical theories are continuous with scientific theories. Contemporary anti-exceptionalists include how they deal with semantic paradoxes as part of the logical evidence data. The recent development of the metainferential hierarchy of S-logics shows that there are multiple options to deal with such paradoxes. LP and 𝖲𝖳 itself are only the first steps of this hierarchy. The logics TS/ST, …, 𝖲𝖳𝜔 are also options to deal with semantic paradoxes. This talk explores the reasons to go beyond the first steps. We show that LP, ST, and the logics of the ST-hierarchy offer different diagnoses for the same evidence. This data is not enough to adopt one of these logics. We will thus have to discuss other elements to evaluate the revision of classical logic. How close should we be to classical logic? Which logic should be used during the revision? Should a logic be closed under its own rules? Could a logic without Modus Ponens be adopted?

Video: click here

Abstract: In this talk I will discuss some features of special classes of collection frames for relevant logics. In particular, I will discuss functional set frames and their connection to Urquhart's semilattice semantics, and I will discuss non-reflexive collection frames and some of the consequences of dropping the reflexivity requirement. This is partially joint work with Greg Restall.

Video: click here

Abstract: One of the all time favorite strategies for defining a non-classical negation proceeds by considering additional truth-values, besides `the True' and `the False', with the intent of using the latter to localise the phenomena of negation-inconsistency and negation-undeterminedness. From a philosophical standpoint, such an approach often translates, with varying degrees of success, into the consideration of `gaps' and `gluts', thought of as truth-values on their own right. From the perspective of the standard Tarskian consequence-theoretic framework, one may claim that the collection of truth-values associated to a given logic constitutes hardly anything beyond a technical expedient used within the so-called `logical matrices' in order to define some convenient notion of entailment. Indeed, at the metalogical level, no more than one or two `logical values' are needed in order to explicate any given consequence relation and the associated one-dimensional `logical theories' that are intended to collect the assertions upon which one happens to be interested. In this talk I will defend the systematic use of a generalized notion of logical consequence that allows for: (i) gappy and glutty reasoning to be naturally captured, at the metalogical level; (ii) a two-dimensional notion of logical theory, containing both assertions and denials, to be explored; (iii) a plurality of inferential mechanisms to cohabit. Furthermore, concerning the choice of logical primitives, I will also argue that truth-values and judgments about logical consequence are advantageously replaced by cognitive attitudes and judgments about logical incompatibility.

Video: click here

Abstract: Dialectica categorical models of the Lambek Calculus were first presented in the Amsterdam Colloquium a long time ago. Following Lambek's lead, we approached the Lambek Calculus from the perspective of Linear Logic and adapted the Dialectica categorical models for Linear Logic to Lambek's non-commutative calculus. The old work took for granted the syntax of the Lambek calculus and only discussed the exciting possibilities of new models for the modalities that Linear Logic introduced. Many years later we find that the work on dialectica models of the Lambek calculus is still interesting and that it might inform some of the most recent work on the relationship between Categorial Grammars and notions of Distributional Semantics. Thus we revisited the old work, making sure that the syntax details that were sketchy on the first version got completed and verified, using automated tools such as Agda and Ott. Ultimately we are interested in the applicability of the original systems to their intended uses in the construction of semantics of Natural Language. But before we can discuss it, we need to make sure that the mathematical properties that make the Lambek calculus attractive are all properly modeled and this is the main aim of this paper. We recall the Lambek calculus with its Curry-Howard isomorphic term assignment system. We extend it with a $\kappa$ modality, inspired by Yetter's work, which makes the calculus commutative. Then we add the of-course modality $!$, as Girard did, re-introducing weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present algebraic semantics and categorical semantics, proved sound and complete for the whole system. Finally, we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.

Video: click here

Abstract: Redstone is a system of components in the Minecraft video game that allows players to build various virtual machines. If we merely consider whether a redstone circuit is powered or not, then redstone circuitry is both functionally complete with respect to classical propositional functions (since it is easy to build, e.g., a NOR gate) and Turing complete (in the slightly attenuated practical sense, often mobilized in computer science discussions, that ignores the finitude of the memory in any particular machine). Much has been made of this as a means to teach basic propositional logic, and ambitious minecraft players have built fully functional (finite memory) universal Turing machines within the game. The Minecraft redstone circuitry system is, however, far more complex than this. Circuits are not merely on or off, powered or unpowered. Instead, the voltage running through a redstone circuit varies from level 0 (unpowered) to level 15 (fully powered). Hence, redstone circuitry involves a sixteen-valued logic. In this talk I will prove that the available redstone components in Minecraft are functionally complete with respect to sixteen-valued truth functions, and in fact are redundant - not all available components are required for the proof. Along the way we will also see some interesting examples of the kinds of computing machines that can be built within Minecraft, including a sixteen-valued memory circuit.

Video: click here

Abstract: Propositional dynamic logic (PDL) is a framework for reasoning about nondeterministic program executions (or, more generally, nondeterministic actions). In this setting, nondeterminism is taken as a primitive: a program is nondeterministic iff it has multiple possible outcomes. But what does "possible" mean, here? This talk explores an epistemic interpretation: working in an enriched logical setting, we represent nondeterminism as a relationship between a program and an agent deriving from the agent’s (in)ability to adequately measure the dynamics of the program execution. More precisely, using topology and the framework of dynamic topological logic, we show that dynamic topological models can be used to interpret the language of PDL in a manner that captures the intuition above, and moreover that continuous functions in this setting correspond exactly to deterministic processes. We prove that certain axiomatizations of PDL remain sound and complete with respect to corresponding classes of dynamic topological models. We also extend the framework to incorporate knowledge using the machinery of subset space logic, and show that the topological interpretation of public announcements coincides exactly with a natural interpretation of test programs. Finally, we sketch a generalization of the topological paradigm in which the distinction between action and measurement (i.e, between functions and opens) is erased, highlighting some preliminary results in this direction.

Video: click here

Abstract: Some disciplines are in the business of telling us what is. Physics, for instance, seems to be a case in point. By contrast, other disciplines such as ethics, jurisprudence and, in the eyes of many, epistemology are normative disciplines. They are characterized by the fact that they concern themselves with normatively assessable subject matters (forms of behavior, practices, actions or mental states) and they essentially involve normative concepts. According to the traditional story, logic too should be grouped with these normative disciplines. However, in recent years a counternarrative has gained currency. It denies that logic is normative. Metalogical statements do not in and of themselves have any implications as to how we ought to think. Inasmuch as there are plausible implications of this kind, they must have their source in additional, non-logical principles, which together with logical principles give rise to them. As the counternarrative takes pains to emphasize, the same is true of virtually any discipline, including paradigmatically descriptive ones. Hence, logic enjoys no special normative status---the traditional story is revealed to be a myth. In this paper, I probe the counternarrative and argue that it begs the question because it presupposes that logic, by its very nature, is concerned with a non-normative subject matter. Rather than adopting a contrary position, I suggest we ought to be pluralists about the subject matter of logic—a meta-pluralism that is orthogonal to standard forms of logical pluralism. My proposed meta-pluralism about logic allows us to treat logic as a formal model, which much like, say, decision theory may have both descriptive and normative applications. I close by developing the notion of logic as a normative model.

Video: click here

Abstract: Logicians and metaphysicians have developed various models and semantics of quantified modal logic. These semantics come with ontological and metaphysical implications regarding the references of singular terms --- such as the necessity of Hesperus being Phosphorus. My primary question in this talk is how these metaphysical facts can be a posteriori facts, as opposed to a matter of logic, of the sort that a cognizer can come to know. The goal of this talk is to give a semantics that sheds new light on this aposteriority. I will take an approach in terms of intensional logic that treats all singular terms, predicates, and quantifiers as uniformly intensional. Combined with epistemic logic, my approach will provide a semantics and logic in which metaphysical principles regarding cross-world reference are substantial facts that a cognizer can both learn and use in their modal reasoning and theorizing.

Video: click here

Abstract: Categorial logic has been on the map at least since the publication of Bill Lawvere's "Adjointness in Foundations" in 1969. But in philosophical quarters, it hasn't received as much attention as I think it deserves. In part, this is likely due to a presentational issue: categorial logic is often presented in a way that assumes deep familiarity with much more category theory than philosophers typically possess. The first purpose of this talk is to present the basics of categorial logic---in particular, an elementary version of the theory of hyperdoctrines for classical logic---in a way that presupposes very little in the way of knowledge of category theory. The second goal of the talk is to give reasons for philosophers to be interested in the perspective hyperdoctrines offer on some traditional questions. Overall, my hope is that by the end of the talk, at least a few of you will have been convinced that the hyperdoctrinal perspective offers the possibility of illuminating problems either logical or philosophical that you've long wrestled with.

Video: click here

Abstract: Programs change quickly, and proofs of program correctness must change quickly alongside the programs whose correctness they prove. I will discuss my work on tools to automate the process of changing proofs. At the core of these tools is a set of proof transformations or strategies to transform proofs, much like program transformations inside of compilers transform programs. These proof transformations operate over proofs in a proof assistant that is based on the Calculus of Inductive Constructions, and take advantage of the wealth of information that constructive proofs contain. With them, automation can repair broken proofs, port proofs from one development to another, implement proof strategies natural to humans like "similarly," and even optimize proofs.

Video: click here

Abstract: This talk will introduce a new logical system in which formulas represent "effects" (e.g. of argumentation), such that these "effects" correspond formally to vectors. In a slogan: content is a vector. The logic involves a deductive system, a semantics with an appropriate notion of logical consequence, and extensions to similarity, inductive logic, and belief revision. The resulting system may be interpreted in probabilistic terms, and it can be applied to logically reconstruct some well-known problems and methods from cognitive psychology, computational linguistics, and machine learning.

Abstract: In his last article, "Undecidability without Arithmetization” (Studia Logica 79.2, 2005, pp.163-230, https://philpapers.org/rec/GRZUWA-2) Grzegorczyk considers a first-order theory TC in the signature of one binary function and two constants, finitely axiomatised by natural axioms, such that the two-generated model of TC is precisely the set of all nonempty words over a two-letter alphabet. He claims that TC is undecidable. Grzegorczyk's proof is both interesting and problematic. It is interesting because it proceeds from first principles, using a Goedelian diagonalisation argument, but based intuitively on Grelling "heterological" paradox rather than on the liar. It is problematic, because the notion of computability / decidability it uses is also defined from first principles. We (mostly Yao) proved that everything computable in Grzegorczyk sense is Turing computable, but whether the converse is true is not clear. At least not to us. I will present Grzegorczyk's proof, or as much of it as Yao and me currently understand. This is work in progress.

Abstract: The recent discovery and exploration of mixed metainferential logics such as TS/ST, (ST/TS)/(TS/ST), and so forth is a breakthrough in our understanding of nontransitive and nonreflexive logics. Moreover, this exploration poses a new challenge to theorists, like me, who have appealed to ST's similarities to classical logic in defending it, since some metainferential logics, such as those mentioned above, seem to bear even more similarities to classical logic than ST does. It can seem that we should replace ST with TS/ST, or with (ST/TS)/(TS/ST), or with the limit of this sequence, of which ST is only the first step. I think this seeming is misleading: for certain purposes, including purposes for which it has been recommended, ST is the right choice, and metainferential hierarchies give us no reason to change this view. ST is indeed only the first step on a grand metainferential adventure; but for understanding the speech acts of assertion and denial, and their role in the norms that constitute linguistic meaning, one step is enough. This talk aims to explain and defend that claim.

Video: click here

Abstract: This paper develops a theory of the semantics and probability of conditionals and statements involving epistemic modals, building on existing informational accounts. The theory validates a number of plausible principles linking probability and modality, including Stalnaker’s Thesis, the principle that the probability of a conditional is the conditional probability of the consequent given the antecedent. Thus the theory escapes so-called triviality results, which are often taken to show that the vindication of these principles is impossible. To achieve this, we deny one of the assumption that leads to triviality: that rational agents update their credences via conditionalization. In place of conditionalization, we offer a new rule for how rational agents should update their credences over time, which we call Hyperconditionalization. Hyperconditionalization and conditionalization agree in their results when nonmodal statements are at stake, but differ crucially for the modal case.