This talk reflects on how logical or mathematical proofs formalized in proof systems relate to philosophical properties of proof.
Generally, the existence of a formalized proof is taken as a standard for correctness (called the standard view in the literature, see e.g. [1]). But formal proofs are conceptually still far-removed from informal proofs (proofs in the way they are actually carried out), and not much is known about their specific relation. For instance, the derivation-indicator view [2] says that a mathematical proof ‘indicates’ an underlying formalized derivation, but how exactly this should happen is unclear.

We will take a relatively high-level strategy to relate informal proofs to formalized derivations, and restrict ourselves to two case studies. The first suggests that we can zoom in on a particular philosophical property that an informal proof possesses, and see how it can be made precise in the formal setting. A case study of this approach is [3], concerning purity of proof; studies can also be found, among others, for the properties of explanation and simplicity of proof. Here, formalized proofs that satisfy a precisified requirement for purity can be taken as corresponding more closely to pure informal proofs of the same theorem.

For the second case study, we take a step back, and differentiate between the types of proof systems in which a proof can be formalized. In particular, a myriad of proof systems exist nowadays for modal logic, which extend the basic modal language in a variety of ways. We may wonder whether all such extensions can provide acceptable formalizations of modal reasoning. The phenomenon of ‘semantic pollution’ of proof systems, most intuitively described as ‘bringing Kripke semantics into the proof system’, is potentially problematic for faithful formalization. We will also consider this property more closely, and present possible formal criteria for it.

Bibliography

1. Avigad, Jeremy,Reliability of mathematical inference,Synthese,vol. 198 (2021), no. 8, pp. 7377–7399.
2. Azzouni, Jody,The derivation-indicator view of mathematical practice,Philosophia Mathematica,vol. 12 (2004), no. 2, pp. 81–106.
3. Martinot, Robin,Ontological Purity for Formal Proofs,The Review of Symbolic Logic,2023, pp. 1–40.
4. Stra{\ss}burger, Lutz,Proof nets and the identity of proofs,arXiv preprint cs/0610123,2006.

The purpose of the paper is to provide a thorough account of the issue of empty terms and ontological assumptions as they play throughout the history of Western logic, beginning with Aristotelian syllogistic and going up till the Boolean algebra and the emergence of modern formal logic. Modern formal logic, using the notion of the universe of discourse, does not allow for constructing interpretations of formal languages for empty universes. In contemporary discussions, it is widely assumed that the Aristotelian syllogistic did not allow for the use of empty terms as well. Upon closer examination, this view does not reflect the historical reality, and the issue of empty terms is much more complex. Throughout history, it has been extensively discussed both in relation to categorical statements and the Logical Square. In the paper, I relate those discussions. I assert 1) that the (non)emptiness of terms did not emerge as an issue in Aristotelian logic, and the dominant modern interpretation stems from the development of formal logic and attempts to render syllogistic using modern notation, 2) that the interest of Arabic philosophers in the issue can be explained by different ways of expressing existence and attribution in Indo-European and Semitic languages, 3) that the conditional treatment of existential assumptions proposed by Ockham serves as the origins of the universe of discourse idea. I end by asserting that, firstly, throughout the history we can observe a rising awareness of empty terms as an issue that needs to be addressed, secondly, in parallel to it, we can trace the origins of the modern universe of discourse idea.

Ciardelli [1] suggests a way to lift classical semantic accounts of conditionals that assign propositions to conditional sentences to the inquisitive semantics setting. In the resulting framework, antecedents and consequents of conditional sentences may be associated with multiple alternative propositions, and a conditional sentence is taken to express that for each alternative for the antecedent, if that alternative were to obtain, then some corresponding alternative for the consequent would also obtain. This type of lifting can be used to handle issues concerning disjunctive antecedents, conditional questions and unconditionals. In this talk, I consider the conditional inquisitive logics that Ciardelli’s lifting recipe gives rise to. In particular, I focus on how to construct axiom systems for inquisitive logic versions of various conditional logics.

Bibliography

1. Ivano Ciardelli,Lifting conditionals to inquisitive semantics,Semantics and Linguistic Theory (SALT),(M. Maroney, C.-R. Little, J. Collard and D. Burgdorf, editors),vol. 26,Ithaca, NY: LSA and CLC Publications,2016,pp. 732–752.

Authors: Avgerinos Delkos and Marianna Girlando

Counterfactuals, studied in the seminal book by D. Lewis [2], are conditional statements describing consequences of states of affairs that might not have occurred. Ceteris paribus counterfactuals take into account specific conditions which hold at the actual state, and which ought to be kept unchanged throughout the evaluation.

Inspired by the approach of Girard and Triplett in [3,4], we define ceteris paribus conditionals as dynamic operators over (weakly) centered sphere models. We introduce three ways of evaluating the operators, by updating sphere models based on ceteris paribus sets of formulas.

Our approach features two main novelties: on the one hand, we define our ceteris paribus conditionals as proper dynamic operators, thus allowing for iterated evaluations. On the other hand, when updating the worlds within a system of sphere we additionally take into account a notion of ‘significance’ of the formulas that ought to be kept unchanged.

We discuss the relations of our model updates with other prioritisations introduced in the literature (mainly considering [3,4]). Furthermore, we show completeness of the set of valid formulas in the updated centered (resp. weakly centered) sphere models with respect to Lewis’ axiomatization of the conditional logic \(\mathsf{VC}\) (resp. \(\mathsf{VW}\)).
A preprint with full details is available [1].

Bibliography

1. A. Delkos and M. Girlando,A dynamic approach to ceteris paribus counterfactuals,arXiv preprint (2023), arXiv:2312.15209, {https://arxiv.org/abs/2312.15209}
2. D. Lewis,Counterfactuals,Blackwell,Oxford,1973.
3. P. Girard and M.A. Triplett,Ceteris paribus logic in counterfactual reasoning,Proceedings Fifteenth Conference on Theoretical Aspects of Rationality and Knowledge(TARK 2015),(R. Ramanujam, editor),vol. X215EPTCS,2015,pp. 176–193.
4. P. Girard and M.A. Triplett,Prioritised ceteris paribus logic for counterfactual reasoning,Synthese,vol. 195 (2018), no. 4, pp. 1681–1703.