Core type theory

David Ripley

The Curry-Howard correspondence between intuitionistic logic and the simply-typed lambda calculus forms an important bridge between logical and computational research. This talk develops a variant typed lambda calculus, called “core type theory”, that stands in a similar correspondence to Neil Tennant’s “core logic” (fka “intuitionistic relevant logic”), and shows some basic (and some surprising!) results about this calculus.

Variable Free Semantics: Putting competition effects where they belong

Pauline Jacobsen

This talk will have two parts. First I will discuss the approach to semantics making no use of variable names, indices, or assignment functions that I have advocated in a series of papers (see especially Jacobson, 1999, Linguistics and Philosophy and 2000, Natural Language Semantics, also exposited in Jacobson 2014 textbook Compositional Semantics, OUP). There are a number of theoretical and empirical advantages to this approach, which will be just briefly reviewed. To mention the most obvious theoretical advantage: the standard use of variable names and indices in semantics requires meanings to be relativized to assignment functions (assignments of values to the variable names), adding a layer to the semantic machinery. This program eliminates this and treats all meanings as ‘healthy’ model theoretic objects (the meaning of a pronoun, for example, is simply the identity function on individuals, not a function from assignments to individuals). I will then show a new empirical payoff, which concerns competition effects found in ellipsis constructions. These competition effects have gone under the rubric of MaxElide in the linguistics literature. One example centers on the contrast in (1) (on the reading where each candidates hope is about their own success):

  1. a. Harris is hoping that South Carolina will seal the nomination for her, and Warren is too. (= ‘hoping that it will seal nomination for her (Warren)’)
    b. ?*Harris is hoping that South Carolina will seal the nomination for her, and Warren is also hoping that it will. (= ‘seal the nomination for her (Warren)’)

The ‘standard’ wisdom is there is a constraint in the grammar that when material is ‘missing’ (or, ‘elided’) if a bigger constituent can be elided, the bigger ellipsis is required. Why the grammar should contain such a constraint is a total mystery; moreover I and others have argued elsewhere that grammatical competition constraints represent a real complication in the grammar. When there are competition effects they should be located in speakers and hearers (we know that speakers and hearers do compute alternatives – Gricean reasoning, for example, is based on that assumption). Under the variable free account, the missing material in (1a) is of a different type than that in (1b). In (1a), the listener need only supply the property ‘be an x such that x hopes that SC will seal nomination for x‘ which is the meaning of the VP in the first clause. In (1b) what must be supplied is the 2-place relation ‘seal the nomination for’ (note that this is in part because the pronoun her in the first clause is not a variable, and so [[seal the nomination for her]] is the function from an individual x to the property of sealing the nomination for x, which in turn is the two place relation named above. The competition effect is thus about types not size, and can be given a plausible explanation in terms of communicative pressures. Assuming that meanings of more complex types are more difficult to access than those of simpler types, there is a pressure for speakers to choose the simpler type ellipsis. The type competition story crucially relies on the claim that expressions containing pronouns unbound within them denote functions from individuals to something rather than functions from assignment functions.

How to deal with semantic paradox (Hint: accept defeat)

Steven Dalglish

I contend that semantic paradox shows we should regard the rules of inference for semantic notions as defeasible. Truth is a prominent semantic notion for which semantic paradox poses a problem, and so a first step in solving semantic paradox is handling a semantic notion of truth. This talk investigates how defeasible rules of inference for a semantic notion of truth can form the basis for a successful truth-conditional theory of meaning. I start by using Default Logic for representing the rules of inference for a truth predicate as defeasible, before adding preferences over rules and modifying the criteria for defeat.

A Dynamic Solution to the Liar Paradox

Martin Pleitz

The Liar paradox arises when we combine the assumption that a sentence can refer to itself with our naïve notion of truth and apply our unrevised logic. Most current approaches to the Liar paradox focus on revising our notion of truth and logic because nowadays almost everyone is convinced that there are self-referential sentences. I will argue against this conviction. My argument starts from observations about the metaphysics of expressions: A meaningful expression is based in a syntactic expression which in turn is based in a non-semiotic object, and these are pairwise distinct. As all objects of this three-fold ontology exist only relative to contexts, we can import ideas from tense logic about how existence and reference can interact in a contextualist metaphysics. Semantico-metaphysical reasoning then shows that in this dynamic setting, an object can be referred to only after it has started to exist. Hence the self-reference needed in the Liar paradox cannot occur, after all. As this solution is contextualist, it evades the expressibility problems of other proposals.

Proof-theoretic Harmony

Intensional aspects from a second-order perspective

Luca Tranchini

The talk will focus on harmony, the widely discussed condition that two collections of introduction and of elimination rules for a certain logical constant should satisfy in order to perfectly match each other. Attention will be restricted to rules for propositional connectives in single-conclusion natural deduction format.

I will first argue that a decent criterion of harmony should be (hyper-)intensional, in the sense that taken two equivalent collections of elimination rules (i.e. such that each rule of the first collection is derivable from the rules in the second collection, and vice versa), it may well be that only one of the two collections is in harmony with a given collection of introduction rules.

To precisely formulate an intensional criterion for harmony we propose to modify the (extensional) criterion for harmony recently proposed by Schroeder-Heister (for short SH-harmony) and based on the idea that to any collection of introduction and of elimination rules one can associate a formula of intuitionistic propositional logic with propositional quantification (IPC2). Two collections of introduction and elimination rules for a certain connective are in SH-harmony if the two formulas associated to them are interderivable in IPC2.

An intensional criterion is achieved by imposing on the two formulas a condition stricter than intederivability: isomorphim. We will present the notion of isomorphism (well-known from category theory and computational study of proof systems), stress its significance for proof-theoretic semantics, and finally apply it to clarify the relationship between different ways of generating collections of elimination rules from a given collection of introduction rules known in the literature.

A Modal Theory of Free Choice Sequences

Ethan Brauer

Free choice sequences (also called ‘infinitely  proceeding sequences’) are a concept from intuitionistic mathematics that are central to the development of the intuitionistic theory of the continuum. Free choice sequences have, however, been largely rejected or ignored both by classical and other constructive mathematicians. In this talk I argue that the objections to free choice sequences can be overcome by grounding the concept in our temporal intuition and formalizing the theory in modal logic. I will present a theory of free choice sequences as a modal extension of classical second-order arithmetic. The resulting theory is able to prove modal versions of the intuitionist’s axioms for so-called lawless sequences, suffices for the development of a theory of real number generators, and captures many results distinctive of intuitionistic analysis including the non-existence of functions on real numbers with definable discontinuities.

Indexicals, Time, and Compositionality

Peter Pagin

Kaplan’s official argument in “Demonstratives” for Temporalism, the view that some English sentences express propositions that can vary in truth value across time, is the so-called Operator Argument: temporal operators, such as “sometimes”, would be vacuous without such propositions.

Equally important is the argument from compositionality. Without temporal propositions, the sentences

(I) It is raining where John is
(2) It is raining where John is now

would express the same proposition. But they embed differently:

(3) Sometimes, it is raining where John is
(4) Sometimes it is raining where John is now

(3) and (4) express distinct propositions, so if they both are of the form “Sometimes, p”, and if (1) and (2) express the same proposition, we have a violation of compositionality.

In this talk it is shown that with Switcher Semantics, which allows for a generalized form of compositionality, we can have the result that (1) and (2) agree in content when unembedded (assertoric content) but differ in content when embedded under temporal operators (ingredient sense).

We can also show that Switcher Semantics, over Kaplan’s models, preserves the validities in the Logic of Demonstratives. All in all, the arguments for Temporalism are substantially undermined.

The Explanatory Value of Category Theory

Ellen Lehet

Category theory has proven to be applicable across all of mathematics. In some sense this is not surprising because category theory was created for the purpose of application (specifically, application to algebraic topology). But I will argue that the significance of category theory extends past its applicability — in particular, there is a significant explanatory benefit. The question of what constitutes a mathematical explanation is of perennial interest to philosophers. Reflection on category theory’s unique role in mathematics unearths some features of mathematical explanation that are not often made explicit and that philosophers have tended not to notice.

There are many ways that category theoretic methods provide explanations. For instance, important results in different areas of mathematics are unified by the fact that they are all corollaries of the same category theoretic theorem, such as the theorem that right adjoints preserve limits. Or consider the ways of defining structures in category theory with universal properties — the whole perspective sheds light on how constructions from different domains are related to one another. The categorical product for instance, unites many seemingly unrelated mathematical constructions such as the Cartesian product, union, and conjunction. Such examples introduce both generalization and unification within mathematics. Moreover, this unification allows for meaningful and surprising mathematical analogies to arise. These gen- eralizations and analogies are explanatory and result from the structural features of category theory.

In order to highlight the explanatory value of category theory, I will first provide a characterization of the structure unique to category theory. It is this structure that makes category theory apt for producing explanations. With a clear picture of category theoretic structure, I will present a few examples that illustrate how category theory proves to be explanatory — in particular, how the structural features of category theory are explanatory.

Anti-Exceptionalism and Explanations in Logic

Ole T. Hjortland & Ben Martin

According to logical anti-exceptionalism we come to be justified in believing logical theories by similar means to scientific theories. This is often explained by saying that theory choice in logic proceeds via abductive arguments (Priest, Russell, Williamson, Hjortland). Thus, the success of classical and non-classical theories of validity are compared by their ability to explain the relevant data. However, as of yet there is no agreed upon account of which data logical theories must explain, and subsequently how they prove their mettle. In this paper, we provide a non-causal account of logical explanation, and show how it can accommodate important disputes about logic.

Saving Truth for Intuitionists

Andrew Tedder (joint work with Stewart Shapiro)

We consider a handful of solutions to the liar paradox which admit a naive truth predicate and employ a non-classical logic, and which include a proposal for classical recapture. Classical recapture is essentially the property that the paradox solvent (in this case, the non-classical interpretation of the connectives) only affects the portion of the language including the truth predicate – so that the connectives can be interpreted classically in sentences in which the truth predicate does not occur.

We consider a variation on this theme where the logic to be recaptured is not classical but rather intuitionist logic, and consider the extent to which these handful of solutions to the liar admit of intuitionist recapture by sketching potential ways of altering their various methods for classical recapture to suit an intuitionist framework.