Courses
Sorin Bangu (University of Bergen)
How can we have mathematical knowledge? A cognitive middle way. On the standard ('Euclidean') picture of mathematics, the answer to this question is that proofs give us mathematical knowledge. More explicitly, proofs show why (and how) some initial assumptions entail a mathematical proposition. But a serious problem arises right away: while this entailment (the proof itself) is necessary to hold, we are still not entitled to say that we know the proposition in question until we provide reasons to claim that we know these assumptions as well. And, when these assumptions are the fundamental axioms (of arithmetic, or of set theory), the question reduces to how we know them; that is, what is our justification to believe them? After we examine some possible ways to provide this justification (and find them unsatisfactory), I'll argue that the best hope is to resort to considerations of a non-mathematical character: the empirical evidence recently provided by cognitive science about the existence of innate mathematical abilities.
Reading suggestions:
Mary Tiles 'Axiomatization, Rigor and Reason' Ch. 1 (pp. 7-32) in her Mathematics and The Image of Reason. Routledge, 1991.
Penelope Maddy 'The Problem' Ch. 1 (pp. 2-37) in her Defending the Axioms. Oxford Univ. Press, 2011.
Two chapters from Bangu, S. (ed.) Naturalizing Logico-Mathematical Knowledge: Approaches from Philosophy, Psychology and Cognitive Science. Routledge 2018: (1)Sorin Bangu: 'A Naturalist Lanscape' (pp. 1-15). (The Introduction to the book). (2) Karen Wynn: 'Origins of Numerical Knowledge' (pp. 106-131).
Constantin C. Brîncuș (Institute of Philosophy and Psychology/ University of Bucharest)
Open-ended Logical Inferentialism. Logical inferentialism takes the proof-theoretic notions of inference and proof to have priority over the model-theoretic ones of truth and reference. Viewed as a meta-semantic approach, it maintains that the meanings of the logical terms (propositional operators and quantifiers) are determined/fixed/defined by the logical axioms and rules that govern their use in a logical calculus. One challenge for the logical inferentialist program is the fact that the axioms are rules are compatible with different interpretations for the logical terms, i.e., the meanings are not uniquely determined by the rules. In my talk, I critically examine the idea that the open-ended natural deduction rules of inference for the logical operators and quantifiers uniquely determine their meanings.
Reading suggestions:
Constantin C. Brîncuș, "Are the Open-Ended Rules for Negation Categorical?”, Synthese. An International Journal for Epistemology, Methodology and Philosophy of Science, 198, pp. 7249–7256 (2021)
Constantin C. Brîncuș, "Inferential Quantification and the Omega Rule". In Antonio Piccolomini d'Aragona (Ed.) Perspectives on Deduction, Synthese Series, Springer (forthcoming) (preprint)
Jared Warren . 2020. Shadows of Syntax. Revitalizing Logical and Mathematical Conventionalism, OUP. (pp. 29-33, 78-80, 85-86, 255-59).
Fabien Carbo-Gil (Université d'Aix-Marseille)
Understanding what we misunderstand by proving the unprovable. One of the most important features of formal logic is that by permitting an unambiguous definition of what a formal system is, it allows logicians to prove meta-logic theorems that tell us which goals we can or can’t expect to achieve by using different kinds of formal systems. We will center our presentation on the case of first-order axiomatization of set theory ZFC which is widely used as a foundation for mathematics. In the case of ZFC, the meta-theorems that we have in mind comprise Gödel’s incompleteness theorems and Löwenheim-Skolem theorems. These meta-theorems are usually seen as “limitating results” that show us the limits of what it is possible to achieve within ZFC. To the contrary, we will argue that this kind of meta-theorems can be used and has been used to try to override formal limitations, to try to reduce the distance between mathematicians informal practices and formal systems. In order to do that, we will introduce Gödel’s incompleteness theorems and Löwenheim Skolem theorem and discuss the philosophical meaning of these theorems. Then we will see how if we follow Gödel and adopt a realist point of view toward sets, the incompleteness of ZFC is nothing but an invitation to complete ZFC by adding new axioms and principles to it. We will try to understand how and where the independence phenomena show up in ZFC and how the methods used to prove the independence of statements from ZFC can be used as a starting point to complete ZFC. That gonna lead us to have a look at three subjects that are the main topics of today’s set theory: Large cardinal assumptions; Inner Models; Forcing and forcing axioms. After discussing these subjects, we will introduce our interpretation of Gödel’s absolute notion of provability that rests on large cardinal assumptions. Since this notion was introduced by Gödel in 1946 we will analyse the possibility to maintain such an absolute notion when we take into account the mathematical work that has been done in the domains of Inner Models and Forcing since 1946.
Annalisa Cusi (Mathematics Department, Sapienza University of Rome)
Teaching-learning of proof at upper secondary school level. The theme of my lecture will be the teaching-learning of proof at upper secondary school level. In particular, the focus will be on the design of a path aimed at fostering the development of students' competencies in the use of algebraic language as a thinking tool that supports the exploration of numerical situations, the generalizations that lead to the development of conjectures and the construction of argumentations and proofs. During the lecture, data from teaching experiments will be analysed, by means of specific theoretical constructs, to reflect on the key competencies that need to be activated for an effective use of algebraic language as a thinking tool and on the role that the teacher plays in fostering students' development of such competencies.
References:
Arzarello, F., Bazzini, L., e Chiappini, G. (2001). A model for analyzing algebraic thinking. In R. Sutherland et Al. (Eds.), Perspectives on School Algebra (pp. 61-81). Netherlands: Kluwer Publishers.
Boero, P. (2001). Transformation and Anticipation as Key Processes in Algebraic Problem Solving. In R. Sutherland et Al. (Eds.), Perspectives on School Algebra (pp. 99-119). Netherlands: Kluwer Publishers.
Collins, A., Brown, J.S. e Newman, S.E. (1989). Cognitive Apprenticeship: Teaching the Crafts of Reading, Writing and Mathematics! In L.B. Resnick (Ed.), Knowing, Learning, and Instruction: Essays in Honor of Robert Glaser (pp. 453-494). Hillsdale, NJ: Lawrence Erlbaum Associates.
Duval, R. (2006). A cognitive analysis of problems of comprehension in a learning of mathematics. Educational Studies in Mathematics, 61, 103–131.
Mircea Dumitru (University of Bucharest/ Romanian Academy)
Models and Proofs. I shall discuss the two techniques/tools of building up a logical theory: models and proofs in setting up a logical theory. My own view is model-theoretic and I shall discuss how incompleteness phenomena (especially semantic incompleteness in modal logic) should be taken into account when assessing the advantage of the model-theoretic approach over the proof-theoretic approach.
Valentin Goranko (Stockholm University)
Hybrid Deduction–Refutation Systems: Proofs and Refutations Getting Married. Logical refutation systems are systems of formal derivations intended to derive the non-valid, i.e. semantically refutable, formulae of a given logical system. Even though the idea of formally deriving non-valid syllogisms goes back to Aristotle, it received almost no attention until the early-mid 20th century, when Jan Lukasiewicz started promoting it actively and with some of his students developed complete refutation systems for Aristotle’s syllogistic, classical and intuitionistic logics. Since then, the topic of refutation systems has been revisited and briefly entertained by several logicians, but pursued more systematically by just a few.
The talk will be based mainly on the paper [1], introducing systems of deduction that combine standard deductive systems for deriving logical validities with refutations systems deriving non-validities of a given logical system. Such combined (`hybrid’) systems of deduction employ inference rules involving both provable and refutable premises and conclusions. Simple natural examples of such rules are Modus Tollens (if A -> B is a theorem (hence, valid) and B is refuted, then A is refuted) and the Disjunction property (e.g. in Intuitionistic logic) stated as an inference rule: if A v B is a theorem and A is refuted then B is a theorem.
After a brief historical overview and background on refutation systems (cf. [2]) in this talk I will present the basics of hybrid deduction–refutation systems, including the concept of generic hybrid rules and hybrid deduction–refutation derivations. Then, as an illustrating example, I will present such a system in Natural Deduction style for the classical propositional logic, which is sound and complete both for deductions and for refutations. I will then mention some extensions of hybrid deduction–refutation systems to modal and intuitionistic logics. Finally, I will discuss briefly an emerging hierarchy of higher-order hybrid rules and systems and will conclude with some open problems and potential applications.
References:
[1] Goranko, V: Hybrid Deduction–Refutation Systems. Axioms, Special issue on Deductive systems, 8(4), p.118-136 (2019)
[2] Goranko, V., Pulcini, G., Skura, T.: Refutation systems: an overview and some applications to philosophical logics. In: Liu, F., Ono, H., Yu, J. (Eds.) Knowledge, Proof and Dynamics, Post-proceedings volume with selected papers from the Fourth Asian Workshop on Philosophical Logic, Springer, Logic in Asia: Studia Logica Library, pp. 173-197 (2020)
Reinhard Kahle (University of Tübingen)
Gödel's Incompleteness Theorems. I offer a course "Gödel's Incompleteness Theorems", providing an introduction to the logical framework, an (already quite extensive) sketch of the proofs, and a discussion of the significance of the theorems.
Thomas Piecha (University of Tübingen)
Constructive semantics. We present and discuss two kinds of semantics for constructive logics such as intuitionistic logic, namely proof-theoretic semantics [4] and dialogue semantics [2]. In the former, the meaning of logical constants is given in terms of proof and construction, whereas the latter explains the meaning of logical constants in game-theoretic terms. Both semantics yield a notion of logical validity that can be compared with the notion of provability according to a given proof system. We discuss in particular the question of whether proof systems for intuitionistic logic are complete for these semantics [1, 3].
References:
[1] T. Piecha, Completeness in proof-theoretic semantics. In: T. Piecha and P. Schroeder-Heister (eds), Advances in Proof-Theoretic Semantics, Trends in Logic Vol. 43 (Springer, 2016), pp. 231–251. https://link.springer.com/content/pdf/10.1007/978-3-319-22686-6_15.pdf?pdf=inline%20link.
[2] T. Piecha, Dialogical logic. In: The Internet Encyclopedia of Philosophy, https://iep.utm.edu/dialogical-logic/.
[3] T. Piecha and P. Schroeder-Heister, Incompleteness of intuitionistic logic with respect to proof-theoretic semantics, Studia Logica 107(1), 233-246 (2019). Available online at https://doi.org/10.1007/s11225-018-9823-7 and via Springer Nature SharedIt at https://rdcu.be/5dDs.
[4] P. Schroeder-Heister, Proof-theoretic semantics. In: E. N. Zalta (ed.), Stanford Encyclopedia of Philosophy (Metaphysics Research Lab, Stanford University, 2012). https://plato.stanford.edu/entries/proof-theoretic-semantics/, revised 2018 and 2023
Antonio Piccolomini d'Aragona (Institute of Philosophy, Czech Academy of Sciences)
What to prove and how to prove: two views on the distinction between proof-objects and proof-acts In a seminal paper from 1998, Göran Sundholm has tried to convince Dag Prawitz that a semantic theory of deduction had better employ three notions of proof: proof-object, proof-act and proof-trace. Proof-objects are abstract truth-makers for propositions; as such, they are devoid of epistemic content. Proof-acts are demonstrations used to justify assertions; therefore, they are epistemic in nature. Proof-traces reify proof-acts, so they are objects too; in spite of this, however, they carry epistemic force, as one can use them as "recipes" for performing the proof-acts they describe. In the beginning, Prawitz was sceptical that Sundholm’s distinction was actually needed. In fact, in Prawitz’s earlier semantics of valid arguments, the three notions can be seen to collapse into each other. This collapse, however, results in a number of circularity and decidability problems. To solve these problems, Prawitz’s later theory of grounds introduces an objects-acts-traces distinction reminiscent of that put forward by Sundholm. This notwithstanding, Prawitz’s ground-theoretic picture retains many significant peculiarities. These mainly concern the way objects, acts, and traces relate to each other, and the epistemic status assigned to proof-objects. In my talk, I aim to provide an overview and comparison of Prawitz’s and Sundholm’s semantics, and I argue that the divergences between the two stem from a difference in how Prawitz and Sundholm respectively conceive of the notion of assertion.
References:
[1] A. Piccolomini d'Aragona, Are proofs objects or acts? A comparison of Prawitz's and Sundholm's semantics, in A. Klev (ed), The architecture and archaeology of modern logic. Studies dedicated to Göran Sundholm, Springer (available here)
[2] D. Prawitz, Logical consequence from a constructivist point of view, in S. Shapiro (ed), The Oxford Handbook of Philosophy of Mathematics and Logic, 671–695. Oxford University Press, 2005
[3] D. Prawitz, Explaining deductive inference, in H. Wansing (ed), Dag Prawitz on proofs and meaning, 65–100. Springer, 2015
[4] G. Sundholm, Proofs as acts and proofs as objects: some questions for Dag Prawitz, Theoria, 64 (2-3), 187–216, 1998
[5] G. Sundholm, Semantic values for natural deduction derivations, Synthese 148, 623–638, 2006.
Gabriel Sandu (University of Helsinki)
Game Theoretic Semantics. Proofs vs Strategies. I will introduce the basic ideas of game-theoretical semantics. The central idea is that game theoretical truth in a model is defined as the existence of a winning strategy for one player in a so-called semantical game associated with the model. It is known that under certain assumptions game-theoretical truth is equivalent to Tarskian truth. Hintikka implemented constructivist ideas in game-theoretical semantics by requiring that the players' strategies be recursive. The question I will ask is: do recursive strategies yield proofs? The answer is negative, but we obtain a correspondence between truth and proof if we extend semantical games in a certain way.
Reference: Boyer, J., Sandu, G. ”Between proof and truth”. Synthese 187, 821–832 (2012). https://doi.org/10.1007/s11229-011-9903-y
Andrei Sipoș (University of Bucharest & IMAR & ILDS)
Glimpses of proof mining. We provide an introduction to proof mining accessible to a wide intellectual audience, focused on its historical and philosophical underpinnings, exploring how tools originally created for clarifying the foundations of mathematics may be exploited towards more pragmatic goals. This is followed by a presentation of the milestone achievements of proof mining so far and glimpses of what may yet come.
References:
[1] U. Kohlenbach, Applied proof theory: Proof interpretations and their use in mathematics. Springer Monographs in Mathematics, Springer, 2008.
[2] U. Kohlenbach, Proof-theoretic methods in nonlinear analysis. In: B. Sirakov, P. Ney de Souza, M. Viana (eds.), Proceedings of the International Congress of Mathematicians 2018 (ICM 2018), Vol. 2 (pp. 61–82). World Scientific, 2019.
[3] U. Kohlenbach, Local formalizations in nonlinear analysis and related areas and proof-theoretic tameness. In: P. Weingartner, H.-P. Leeb (eds.), Kreisel’s Interests. On the Foundations of Logic and Mathematics (pp. 45–61). College Publications, Tributes vol. 41, 2020.
[4] A. Sipoș, What proof mining is about. Blog post series, 2020, first part accessible at: https://prooftheory.blog/2020/06/06/what-proof-mining-is-about-part-i/
Iulian D. Toader (University of Vienna)
Quantum-theoretical inferentialism. Quantum-theoretical inferentialism is the view that the semantic content of quantum-theoretical terms is determined by the rules governing their employment in quantum-theoretical inferences, rather than by their representational properties, i.e. properties they have in virtue of semantic rules positing correspondences between such terms and elements of physical reality. After explaining and exploring some basic notions of this view, I will argue that quantum-theoretical inferentialism faces a categoricity problem, analogous to the more familiar categoricity problem for logical inferentialism. This is a problem for the view under discussion, for it shows that the inferential rules of quantum theory do not determine precisely (i.e., uniquely up to some proper isomorphism) the semantic properties of the standard quantum-theoretical formalism. Time-permitting, I explore some possible answers to this problem.
Reading suggestions:
Steinberger, Florian & Murzi, Julien. 2017. 'Inferentialism'. In Blackwell Companion to Philosophy of Language. Wiley Blackwell. pp. 197-224.
Lewis, Peter J., 'Quantum Mechanics and its (Dis)Contents', in Steven French, and Juha Saatsi (eds), Scientific Realism and the Quantum (Oxford, 2020, Oxford Academic, 21 May 2020), https://doi.org/10.1093/oso/9780198814979.003.0009