Formalize!(?) - 3 

Schedule

15:15 - 15:30 Introduction

15:30 - 16:00 Talk 1: Zoe McConaughey (Lille): "Formalizing Aristotle's syllogistic. Towards a dialogical approach"
16:05 - 16:35 Talk 2:  Benjamin Zayton (MCMP, LMU Munich) "Open Texture, Rigor, and Proof" 

16:35 - 17:00 Break

17:00 - 17:30 Talk 3: Victor Aranda (Complutense University of Madrid) "Models of non-classical versions of Church's type theory"
1̶7̶:̶4̶0̶ ̶-̶ ̶1̶8̶:̶1̶0̶ ̶T̶a̶l̶k̶ ̶4̶:̶ ̶A̶d̶r̶i̶e̶n̶ ̶C̶h̶a̶m̶p̶o̶u̶g̶n̶y̶ ̶(̶P̶a̶r̶i̶s̶ ̶1̶)̶ ̶"̶A̶b̶s̶t̶r̶a̶c̶t̶ ̶F̶o̶r̶m̶a̶l̶i̶z̶a̶t̶i̶o̶n̶"̶ (Cancled)
17:40 - 18:10 Talk 4: Pablo Rivas-Robledo (University of Genova) "Self-reference in Gödel sentences"
18:20 - 18:50 Talk 5: Paul Hasselkuß (U Düsseldorf) "Assessing Surveyability. Reframing the Debate on Computer-Assisted-Proofs"
18:50 - 19:00 closing

19:00 - 20:00 The room will stay open for unofficial discussion

Abstracts and title (in order of the talks): 

"Formalizing Aristotle's syllogistic. Towards a dialogical approach" by Zoe McConaughey (Lille).

Abstract: The Greek philosopher Aristotle (4th c. BCE), by developing his syllogistic, is considered the father of formal logic. However, since Lukasiewicz's pioneering work formalizing syllogistic with modern formal logic, many other formalizations have been proposed using various logical frameworks, ranging from axiomatics to natural deduction and operationist logic. The modern formal reconstructions of syllogistic, the origin of logic, are as diverse as the interpretations provided. Without going into the problems of interpretation, I will briefly present Aristotle's syllogistic as can be found in his texts, the now mainstream natural deduction formalization of it, and elements towards a dialogical formalization of syllogistic I have developed, and which I claim to be closer to Aristotle's logical project. Through these problems regarding the modern formalization of Aristotle's syllogistic lies the question of the nature of logic, today and at its origins.

"Open Texture, Rigor, and Proof" by Benjamin Zayton. [The topic of the talk might still be subject to change]

Abstract: Open texture is a kind of semantic indeterminacy first systematically studied by Waismann. In this paper, extant definitions of open texture will be compared and contrasted, with a view towards the consequences of open-textured concepts in mathematics. It has been suggested that these would threaten the traditional virtues of proof, primarily the certainty bestowed by proof-possession, and this suggestion will be critically investigated using recent work on informal proof. It will be argued that informal proofs have virtues that mitigate the danger posed by open texture. Moreover, it will be argued that while rigor in the guise of formalisation and axiomatisation might banish open texture from mathematical theories through implicit definition, it can do so only at the cost of restricting the tamed concepts in certain ways.

"Models of non-classical versions of Church's type theory" by Victor Aranda 

Abstract: Church's type theory is a very expressive logical system which is well suited to the formalization of mathematics. In the last few years, Areces et al. ("Completeness in Hybrid Type Theory", 2014), Manzano et al. (Completeness in Equational Hybrid Propositional Type Theory, 2019) and Manzano et al. ("Hybrid Partial Type Theory", forthcoming) have proposed different non-classical versions of this logic. In this contribution, we will study the models of these higher-order systems to evaluate its capacity to formalize ordinary mathematical practice. In addition to this, we will describe the models of partial versions of Henkin's propositional type theory, which work especially well in contexts of lack of information and indeterminacy.

"Abstract Formalization" by Adrien Champougny

Abstract: 

Reverse mathematics is a branch of mathematical logic that is used, a certain theorem t of every day mathematics being given, to evaluate what is the weakest formal system that proves it. To do this, the idea is first to prove t in a formal system S (thus showing that S is a sufficient condition for t) and then to prove that the axioms of S follow from t (or in other words, S is a necessary condition for t). We call this kind of result a reversal. In practice most reversals are obtained in a framework called second order arithmetic and S is usually one of the so-called “Big Five” (which are subsystems of second-order arithmetic).

Mathematical explanation on the other hand is an old notion that one can track back at least to Aristotle. The idea is that a mathematical explanation of t is (at least typically) a proof of a t that does not merely show that t follows from a given system S but that S is actually the reason why t is true. One of the most famous account of mathematical explanation has been given by Philip Kitcher, starting in 1981. His idea is to consider explanation not from a local point of view (has in the case that we have just mentioned, where the explicandum is just the theorem t and the exlplicans is a proof of t satisfying certain conditions) but from a more holist point : we will say that a theory (or to use his own terms, a systematization) S provides an explanation for a whole field of knowledge F. To make that judgment, we need to show how “description of many phenomenas” (elements of F) can be derived following the same patterns (patterns of S) of derivation which thus reduces “the number of type of facts that we have to considered as ultimate (or brute) ”(axioms of S). In this presentation, I want to argue that the system of the Big Five can provide an explanation of this kind. I will make this case by looking at a few examples of theorems that are proved in systems of the Big Five, showing that their proofs in those systems share a common structure (i.e. they use the same patter

of derivation) which was not the case of their “natural” proofs.

"Self-reference in Gödel sentences " by Pablo Rivas-Robledo

Abstract: 

It is common to present Gödel sentences as self-referential statements. However, little attention has been paid to how exactly Gödel sentences are self-referential, which has led philosophers and mathematicians to make comparisons or equivalences with natural language and to argue that Gödel sentences behave like indexical or demonstrative self-referential statements. In this talk, I will argue that self-reference in first-order arithmetic behaves neither like an indexical nor a demonstrative; instead, it functions like a description, i.e., a sentence that describes itself. To this end, I will explain the mechanism of self-reference involved in the construction of gödel sentences.It turns out that in the language of first-order arithmetic the attainment of self-reference is much more spurious than in natural language. Then I will assess whether the mechanism of arithmetic is similar to the tools we have in natural language to make self-referential statements. I will conclude that the most appropriate candidate is self-reference by descriptions.

"Assessing Surveyability. Reframing the Debate on Computer-Assisted-Proofs" by Paul Hasselkuß

Abstract: As Thurston said, there is a continuity between the debate on formal and computer-assisted proofs. Mathematicians seem to dislike both due to their affinities. In the talk, I’ll discuss the notion of surveyability, which has often been voiced against computer-assisted proofs and, less so, against formal proofs (see Tymoczko 1979, Rota 1997, Easwaran 2009, De Toffoli 2021). Proofs that are hard or impossible to survey, it is claimed, cannot establish a priori truths. In the talk, I argue against this claim. I defend a view of surveyability not as an epistemological criterion, but as a local notion that is stressed by agents only in particular contexts. Using this view, I propose to reframe the debate on computer-assisted proofs in terms of conflicting values