Formalization in Logic, Language, and Mathematics Conference

Andrew Arana, Université de Lorraine, Archives Poincaré
Meaning and interpretation in mathematics

Interpretability in logic formalizes the notion of a “dictionary” for translating statements of one theory into statements of another, in such a way that provability is preserved. For instance, translating “geodesic on the pseudosphere” to “Euclidean straight line” leads by way of Beltrami’s theorem to the observation that hyperbolic geometry is interpretable in Euclidean geometry. Interpretability is thus a way to capture a notion of translation that preserves provability. One might seek to take the dictionary metaphor further and ask whether interpretability preserves meaning as well. In this talk I will address this question by taking into account the constraint on mathematical proof known as “purity of methods”, the proof ideal that says that a proof of a theorem should avoid what is foreign or extraneous to that theorem. Following Hilbert, purity can be understood in terms of meaning, by what belongs to the content of the theorem being proved. Whether a given proof is pure, then, comes down to the meaning of what is proved. It is easy to find algebraic statements interpretable in geometric theories and vice-versa. If meaning is preserved by interpretability, a pure proof of a geometric theorem could employ algebraic statements suitably interpreted in geometric terms. This would be to reject as empty the age-old attempts of mathematicians to develop the autarky of mathematical domains. This talk's general thesis is that while interpretability might seem to present difficulties for assessing purity attributions, one must be quite careful in the lessons that one draws from interpretability, and as a result these alleged difficulties are not so clear-cut.

Ainsley May, University of California, Irvine
Meaning in Mathematics: a folkloric approach.

There is a huge variety of mathematical theorems, yet almost every philosophical account of meaning holds that all mathematical theorems have the same meaning. Such accounts conflict with mathematical practice and cannot distinguish between different mathematical theorems.

In response, I propose a preliminary account of mathematical meaning motivated by the key role played by inferences in mathematics. Many people have noted the importance of inferences to mathematics, with some even suggesting that they play a constitutive role in meaning. However, very little literature exists actually fleshing out such an account, as such I call my attempt to do so, a folkloric account. In this talk I introduce the folkloric account and highlight some of its strengths and weaknesses with the help of examples.

Manuel Rebuschi, Université de Lorraine, Archives Poincaré
Cross-World Subjunctive Modal Logic: Some Philosophical Applications

Kai Wehmeier's subjunctive modal logic (SML) is an enrichment of first-order modal logic (FOML) with indicative and subjunctive markers, so that one can quantify and select objects either in the domain of some reached possible world or in the actual world. Another aspect of SML is the involvement of cross-world extensions of predicates. Wehmeier used his logic to account for cross-world comparisons and for conditionals. In this talk, I will present some philosophical applications of cross-world predication, pertaining to aesthetics, to philosophy of language, and maybe to a few other fields.

Will Stafford, University of Bristol
Is the Proof-Theoretically Valid Logic Intuitionistic?

Several recent results bring into focus the superintuitionistic nature of most notions of proof-theoretic validity, but little work has been done evaluating the consequences of these results.  Proof-theoretic validity claims to offer a formal explication of how inferences follow from the definitions of logic connectives (which are defined by their introduction rules).  This paper explores whether the new results undermine this claim.  It is argued that, while the formal results are worrying, superintuitionistic inferences are valid because the treatments of atomic formulas are insufficiently general, and a resolution to this issue is proposed.

Toby Meadows, University of California, Irvine
When are two models of computation equivalent?

There is a growing literature focused on understanding when two theories are equivalent for some intents and purposes. The main engine of this work is the theory of relative interpretation. Results from this field can be put to a variety of - sometimes controversial - philosophical purposes. However, the most famous and philosophically significant equivalence results are those used as evidence for the Church-Turing thesis. For example, it is a piece of folk knowledge that Turing machines and register machines can be used to execute the same functions. Nonetheless, this equivalence seems quite weak when compared to those obtained between theories. My goal in this paper is to talk about an ongoing project to better understand the nature of the equivalences that obtain between models of computation. 

Olivier Bruneau, Université de Lorraine, Archives Poincaré
Encyclopedias as markers of heritage building: Fluxion articles in British encyclopaedias, 1704-1850

Résumé en français : Si on considère la patrimonialisation comme un processus mettant en scène le passé et le présent en vue de les présenter pour l'avenir, alors les encyclopédies sont de bons candidats pour évaluer ce qui fait patrimoine. Nous nous proposons d'étudier sur le temps long (1704-1860) les entrées \textsc{Fluxion} des encyclopédies britanniques. À l'aide de ce corpus constitué de plus de trente articles, il sera alors possible d'identifier plusieurs marqueurs qui participent à la patrimonialisation des mathématiques~: une référence à l'histoire, les sources d'inspiration et les références bibliographiques.

Abstract: If we consider heritage as a process of exhibiting the past and the present in order to present them for the future, then encyclopedias are good candidates for assessing what constitutes heritage. We propose to study the \textsc{Fluxion} entries in British encyclopaedias over a long period of time (1704-1860). With the help of this corpus of more than thirty articles, it will then be possible to identify several markers that participate in making mathematics into a heritage: a reference to history, sources of inspiration and bibliographical references.

Curtis Mason, University of California, Irvine
Frege on the Unity of Calculus Ratiocinator and Lingua Characterica

In this talk, I aim to reconstruct Frege’s conceptions of lingua characterica and calculus ratiocinator, focusing especially on the manner in which he thought these two kinds of system are related to one another. Towards this end, I develop two characterizations of what Frege meant by these terms. The first characterization, which I call the “descriptive characterization”, outlines the features Frege thought a symbolic logic must possess in order to be a calculus ratiocinator or a lingua characterica. The second characterization, which I call the “functional characterization”, focuses on what Frege thought these two kinds of system should be used for. On the basis of these two characterizations, I argue that Frege thought a lingua characterica should at the same time be a calculus ratiocinator, and vice versa. The first direction of this claim – namely, that for Frege, every lingua characterica should at the same time be a calculus ratiocinator – already exists and is well-defended in the literature. However, the other direction of this claim – namely, that for Frege, every calculus ratiocinator should at the same time be a lingua characterica – is novel. In clarifying Frege’s conception of these notions, we achieve a better understanding of how and why he thought that logic should “advance science”. 

Kai Wehmeier, University of California, Irvine
Is there a tension between variable binding and extensionality?

Perhaps surprisingly, the title question has received different answers in the literature. I will reconstruct the reasoning underlying each of the two answers that have been given -- not to spoil anything, they are: NO (the "traditional" answer) and YES (the "insurgent" answer) -- before trying to adjudicate the matter. Adjudication is easy in one sense (strictly speaking, the traditional camp is right and the insurgent, wrong) but difficult in another, since the insurgents are better seen as disputing the very rules of the extensionality game, rather than the traditional answer to the question when understood on the traditionalist's terms.