NFL Workshop

The idea of Non-Fregean Logics emerged in the sixties together with Roman Suszko’s willingness to formalize Wittgenstein’s Tractatus [5,4]. Non-Fregean Logics (NFL, for short) owe their name to the rejection of the so called Fregean Axiom which says that the identity of referents of two given sentences boils down to the identity of their logical values [3]. In NFLs semantic correlates of sentences are not their logical values, but situations. The language of an NFL is equipped with the connective of identity, {\equiv}, which is intended to reflect the fact that two sentences describe the same situation.

The weakest considered by Suszko NFL is the Sentential Calculus with Identity, SCI for short, build upon Classical Sentential Calculus by the addition of the following axioms characterizing {\equiv}:

({\equiv _{1}}) {\varphi \equiv \varphi}
({\equiv _{2}}) {(\varphi \equiv \psi)\rightarrow (\neg \varphi \equiv \neg \psi)}
({\equiv _{3}}) {(\varphi \equiv \psi)\rightarrow (\varphi \leftrightarrow \psi)}
({\equiv _{4}}) {((\varphi \equiv \psi)\wedge(\alpha \equiv \beta))\rightarrow((\varphi \otimes \alpha) \equiv (\psi \otimes \beta))}

Suszko’s identity refers to a congruence relation, and it is clearly stronger than equivalence. The only valid formulas having {\equiv} as the main connective are of the form `{\varphi \equiv \varphi}, in this sense Non-Fregean identity formalized within SCI is a very strong connective. This interpretation is usually relaxed by extending the axiomatic basis of SCI.

The tutorial Proof-Theoretical Analysis of Non-Fregean Logics, proposed for the conference Non-Classical Logics. Theory and Applications 2022, focuses on proof-theory for NFLs. We pay special attention to structural proof theory taking into consideration sequent systems and natural deduction systems. The issues of cut-elimination and normalization are discussed. We also outline ideas for possible extensions of SCI and its intuitionistic counterpart called ISCI.

We begin with a synthetic tableau system (ST-system, for short) for SCI. In this method there is exactly one binary branching rule and a collection of linear rules called synthetic or synthesizing, since they build complex formulas from their subformulas and/or from their negations. The identity connective is characterized by a collection of such synthesizing rules encoding the basic properties of congruence.

We then move to the structural proof theory for SCI; we present sequent calculus which encapsulates the main properties of identity expressed within axioms ({\equiv_1})–({\equiv_4}), [1]. This particular calculus is then modified to fit the intuitionistic setting of ISCI, [2], for which we also discuss the decidability issue. We also cover WB — a Boolean extension of SCI obtained through the addition of six axioms extending the properties of the identity connective. Now, in contrast to SCI, we can consider a larger set of valid formulas built with the identity connective. We discuss a sequent calculus formalization of WB and its algebraic semantics. We also shortly discuss other extensions considered by Suszko: WT and WH.

In the remaining parts of the tutorial we focus on natural deduction systems for ISCI. Intuitionistic setting requires a constructive interpretation of identity, different ideas of which are discussed. This discussion, in turn, leads us to the identity’s relation to isomorphism, to which we come back in the last part of the workshop. We also address cut elimination in sequent calculus and normalization in natural deduction systems.

Most studied extensions of SCI are WB, WT and WH. We believe it is beneficial to consider analogous extensions of ISCI as well. Two usual ways of introducing extensions of an NFL are through the addition of axioms extending the properties of identity connective or by the addition of inference rules. Here we discuss less straightforward strategy. In WB a formula of the form {p\equiv \neg\neg p} is valid. Naturally, the addition of this formula to ISCI makes it an extension of SCI at once: the law of excluded middle becomes derivable and the starting-point logic is no longer intuitionistic. Thus we need to consider only those extensions that do not affect the constructive character of the logic. We consider two such extensions; one of them is related to the notion of propositional isomorphism, the other introduces a special case of the law of excluded middle.

Bibliography

[1] Chlebowski, S. (2018). Sequent Calculi for SCI. Studia Logica, 106(3):541–563.
[2] Chlebowski, S. i Leszczyńska-Jasion, D. (2019). An investigation into intuitionistic logic with identity. Bulletin of the Section of Logic, 48(4):259–283.
[3] Frege, F. L. G. (2014). Sens i znaczenie. In Biblioteka Klasyków Filozofii: Pisma Semantyczne. Państwowe Wydawnictwo Naukowe.
[4] Omyła, M. (1986). Zarys Logiki Niefregowskiej. Państwowe Wydawnictwo Naukowe.
[5] Suszko, R. (1975). Abolition of the Fregean Axiom. Lecture Notes in Mathematics, 453:169–239.

Reklama