Proof-Theoretical Analysis of Non-Fregean Logics

Dorota Leszczyńska Jasion (Adam Mickiewicz University, Poznań, Poland)

Szymon Chlebowski (Adam Mickiewicz University, Poznań, Poland)

Marta Gawek (University of Lorraine, CNRS, LORIA)

Agata Tomczyk (Adam Mickiewicz Uniwersity, Poznań, Poland)

Dawid Czech (Adam Mickiewicz Uniwersity, Poznań, Poland)

Description:  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.


[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.



Applications of Relating Semantics to Philosophical Logic

Tomasz Jarmużek (Nicolaus Copernicus University)

Description:  Relating Logic is a logic of relating connectives (just as Modal Logic is a logic of modal operators). The basic idea behind a relating connectives is that the logical value of a given complex proposition is the result of two things:

(i) the logical values of the main components of this complex proposition, supplemented with

(ii) a valuation of the relation between these components.

The latter element is a formal representation of an intensional relation that emerges from the connection of several simpler propositions into one more complex proposition. More formally, let A1, ..., An be propositions with some fixed logical values and let c be an n-ary relating connective. Then the logical value of complex sentence c(A1, ..., An) depends not only on the logical values of A1, ..., An, but additionally on the value of the connection between A1, ..., An. It therefore depends on an additional valuation of pairs (n-tuples) that is the part of the overall process of evaluation of the logical values of complex propositions built with relating connectives. This way we can form logical systems to deal with reasoning about non-logical relationships. They are determined with relating semantics.

Although the simplest model in relating semantics is a pair ⟨ v, R ⟩, the situation may get more complicated. We can use multi-relating models to represent more types of non-logical relations between sentences. In addition, the valuation of relationships between sentences may not be binary but may be many-valued or more subtly graded. Furthermore, we can mix relating semantics with possible world semantics, equipping all worlds with additional valuations of complex sentences. Last, but not least, any semantics may be treated as relating one, when we assume that in case of complex sentences a relationship is represented by a universal relation.

The solution that relating semantics offers seems to be quite natural, since when two (or more) propositions in natural language are connected by a connective, some sort of emergence occurs. In fact, the key feature of intensionality is that adding a new connective results in the emergence of a new quality, which itself does not belong to the components of a given complex proposition built by means of the same connective. An additional valuation function determines precisely this quality.Talking about emergence is justified here, because the quality that arises as a result of the connections between the constituent propositions is not reducible to the properties of those propositions. Consequently, if the phenomenon of emergence is to be properly captured, we need additional valuations in a model. The key feature of relating semantics is that it enables us to treat non-logical relations between sentences seriously.


[1] Tomasz Jarmużek & Francesco Paoli (2021): Relating Logic and Relating Semantics. History, Philosophical Applications and Some of Technical Problems. Logic and Logical Philosophy 30(4), p. 563–577, doi:10.12775/LLP.2021.025.

[2] Mateusz Klonowski (2021): History of Relating Logic. The Origin and Research Directions. Logic and Logical Philosophy 30(4), p. 579–629, doi:10.12775/LLP.2021.021.


Daniela Glavaničová, Matteo Pascucci. Applications of relating semantics in the normative domain

Luis Estrada-Gonzalez, Mateusz Klonowski. An analysis of poly-connexivity in Boolean connexive logic

Alessandro Giordani. From the Logic of Grounding to Relating Logic

Luis Estrada-Gonzalez. Connexive logic: relating semantics as compatibility semantics

Maria Martinez-Ordaz. Scientific understanding meets relating logic

Tomasz Jarmużek, Mateusz Klonowski, Daniela Glavaničová, Piotr Kulicki. Tableaux for some deontic logics with the explicit permission operator

Oleg Grigoriev, Krystyna Mruczek-Nasieniewska, Marek Nasieniewski, Yaroslav Petrukhin, Vasiliy Shangin. On Embedding of D2 into the Minimal Discussive Logic



Advances in Formal Ontology

Janusz Kaczmarek (University of Łódź)

Description: Ontology is a theoretical subdiscipline of philosophy. `What exists, what is?' is the fundamental question of ontological research. There exist and there are people, animals, plants, clouds, mountains. There are also qualities, relations, actions, sensations, time and space. Sometimes ontology (metaphysics) is defined as the philosophical science of being as being. Formal ontology is a certain variant of ontology as such, a certain way of investigating and inquiring into ontological questions, problems, concepts, and theorems. What kind of way is it? Here, in formal ontology, we use formal tools and methods. To these tools and methods belong, among others, methods which we can find in logic, algebra, systems theory, and, recently, also general topology. For example, in 1905 Russell's theory of descrptions (On Denoting) was presented, which explained, with the help of logical tools, how to use names correctly. In the 1920s, Polish logician J. Łukasiewicz used 3-valued logic to study the determinism/indeterminism problem. In the 1980s and 1990s, the philosophy of action (cf. Belnap and Perloff) was developed; this philosophy and logic (cf. STIT Logic) can be seen as a formal analysis of one of Aristotle's categories, namely the category of action; in the 20th century between 1920 and 1930, Russell and Wittgenstein proposed the ontology of logical atomism that relied heavily on the achievements of sentence logic and first-order logic of the time. In turn, in the 1980s, Wittgenstein's proposal presented in Tractatus Logico-Philosophicus was interpreted by Polish philosopher and ontologist B. Wolniewicz. His interpretation makes use of lattice theory. In the last few decades general topology and mathematical theory of categories (mathematical because we want to distinguish it from the theory of categories already proposed by Aristotle) have also been used to study and interpret philosophical and ontological problems (e.g., R. Thom, K. Kelly, O. Schulte and C. Juhl, T. Mormann). During the workshop selected propositions, topics, problems in the field of formal ontology, including topological ontology, will be presented. The following philosophers ontologists, and logicians will take part in it:

  1. Uwe Meixner is the author of the monograph Axiomatic Formal Ontology. Springer Publishing described this monograph as follows:
    Axiomatic Formal Ontology is a fairly comprehensive systematic treatise on general metaphysics. The axiomatic method is applied throughout the book. Its main theme is the construction of a general non-set-theoretical theory of intensional entities. Other important matters discussed are the metaphysics of modality, the nature of actual existence, mereology and the taxonomy of entities.
  2. Piotr Błaszczyk is the author of the monograph Philosophical analysis of Richard Dedekind's treatise «Stetigkeit und irrationale Zahlen» (in Polish); in this monograph he analyses Dedekind's work through the existential ontology of Ingarden (Polish philosopher, phenomenologist, ontologist); he deals with topics at the intersection of ontology and philosophy of mathematics; he examines, among other things, the structure of a mathematical proof referring to Pythagoras, Poincare, Hilbert.
  3. Kordula Świętorzecka is the author of the monograph Classical Conception of the Changeability of Situations and Things Represented in Formalized Languages; she examines, among other things, different systems of logic of time and the logic of change and the structure of proofs for the existence of God (e.g., Gödel's proof).
  4. Bartłomiej Skowron has published the monograph Part and Whole. Towards topo-ontology (in Polish); in it, he examines ontological issues through topological and mereological tools; his main interests focus on ontological problems of the description of ideas, personality, and methodological use of topology and category theory in philosophical research.
  5. Janusz Kaczmarek is the author of the monograph Individuals. Ideas. Concepts. Research in Formalised Ontology (in Polish); he currently works mainly in the area of topological ontology and, using the tools of general topology, studies ontological concepts (objects) such as: state of affairs, possible world, monad, system, ideas and many others.



Graded Logic

Jozo Dujmović (State University of San Francisco)

Description:  Graded logic (GL) is the logic of human reasoning with graded percepts. Human percepts of truth, importance, satisfaction, suitability, preference, and many others, are all graded, i.e., they are a matter of degree. Without the loss of generality, all degrees are normalized in the interval [0,1], where 0 denotes the lowest degree and 1 denotes the highest degree of the intensity of given percept. Truth is the most important of graded percepts because all graded percepts can be described as the degree of truth of the statement asserting that a given percept has the highest intensity. For example, the degree of truth of the statement "the object A completely satisfies all our requirements" is equivalent to the degree of satisfaction (or suitability) of A. Obviously, truth is not an anonymous real number, but the percept that has both the intensity and a clear semantic identity: the role, meaning, and importance for specific stakeholder. The stakeholder is defined as an individual, or an organization, who specify an assertion, and then need to know its degree of truth. Usually, that is done in the process of decision-making, where the stakeholder evaluates alternatives and selects the most suitable alternative. GL is fully humancentric: its main goal is to be consistent with observable properties of human reasoning. That is the motivation for development of GL.

GL is based on the concept that both simultaneity (conjunction) and substitutability (disjunction) are a matter of degree. This concept was introduced in 1973. The conjunction degree (later renamed andness) is an indicator of similarity between a logic aggregator and the full (or pure) conjunction (the minimum function). The disjunction degree (later renamed orness) is an indicator of similarity between a logic aggregator and the full (pure) disjunction (the maximum function). Andness and orness are adjustable and complementary indicators, observable and measurable in human reasoning. The highest orness (1) corresponds to the lowest andness (0), and the highest andness (1) corresponds to the lowest orness (0). The andness 1 denotes the full conjunction, and the orness 1 denotes the full disjunction. Between these extreme points we have the graded (or partial) conjunction and the graded (or partial) disjunction functions with adjustable degrees of andness/orness. Therefore, the models of graded conjunction/disjunction must provide continuous transition from the full conjunction to the full disjunction.

Both the inputs and the output of the graded conjunction function and the graded disjunction function are the degrees of truth. The graded conjunction is a basic GL function where andness is greater than orness. It is the model of simultaneity, and consequently the output of this function is primarily affected by the low values of arguments. The graded disjunction is a basic GL function where orness is greater than andness. It is the model of substitutability, and consequently the output of this function is primarily affected by the high values of arguments. Human logic reasoning provably combines simultaneity and substitutability.

All means are functions that return values between the minimum and the maximum of their arguments. Thus, means can be interpreted as logic functions. The centroid of all means, where andness equals orness (i.e., both have the value 1/2), is the traditional arithmetic mean. The arithmetic mean is interpreted as the logic neutrality because it simultaneously has 50% of conjunctive properties and 50% of disjunctive properties. Parameterized means, such as power means and exponential means, provide the desirable continuous transition from the full conjunction to the full disjunction. In addition, when used as logic functions, means provide another necessary property: means can be weighted and support the degree of importance of input arguments. In human reasoning, each truth has a meaning and consequently also a specific degree of importance for its stakeholder. It is not exaggeration to claim that all logic models where truth does not come with its importance degree, must be rejected as realistic models of human reasoning. Many means, such as weighted power means, use weights to express the impact/importance of individual arguments. So, such means are the primary candidates for serving as graded logic aggregators.

The use of annihilators is a fundamental observable property of the graded conjunction and the graded disjunction used in human reasoning. If the graded conjunction supports the annihilator 0, then such operator is called hard; if the annihilator 0 is not supported, then the operator is called soft. If the graded disjunction supports the annihilator 1, then such operator is called hard; if the annihilator 1 is not supported, then the operator is called soft. The hard graded conjunction can be verbalized as the "must have" condition, where each input is considered mandatory, so that its nonsatisfaction unconditionally yields the output 0. The hard graded disjunction can be verbalized as the "enough to have" condition, where each input is considered sufficient to fully satisfy stakeholder's requirements: its value 1 unconditionally yields the output 1. Both the graded conjunction and the graded disjunction can be soft, verbalized as the "nice to have" condition where the properties of aggregation are conjunctive or disjunctive, but the annihilators are not supported. Both hard and soft logic aggregators are provably present and used in human reasoning.

The basic Graded Conjunction/Disjunction (basic GCD) is the fundamental GL aggregation function that includes and integrates 7 types of logic aggregation: full conjunction, hard graded conjunction, soft graded conjunction, neutrality (the weighted arithmetic mean), soft graded disjunction, hard graded disjunction, and the full disjunction. The basic GCD and negation are sufficient to create all other compound GL functions, such as graded absorption, implication, abjunction, equivalence, exclusive disjunction, and others. In vertices of the unit hypercube GL and the classical Boolean logic are identical. Therefore, GL is a seamless generalization of the classical Boolean logic inside the whole unit hypercube.

Conjunctive properties can be stronger than the full conjunction, and disjunctive properties can be stronger than the full disjunction. The extreme conjunctive function is called the drastic conjunction (the function where the output is 1 only if all inputs are 1, and in all other cases the output is 0). The extreme disjunctive function is called the drastic disjunction (the function where the output is 0 only if all inputs are 0, and in all other cases the output is 1). To cover the full spectrum of logic aggregators in GL we also use the extended GCD, which is a function that provides the andness-directed continuous transition from the drastic conjunction to the drastic disjunction. The extended GCD includes the basic GCD in the segment between the pure conjunction and the pure disjunction. All forms of GCD satisfy De Morgan duality.

The extended GCD in the range of high andness between the full conjunction and the drastic conjunction is called hyperconjunction. Similarly, hyperdisjunction is the extended GCD in the high orness range between the full disjunction and the drastic disjunction. Hyperconjunction covers the area of t-norms and the hyperdisjunction covers the area of t-conorms. That includes the product t-norms/t- conorms, which model the probability of independent events. In this way GL includes models of probabilistic reasoning, building useful bridges between logic and the probability theory.

One of central results of GL is the graded logic conjecture which claims that 10 basic types of logic functions, consisting of 7 function types of basic GCD, hyperconjunction, hyperdisjunction, and negation are necessary and sufficient to adequately model mental processes when human beings aggregate subjective categories, i.e., degrees of truth corresponding to various graded percepts. After selecting an appropriate type of GCD aggregator, humans regularly perform fine tuning of aggregator by additionally adjusting both the desired importance and the desired andness/orness. The extended GCD and negation are necessary and sufficient components for building a graded propositional calculus that can process graded/partial truth in a way consistent with observable properties of human reasoning.

GL is highly applicable and supported by collection of professional software tools. In industrial setting, GL is the fundamental component of decision engineering, an area of professional decision- making based on complex logic criteria, that can use hundreds of inputs. Published applications of GL are in the areas of ecology, evaluation, optimization, and selection of computer hardware and software, medicine (evaluation of disease severity and patient disability), public health (evaluation of priority for vaccination), geography and space management (suitability maps), agriculture, urban planning, evaluation of data management systems, web browsers, search engines, windowed environments, websites, e-commerce sites, homes (in online real estate), groundwater contamination, cybersecurity, and others. A detailed presentation of GL, a presentation of decision engineering applications of GL (evaluation, optimization, comparison, and selection of complex alternatives), as well as a survey of the GL-based LSP decision method and corresponding literature can be found in the monograph by J. Dujmović.


[1] Jozo Dujmović (2018): Soft Computing Evaluation Logic: The LSP Decision Method and Its Applications. John Wiley & Sons, Inc., doi:10.1002/9781119256489.