ABSTRACT. The idea of tolerance relations seen as a formalization of the intuitive notion of resemblance was formalized by E. C. Zeeman in 1960s. In mathematics, as a natural generalization of congruences, tolerances appeared to be a very useful tool, especially in universal algebra.

Tolerances of a lattice L are reflexive, symmetric relations compatible with lattice operations of L. They form a lattice denoted by Tol(L).

A block of a tolerance T ∊ Tol(L) is a maximal set X ⊆ L satisfying X² ⊆ T. Blocks are convex sublattices of L, and it was shown by G. Czédli that they form a lattice (denoted by L/T), called the factor lattice of L modulo T. Although this construction generalizes the notion of a factor lattice L/φ defined by means of a congruence φ ∊ Con(L), properties of factor lattices modulo tolerances are significantly different. For instance, L/φ belongs to the same equational class as L, however, the lattice L/T does not belong to it, in general.

It is known that for any φ ∊ Con(L), the congruence lattice of the factor lattice L/φ is isomorphic to the principal filter [φ) of φ in Con(L) (homomorphism theorem). Moreover, any ψ ∊ Con(L), ψ ≥ φ induces the congruence ψ/φ on the factor lattice L/φ such that (L/φ)/(ψ/φ) ≅ L/ψ holds (second isomorphism theorem).

In this talk we formulate analogous results for tolerance factors defining a new partial order ⊑ on the lattice Tol(L) such that for any S ∊ Tol(L) with T ⊑ S, the tolerance S/T is induced on the factor lattice L/T. We also discuss the philosophical background of tolerances and their significance in lattice theory.

References:

[1] Ivan Chajda (1991): Algebraic Theory of Tolerance Relations. Univerzita Palackého Olomouc, Olomouc.

[2] George Grätzer (2011): Lattice Theory: Foundation. Springer, Basel, doi:10.1007/978-3-0348-0018-1.

[3] Joanna Grygiel (2019): Many faces of lattice tolerances. Bulletin of the Section of Logic 48(4), pp. 285–298, doi:10.18778/0138-0680.48.4.03.

[4] Joanna Grygiel & Sándor Radeleczki (2013): On the tolerance lattice of tolerance factors. Acta Mathematica Hungarica 141(3), pp. 220–237, doi:10.1007/s10474-013-0340-x.

[5] Eric Christopher Zeeman (1962): The topology of the brain and visual perception. In Marion Kirkland Fort, editor: Topology of 3-Manifolds and Related Topics, Dover Publications, New Jersey.

ABSTRACT. In this paper we split every basic propositional connective into two versions, one is called extensional and the other one intensional. The extensional connectives are semantically characterized by standard truth conditions that are relative to possible worlds. Assertibility and deniability of sentences built out of atomic sentences by extensional connectives are defined in terms of the notion of truth. The intensional connectives are characterized directly by assertibility and deniability conditions without the notion of truth. We pay special attention to the deniability condition for intensional implication. We characterize the logic of this mixed language by a system of natural deduction that sheds some light on the inferential behaviour of these two kinds of connectives and on the way they can interact.

ABSTRACT. The present paper addresses several puzzles related to the Rule of Existential Generalization, (EG). In solution to these puzzles, I clearly distinguish (EG) from a modified Rule of Existential Quantifier Introduction, which is derivable from (EG). Both these rules are often confused and both are considered as primitive. But I show that (EG) itself is derivable from the proper Rule of Existential Quantifier Introduction. The latter rule must be primitive in logical systems that treat both total and partial functions, for the universal and the existential quantifiers are not interdefinable in them. An appropriate natural deduction for such a system is deployed. It utilises an adequate definition of substitution which is capable of handling not only a higher-order quantification, but also (hyper)intensional contexts.

ABSTRACT. The aim of our paper is twofold: firstly we present a sequent calculus for an intuitionistic non-Fregean logic ISCI, which is based on the calculus presented in [1] and, secondly, we discuss the problem of decidability of ISCI via the obtained system. The original calculus from [1] did not provide the decidability result for ISCI. There are two problems to be solved in order to obtain this result: the so-called loops characteristic for the intuitionistic logic and the lack of the subformula property due to the form of the identity-dedicated rules. We discuss the possible routes to overcome these problems: we consider the weaker version of the subformula property, guarded by the complexity of formulas which can be included within it; we also present a proof-search procedure such that when it fails, then there exists a countermodel (in Kripke semantics for ISCI).

References [1] S. Chlebowski & D. Leszczynska-Jasion (2019): An Investigation into Intuitionistic Logic with Identity. Bulletin of the Section of Logic 48(4), p. 259–283, doi:10.18778/0138-0680.48.4.02. Available at https://czasopisma.uni.lodz.pl/bulletin/article/view/6272.

ABSTRACT. This presentation will give an overview of our ongoing work in developing knowledge extraction methods for description logic-based ontologies. Because the stored knowledge is not only given by axioms stated in an ontology but also by the knowledge that can be inferred from these axioms, knowledge extraction is a challenging problem. Forgetting creates a compact and faithful representation of the stored knowledge over a user-specified signature by performing inferences on the symbols not in this signature. After an introduction of the idea of forgetting, an overview of our forgetting tools and some applications we have explored, I will discuss recent work we have done in collaboration with SNOMED Intl to use our tools on the medical ontology SNOMED CT. Building on these experiences, we have developed a new consequence-based approach for computing self-contained subontologies that satisfy the SNOMED modelling guidelines. Such subontologies make it easier to reuse and share content, assist with ontology analysis, and querying and classification is faster.

The research was undertaken in several projects spanning several years funded by the UKRI/EPSRC (research, Doctoral awards, IAA), the University of Manchester and IHTSDO (SNOMED Intl).

ABSTRACT. 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, ≡, 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 ≡:

(≡1) φ ≡ φ

(≡2) (φ ≡ ψ) → (¬ φ ≡ ¬ ψ)

(≡3) (φ ≡ ψ) → (φ ↔ ψ)

(≡4) ((φ ≡ ψ) ∧ (α ≡ β)) → ((φ ⊗ α) ≡ (ψ ⊗ β))

Suszko's identity refers to a congruence relation, and it is clearly stronger than equivalence. The only valid formulas having ≡ as the main connective are of the form `φ ≡ φ', 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 (≡1)–(≡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 ≡ ¬¬ 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.

References:

[1] Szymon Chlebowski (2018): Sequent Calculi for SCI. Studia Logica 106(3), pp. 541–563, doi:10.1007/s11225-017-9754-8.

[2] Szymon Chlebowski & Dorota Leszczyńska-Jasion (2019): An investigation into intuitionistic logic with identity. Bulletin of the Section of Logic 48(4), pp. 259–283, doi:10.18778/0138-0680.48.4.02.

[3] Gottlob Frege (1948): Sense and reference. The Philosophical Review 57(3), pp. 209–230. Available at 10.2307/2181485.

[4] Mieczysław Omyła (1986): Zarys Logiki Niefregowskiej (Introduction to Non-Fregean Logic). Państwowe Wydawnictwo Naukowe, Warszawa.

[5] Roman Suszko (1975): Abolition of the Fregean axiom. In Rohit Parikh, editor: Logic Colloquium, Lecture Notes in Mathematics 453, Springer, Berlin, Heidelberg, pp. 169–239, doi:10.1007/BFb0064874.

ABSTRACT. 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, ≡, 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 ≡:

(≡1) φ ≡ φ

(≡2) (φ ≡ ψ) → (¬ φ ≡ ¬ ψ)

(≡3) (φ ≡ ψ) → (φ ↔ ψ)

(≡4) ((φ ≡ ψ) ∧ (α ≡ β)) → ((φ ⊗ α) ≡ (ψ ⊗ β))

Suszko's identity refers to a congruence relation, and it is clearly stronger than equivalence. The only valid formulas having ≡ as the main connective are of the form `φ ≡ φ', 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 (≡1)–(≡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 ≡ ¬¬ 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.

References:

[1] Szymon Chlebowski (2018): Sequent Calculi for SCI. Studia Logica 106(3), pp. 541–563, doi:10.1007/s11225-017-9754-8.

[2] Szymon Chlebowski & Dorota Leszczyńska-Jasion (2019): An investigation into intuitionistic logic with identity. Bulletin of the Section of Logic 48(4), pp. 259–283, doi:10.18778/0138-0680.48.4.02.

[3] Gottlob Frege (1948): Sense and reference. The Philosophical Review 57(3), pp. 209–230. Available at 10.2307/2181485.

[4] Mieczysław Omyła (1986): Zarys Logiki Niefregowskiej (Introduction to Non-Fregean Logic). Państwowe Wydawnictwo Naukowe, Warszawa.

[5] Roman Suszko (1975): Abolition of the Fregean axiom. In Rohit Parikh, editor: Logic Colloquium, Lecture Notes in Mathematics 453, Springer, Berlin, Heidelberg, pp. 169–239, doi:10.1007/BFb0064874.

ABSTRACT. 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, ≡, 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 ≡:

(≡1) φ ≡ φ

(≡2) (φ ≡ ψ) → (¬ φ ≡ ¬ ψ)

(≡3) (φ ≡ ψ) → (φ ↔ ψ)

(≡4) ((φ ≡ ψ) ∧ (α ≡ β)) → ((φ ⊗ α) ≡ (ψ ⊗ β))

Suszko's identity refers to a congruence relation, and it is clearly stronger than equivalence. The only valid formulas having ≡ as the main connective are of the form `φ ≡ φ', 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 (≡1)–(≡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 ≡ ¬¬ 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.

References:

[1] Szymon Chlebowski (2018): Sequent Calculi for SCI. Studia Logica 106(3), pp. 541–563, doi:10.1007/s11225-017-9754-8.

[2] Szymon Chlebowski & Dorota Leszczyńska-Jasion (2019): An investigation into intuitionistic logic with identity. Bulletin of the Section of Logic 48(4), pp. 259–283, doi:10.18778/0138-0680.48.4.02.

[3] Gottlob Frege (1948): Sense and reference. The Philosophical Review 57(3), pp. 209–230. Available at 10.2307/2181485.

[4] Mieczysław Omyła (1986): Zarys Logiki Niefregowskiej (Introduction to Non-Fregean Logic). Państwowe Wydawnictwo Naukowe, Warszawa.

[5] Roman Suszko (1975): Abolition of the Fregean axiom. In Rohit Parikh, editor: Logic Colloquium, Lecture Notes in Mathematics 453, Springer, Berlin, Heidelberg, pp. 169–239, doi:10.1007/BFb0064874.