1st SNS-KCL Logic and Philosophy of Mathematics Meeting

The Logic and Philosophy of Mathematics research clusters at Scuola Normale Superiore and King's College London have expanded significantly in recent years, cultivating vibrant research communities. This two-day workshop offers researchers from both clusters an opportunity to present their work and exchange ideas, promoting collaboration between the two departments. 

Organized by PRIN project PUMa "Proof and understanding in mathematics. Purity of methods, simplicity, and explanation in mathematical reasoning" (Principal Investigator, prof. Mario Piazza, SNS) 

Speakers:

Graham Leigh (University of Gothenburg)

Lavinia Picollo (National University of Singapore)

Matteo Bizzarri (SNS)

Pietro Brocci (SNS)

Maria Beatrice Buonaguidi (KCL)

Pedro Del Valle-Inclan (SNS)

Pablo Dopico (KCL)

Mahin Hossain (KCL)

Carlo Nicolai (KCL)

Andrea Sabatini (SNS)

Matteo Tesi (TU Wien)

Pietro Vigiani (SNS)

Schedule:

12th June

13th June

Abstracts

Lavinia Picollo:  Topic-neutrality without semantics

The notion of logical consequence relies on the distinction between logical and non-logical constants. It is commonly believed that the defining characteristic of logicality is topic-neutrality, but the most popular accounts of topic-neutrality all have well-known problems. In recent work, Halbach suggests that the issue lies in the appeal to domains, and puts forward a new criterion that eliminates them. Some problems, however, still remain, and others are created. In this talk I suggest an alternative topic-neutrality criterion (originated in early work by Lindenbaum and Tarski) that avoids all new and most remaining issues by doing away with semantic notions altogether.

Matteo Bizzarri: Proof Theory and Music Analysis: A Novel Approach (j.w.w. Satoshi Tojo)

Music and language are thought to share a common origin, leading to numerous research endeavors that have sought to analyze music through a compositional approach, grounded in linguistic grammar rules. In this study, we extend and refine this method, demonstrating that the analysis can be systematically represented using rigorous proof theory, akin to how formal logic elucidates natural language semantics. Our approach involves the use of sequent calculus to construct a proof, notably extending Lambek calculus for categorial grammar to a labeled version. The introduction of labels enables each term within a sequent to be interpreted as a chord with a specified key (tonality). This labeling allows us to precisely determine the grammatical validity of a given sequence of chords. Given that music grammar varies with genre and era, our formalism is designed to accommodate flexible addition and reduction of applicable rules. Additionally, we show that this process of analysis is reversed in Tableaux style, to simulate the process of composition. This methodology not only enhances our understanding of music from a linguistic perspective but also provides a versatile framework for adapting to the evolving nature of musical grammar.

Pietro Brocci: The justificatory power of classical disquotational truth.

Principles for truth, starting from relatively elementary theories of arithmetic, can justify mathematical theories of significantly greater strength. In particular, disquotational truth is well-suited as a tool to discover new mathematical truths. For example,  we can iteratively employ formalized soundness statements for the disquotational theory, i.e. reflection principles, providing foundations for predicative mathematics. As it is done in a non-classical setting by Fischer, Nicolai, Horsten (2021).

The limits of predicativity, as understood by Feferman, are by no means uncontroversial. Recent results suggest that ordinal much bigger than the Feferman-Schutte can be predicatively defined. Moreover, the reflection strategy employs new principles for truth that are not conservative over the base theory. Following McGee (2005), I argue that conservativity is a necessary safety measure to ensure that the axioms for truth are akin to an explicit definition, i.e. they do not have any theoretical impact but serve to define a new component of the language.  

I propose a different approach to overcome these shortcomings: I provide a conservative addition to the definition of a theory of disquotational truth, by employing a principle introduced in Cantini (1989). This theory provides foundations for a portion of impredicative mathematics. Furthermore,  since this is done in classical logic it makes the move to non-classical disquotational truth less appealing.

Maria Beatrice Buonaguidi: What's the HYPE about hyperintensional logics? Fine-grained criteria for hyperintensionality

Traditionally, hyperintensional contexts and operators are defined in a negative way, namely, as contexts and operators which do not license unrestricted intersubstitutivity for necessary equivalents, or for logical equivalents (Cresswell 1975, Nolan 2014). I argue that this notion of hyperintensionality is too vague, especially when it needs to be used to judge whether a logical consequence relation counts as hyperintensional.

Starting by challenging a criterion for hyperintensionality for a logical consequence relation suggested by Odintsov and Wansing (2021), I will present several different criteria for a logic to be hyperintensional. This will help me draw a diagnosis of hyperintensionality as, simply, some degree of asymmetry between preservation of truth and preservation of falsity. Furthermore, I will argue that hyperintensionality can show up at different levels for different consequence relations, licensing a spectrum of hyperintensional behaviour: as a case study of this, I will consider N-logics and HYPE (Leitgeb 2019).

Pedro Del Valle-Inclan: Carnap’s problem, definability and compositionality

In his Formalization of Logic (1943) Carnap pointed out that there are non-normal interpretations of classical logic: non-standard interpretations of the connectives and quantifiers that are consistent with the classical consequence relation of a language.

Different ways around the problem have been proposed. In a recent paper, Bonnay and Westerståhl argue that the key to a solution is imposing restrictions on the type of interpretation we take into account. More precisely, they claim that if we restrict attention to interpretations that are (a) compositional, (b) non-trivial and (c) in the case of the quantifiers, invariant under permutations of the domain, Carnap's Problem is avoided.

This paper has two goals. The first is to show that Bonnay and Westerståhl’s solution to Carnap's Problem doesn't work. The second is to argue that something similar to their proposal seems to do the job.

The problems with Bonnay and Westerståhl’s approach trace back to issues concerning the (un)definability of subsets of the domain of first-order structures, as well as to the compositionality of first-order languages. After expanding on these problems, I'll propose a way to modify Bonnay and Westerståhl’s account and solve Carnap's Problem.

Pablo Dopico: An axiomatic theory of truth for maximal consistent supervaluations and its schematic extension.

As is well-known, Andrea Cantini proposed an axiomatization of Kripke fixed-point semantics constructed over the supervaluationist scheme vc which he called $\mathrm{VF}$, and proved that the theory was sound with respect to the fixed-point models generated by that scheme. Moreover, he showed that $\mathrm{VF}$ was a remarkably strong theory, matching the strength of the impredicative theory $\mathrm{ID}_1$.

In recent work with Daichi Hayashi, we have undertaken this task for the Kripkean theories constructed over the schemes vb and mc providing the sound theories $\mathrm{VF}^-$ and $\mathrm{VFM}$, respectively. In this talk, I will initially summarise these results, and will then move on to consider the schematic extension, in the sense of Feferman (1991), of the theory $\mathrm{VFM}$. Thus, I provide a model for this theory, and carry out its proof-theoretic analysis. The main result presented in the talk will be the establishment that this schematic extension is as proof-theoretically strong as the theory $\mathrm{RA}_{<\Gamma_0}$.

 Carlo Nicolai: Instatiation Patterns. 

Concerns about the expressive limitations of type-theoretic approaches to properties may lead philosophers to favour type-free options, typically formulated in a first-order language. Given the success of standard set theory and the iterative conception, there have been attempts to formulate theories of properties based on ZFC, justified by an iterative picture. Such approaches, although prima facie type-free, ban any form of self-predication/instantiation, which is in some cases desirable for properties, if  not for sets. An obvious alternative is to explore theories of properties based on non-wellfounded set theories and the conceptions on which they are based. In the talk I will discuss and develop this alternative.

Andrea Sabatini: A new Gentze-style approach to default logics

In this talk, we investigate default reasoning from a structural proof-theoretic perspective. We introduce hybrid hypersequent calculi for propositional default logics, where extra-logical rules directly capture default rules, while parallel composition of sequents and antisequents formalizes contrary updating on the conclusions of extra-logical rules. We establish the admissibility of structural rules and the invertibility of logical rules, showing that cut-free proofs exhibit a weakened form of analyticity. Next, we prove that specific hybrid hypersequent calculi are sound and weakly complete with respect to credulous consequence based on Lukaszewicz extensions. Moreover, we propose a hypersequent-based decision method for skeptical consequence which circumvents the need for early computation of all extensions. Lastly, we show how the notion of control set can be modified so as to get strongly complete sequent calculi for credulous consequence based on Lukaszewicz extensions.

Pietro Vigiani: Entailment and Containment: A Ternary Approach to Information and Topic Inclusion 

Relevant containment logics, as developed by Richard Sylvan, fuse a topic-theoretic framework, for the analysis of containment, to Routley-Meyer semantics, for the analysis of entailment. However, Sylvan’s framework posits an unfortunate discord between how topics are handled at logical and non-logical worlds, thus failing to match the harmony in the meaning of connectives in relevant logics. In this paper, we follow the intuitions underlying relevant logics’ ternary relation semantics to develop a sound and complete axiomatisation of relevant containment logics with a harmonious treatment of the truth and topical conditions underlying, respectively, information and topic inclusion.

Contact:

Pietro Brocci (pietro.brocci@sns.it)

Maria Beatrice Buonaguidi (maria.buonaguidi@kcl.ac.uk)

Pablo Dopico (pablo.dopico@kcl.ac.uk)