Author: mar08022

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.

Computational Cognitive Modeling for Syntax and Semantics

Adrian Brasoveanu

I introduce a typical experimental task in psycholinguisticsself—paced reading—and show how to build end-to-end simulations of a human participant in such an experiment; end-to-end means that we model visual and motor processes together with specifically linguistic processes (syntactic and semantic parsing) in a complete model of the experimental task. The model embeds theoretical hypotheses about linguistic representations and parsing processes in an independently motivated cognitive architecture (ACT-R). In turn, the resulting cognitive models can be embedded in Bayesian models to fit them to experimental data, estimate their parameters and perform quantitative model comparison for qualitative theories.

Unveiling the constructive core of classical theories

Sara Negri

Unveiling the constructive core of classical theories: A contribution to 90 years of Glivenko’s theorem

Glivenko’s well known result of 1929 established that a negated propositional formula provable in classical logic is even provable intuitionistically. Similar later transfers from classical to intuitionistic provability therefore fall under the nomenclature of Glivenko-style results: these are results about classes of formulas for which classical provability yields intuitionistic provability. The interest in isolating such classes lies in the fact that it may be easier to prove theorems by the use of classical rather than intuitionistic logic. Further, since a proof in intuitionistic logic can be associated to a lambda term and thus obtain a computational meaning, such results have more recently been gathered together under the conceptual umbrella “computational content of classical theories.” They also belong to a more general shift of perspective in foundations: rather than developing constructive mathematics separately, as in Brouwer’s program, one studies which parts of classical mathematics can be directly translated into constructive terms.

We shall survey how Glivenko-style results can be easily obtained by the choice of suitable sequent calculi for classical and intuitionistic logic, by the conversion of axioms into inference rules, and by the procedure of geometrization of first order logic.