repositorio.ufrn.br · Catalogação da Publicação na Fonte. UFRN / SISBI / Biblioteca Setorial...

Thiago Nascimento da Silva

Algebraic semantics for Nelson’s logic 𝒮

Natal, RN, Brasil

2017



Dissertação de Mestrado apresentada ao Pro-grama de Pós-Graduação em Sistemas eComputação como requisito parcial paraobtenção do título de Mestre em Sistemas eComputação.

Universidade Federal do Rio Grande do Norte – UFRN

Departamento de Informática e Matemática Aplicada – DIMAp

Programa de Pós-Graduação em Sistemas e Computação – PPgSC

Supervisor: Umberto Rivieccio

Co-supervisor: João Marcos de Almeida

Natal, RN, Brasil

2017

Catalogação da Publicação na Fonte. UFRN / SISBI / Biblioteca Setorial

Especializada do Centro de Ciências Exatas e da Terra – CCET.

Elaborado por Joseneide Ferreira Dantas - CRB-15/324

Silva, Thiago Nascimento da.

Algebraic semantics for Nelson’s logic S / Thiago Nascimento da Silva. – 2017.

64 f.

Dissertação (mestrado) – Universidade Federal do Rio Grande do Norte, Centro

de Ciências Exatas e da Terra, Departamento de Informática e Matemática Aplicada,

Programa de Pós-Graduação em Sistemas e Computação. Natal, RN, 2017.

Orientador: Umberto Rivieccio.

Coorientador: João Marcos de Almeida.

1. Lógica algébrica – Dissertação. 2. Semântica – Dissertação. 3. Lógicas de

Nelson – Dissertação. I. Rivieccio, Umberto. II. Almeida, João Marcos de. III.

Título.

RN/UF/BSE-CCET CDU 510.6



Dissertação de Mestrado apresentada ao Pro-grama de Pós-Graduação em Sistemas eComputação como requisito parcial paraobtenção do título de Mestre em Sistemas eComputação.

Trabalho aprovado. Natal, RN, Brasil, 25 de janeiro de 2018:

Prof. Dr. Umberto RivieccioOrientador - Presidente

Prof. Dr. João Marcos de AlmeidaCo-orientador

Prof. Dr. Hugo Luiz MarianoMembro Externo

Natal, RN, Brasil2017

To my family, for their endless support.

Acknowledgements

In conclusion of these two years of studying I am grateful for everything I expe-

rienced and I owe gratitude to some special people who contributed to my journey. To

my advisers João Marcos (In the first year) and Umberto Rivieccio (In the second year)

- thanks for the guidance and patience. To my friends from the Logic group (Carol (in

memoriam), Evelyn, Hudson, João Daniel, Patrick, Raquel and Sanderson) for their con-

tinuous contributions both logic and english, as well as philosophy. To my friends from

UFES (Aaron, Bruno, Eneas and José) for the years that we spent studying together. For

all the effort to guarantee my admission in the master’s degree I would like to thanks

Professor João Marcos, Helida and Professor Uirá. I am also grateful to the professors

Elaine Pimentel and Matthew Spinks for their valued contribution to my work. I would

like to express gratitude to my family for all the indispensable support. Napoleão and

Rony, without their support I couldn´t continue my studies. Nilson and Luciene, and

Fran, thanks for helping with my moving to Natal. Finally, to Ana Paula, thanks for your

daily help, support and comprehension.

“And you shall know the truth, and the truth shall set you free.”

— John 8:32, Bible

ResumoAlém da mais conhecida lógica de Nelson (𝒩 3) e da lógica paraconsistente de Nelson

(𝒩 4), David Nelson introduziu no artigo de 1959 "Negation and separation of concepts

in constructive systems", com motivações de aritmética e construtividade, a lógica que

ele chamou de "𝒮". Naquele trabalho, a lógica é definida por meio de um cálculo (que

carece crucialmente da regra de contração) tendo infinitos esquemas de regras, e nenhuma

semântica é fornecida.

Neste trabalho nós tomamos o fragmento proposicional de 𝒮, mostrando que ele é alge-

brizável (de fato, implicativo) no sentido de Blok & Pigozzi com respeito a uma classe

de reticulados residuados involutivos. Assim, fornecemos a primeira semântica para 𝒮

(que chamamos de 𝒮-álgebras), bem como um cálculo estilo Hilbert finito equivalente à

apresentação de Nelson. Fornecemos um algoritmo para construir 𝒮-álgebras a partir de

𝒮-álgebras ou reticulados implicativos e demonstramos alguns resultados sobre a classe

de álgebras que introduzimos. Nós também comparamos 𝒮 com outras lógicas da família

de Nelson, a saber, 𝒩 3 e 𝒩 4.

Palavras-chaves: Lógica, Lógicas de Nelson, Lógicas construtivistas, Negação forte,

Lógica de Nelson paraconsistente, Lógicas subestruturais, Reticulados residuados três-

potente, Lógica algébrica.

AbstractBesides the better-known Nelson logic (𝒩 3) and paraconsistent Nelson logic (𝒩 4), in

Negation and separation of concepts in constructive systems (1959) David Nelson intro-

duced a logic that he called 𝒮, with motivations of arithmetic and constructibility. The

logic was defined by means of a calculus (crucially lacking the contraction rule) having

infinitely many rule schemata, and no semantics was provided for it.

We look in the present dissertation at the propositional fragment of 𝒮, showing that it

is algebraizable (in fact, implicative) in the sense of Blok and Pigozzi with respect to a

class of involutive residuated lattices. We thus provide the first known algebraic semantics

for 𝒮(we call them of 𝒮-algebras) as well as a finite Hilbert-style calculus equivalent to

Nelson’s presentation. We provide an algorithm to make 𝒮-algebras from 𝒮-algebras or

implicative lattices and we prove some results about the class of algebras which we have

introduced. We also compare 𝒮 with other logics of the Nelson family, that is, 𝒩 3 and

𝒩 4.

Key-words: Logic, Nelson’s logics, Constructive logics, Strong negation, Paraconsistent

Nelson logic, Substructural logics, Three-potent residuated lattices, Algebraic logic.

Contents

Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

1 NELSON’S LOGIC 𝒮 . . . . . . . . . . . . . . . . . . . . . . . . . . 19

1.1 A brief introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

1.2 Nelson’s logic 𝒮 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

2 ALGEBRAIZATION . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

2.1 𝒮 is algebraizable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

2.2 𝒮-algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

2.3 𝒮-algebras as residuated lattices . . . . . . . . . . . . . . . . . . . . . 31

3 CALCULUS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

3.1 A finite Hilbert-style calculus for 𝒮 ′ . . . . . . . . . . . . . . . . . . . 35

3.2 Deduction theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

4 MORE ON 𝒮-ALGEBRAS . . . . . . . . . . . . . . . . . . . . . . . 43

4.1 ℒ3 algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

4.2 Making 𝒮-algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

5 RELATION WITH 𝒩 3 AND 𝒩 4 . . . . . . . . . . . . . . . . . . . . 47

5.1 𝒩 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

5.2 𝒩 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

6 CONCLUSION . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

7 FUTURE WORK . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

BIBLIOGRAPHY . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

17

PrefaceIn order to study the notion of constructible falsity, David Nelson introduced a

few systems of non-classical logic. Nelson’s systems combine an intuitionistic approach

to truth and a dual-intuitionistic treatment of falsity. The logics introduced by Nelson

(𝒮, 𝒩 3, and 𝒩 4) accept some important theorems of classical logic, like ¬¬𝜑 ⇔ 𝜑, while

rejecting others, like (𝜑 ⇒ (𝜑 ⇒ 𝜓)) ⇒ (𝜑 ⇒ 𝜓) and (𝜑 ∧ ¬𝜑) ⇒ 𝜓. Nelson introduced

these logics with the aim of studying constructive proofs in Number Theory. To such

an end he gave a definition of truth [Nelson, 1949, Definition 1] (analogous to Kleene’s

[Kleene, 1945, p. 112]) according to which a formula could be either affirmed or denied.

The main logic which we are going to study in this work does not respect the

formula (𝑝∧¬𝑝) ⇒ 𝑞. In logics respecting this formula, every theory containing a formula

and its negation is trivial, that is, all formulas are in the theory. Paraconsistents logics

are a weakening of classical logic lacking this formula, we can have a theory that has a

conjunction of a formula and its negation, but is not trivial. Besides the philosophical and

mathematical interest about these, there is aplicational interest for computer science. As

an example we can mention a database having a considerable amount of information. It

is plausible to consider that the database has information that contradicts each other,

either in storing incorrect information or in having more than one source. One can fix

the problem by eliminating the contradictory information, but in doing that we may lose

importation information. Another way is to use some paraconsistent logic to infer results.

Results about the application of paraconsistent logics in computer science can be seen in

[Abe et al., 2015, Chapter 6].

The first system for studying constructible falsity is introduced in [Nelson, 1949]

and is nowadays known as Nelson’s logic, called 𝒩 3 following [Odintsov, 2008]. A paracon-

sistent version of 𝒩 3, called nowadays 𝒩 4, was introduced in [Almukdad and Nelson, 1984].

In fact 𝒩 3 is an axiomatic extension of 𝒩 4 by the axiom ¬𝜑 → (𝜑 → 𝜓). The logic

𝒩 3 is well studied, both in a proof-theoretic approach and through algebraic methods

[Odintsov, 2008]. For 𝒩 4 the results are more recent and due to the work of Odintsov

[Odintsov, 2008] we know that 𝒩 4 (and also 𝒩 3) is algebraizable in the sense of Blok

and Pigozzi [Blok and Pigozzi, 1989].

Besides 𝒩 3 and 𝒩 4, Nelson introduced a logic which he called 𝒮 [Nelson, 1959],

18 CONTENTS

also aimed at the study of the concept of realizability. The original presentation of 𝒮 by

Nelson has infinite rule schemata, no algebraic semantics is offered, and it is not clear

whether 𝒩 3 is weaker or stronger than 𝒮. Unlike 𝒩 3 and 𝒩 4, the logic 𝒮 received little

attention and some basic questions about 𝒮 were still open. Can 𝒮 be finitely axiomatized?

What is the exact relation between 𝒮, 𝒩 3 and 𝒩 4? Are the formulas that Nelson claims

not to be derivable in 𝒮 [Nelson, 1959, p. 213] indeed not derivable? We will here use the

modern techniques of algebraic logic to answer these questions. In addition, employing an

algebraic semantics based on distributive lattices we will show that the (corrected version

of) Nelson’s presentation of 𝒮 has redundant rules.

The dissertation is organized as follows. In Chapter 1 we give a short introduction

remembering the basic concepts about algebraic logic, we present the logic 𝒮 and derive

some formulas which will later be used to establish its algebraizability. In Chapter 2 we

prove that 𝒮 is implicative and as consequence of this it is also algebraizable and we

present its equivalent algebraic semantics. We give for 𝒮 two presentations for its seman-

tics. The first one is given directly from its algebraizability thanks to the algorithm of

[Blok and Pigozzi, 1989, Theorem 2.17], the second one is given thanks to the result that

the class of algebras which are a semantics for 𝒮 is a variety. In Chapter 3 we provide an-

other calculus for 𝒮 (which is an axiomatic extension of 𝐹𝐿𝑒𝑤 [Spinks and Veroff, 2008b]),

one that has finite axiom schemata and only one rule schema, modus ponens. Having only

one rule it is much easier to prove the Deduction Metatheorem using induction over deriva-

tions. In Chapter 4 we provide an algorithm to producing 𝒮-algebras from 𝒮-algebras or

implicative lattices and give concrete 𝒮-algebras which provide counter-examples for the

formulas that Nelson claimed to be invalid in 𝒮. In Chapter 5 we prove that 𝒩 3 is a

proper axiomatic extension of 𝒮 and that 𝒮 and 𝒩 4 are not comparable, we show that

we can obtain 𝒩 3 from 𝒮 by adding one axiom. Finishing the dissertation, we show that

the variety of 𝒮-algebras is not finitely generated.

19

1 Nelson’s logic 𝒮Studying algebraic logic, we establish using algebraic methods a bridge between

proof theoretic view and algebraic semantics view. In this chapter we define the basics

concepts that we use to make this bridge, recall Nelson’s original presentation of the

propositional fragment of 𝒮 [Nelson, 1959] and prove some theorems in 𝒮 that will be

used later to establish its algebraizability. The logic which we are going to study in this

dissertation it is a fixed version of 𝒮. Nelson’s original presentation has many typos, we

have fixed the typos and told why we thought that our version is correct.

1.1 A brief introduction

Definition 1. A language is a pair L = ⟨𝐿, ar⟩ where 𝐿 ̸= ∅ is a set and ar : 𝐿 −→ 𝜔 is

a function. Take 𝑠 ∈ 𝐿, we say that ar(𝑠) is the arity of 𝑠.

∙ Take 𝑠 ∈ 𝐿, if ar(𝑠) = 0, then 𝑠 is said to be a constant.

∙ If ar(𝑠) = 𝑛, where 𝑛 > 0, then 𝑛 is said to be a connective. If ar(𝑠) = 1, then 𝑠 is

a unary connective. If ar(𝑠) = 2, then 𝑠 is a binary connective.

In our case, two constants will have constant use: ⊥ (bottom) and ⊤ (top), which represent

falsity and truth, respectively. Their interpretation in the algebra will be minimum (0)

and maximum (1) of the algebra, respectively.

Definition 2. Let Var be an infinite set and L = ⟨𝐿, ar⟩ be a language with Var ∩ 𝐿 =

∅. The L-algebra of formulas Fm above Var is given by the following clausules:

1. Var ⊆ Fm.

2. If 𝑠 ∈ 𝐿 is such that ar(𝑠) = 0, then 𝑠 ∈ Fm.

3. If 𝑠 ∈ 𝐿 is such that ar(𝑠) = 𝑛 > 0, then 𝑠(𝜙1, · · · , 𝜙𝑛) ∈ Fm, where 𝜙𝑖 ∈ Fm.

Definition 3. An evaluation is any homomorphism 𝑣 : Fm −→ A, where A is an algebra

with same similarity of Fm, that is, of type 𝐿.

20 Chapter 1. Nelson’s logic 𝒮

Definition 4. Let Fm be a set of formulas, henceforth the set of equations of the language

L is denoted by E𝑞 and is defined as E𝑞 := Fm × Fm.

We write 𝜑 ≈ 𝜓 rather than (𝜑, 𝜓). We say that an evaluation 𝜐 satisfies 𝜑 ≈ 𝜓 in A

when 𝜐(𝜑) = 𝜐(𝜓). We say that an L-algebra A satisfies 𝜑 ≈ 𝜓 when all evaluations in

A satisfies it, we use the notation A |= 𝜑 ≈ 𝜓.

Definition 5. A substitution is any endomorphism 𝜌 : Fm −→ Fm.

Definition 6. A logic is a pair ℒ = ⟨L,⊢ℒ⟩ where L is a language and

⊢ℒ⊆ P(Fm) × Fm is a relation satisfying the following properties, for all

Γ ∪ Δ ∪ {𝜑} ⊆ Fm:

(I) Identity: If 𝜑 ∈ Γ, then (Γ, 𝜑) ∈ ⊢ℒ.

(M) Monotonicity: (Γ, 𝜑) ∈ ⊢ℒ and Γ ⊆ Δ, then (Δ, 𝜑) ∈ ⊢ℒ.

(T) Transitivity: (Γ, 𝜑) ∈ ⊢ℒ and (Δ, 𝜓) ∈⊢ℒ for every 𝜓 ∈ Γ, then (Δ, 𝜑) ∈⊢ℒ.

(S) Structurality: If (Γ, 𝜑) ∈ ⊢ℒ, then (𝜌Γ, 𝜌𝜑) ∈ ⊢ℒ for every substituition 𝜌.

We are going to write Γ ⊢ℒ 𝜑 to designate (Γ, 𝜑) ∈ ⊢ℒ and a formula 𝜑 such that ∅ ⊢ℒ 𝜑

is said to be a theorem.

1.2 Nelson’s logic 𝒮

Definition 7. Nelson’s logic 𝒮 = ⟨Fm,⊢𝒮⟩ is the sentential logic in the language

⟨∧,∨,⇒,¬,⊥⟩ of type ⟨2, 2, 2, 1, 0⟩ defined by the Hilbert-style calculus with the rule

schemata in Table 1 and the following axiom schemata. Hereupon we shall use 𝜑 ⇔ 𝜓 as

an abbreviation for (𝜑 ⇒ 𝜓) ∧ (𝜓 ⇒ 𝜑).

Axioms

(A1) 𝜑 ⇒ 𝜑

(A2) ⊥ ⇒ 𝜑

(A3) ¬𝜑 ⇒ (𝜑 ⇒ ⊥)

(A4) ¬⊥

(A5) (𝜑 ⇒ 𝜓) ⇔ (¬𝜓 ⇒ ¬𝜑).

1.2. Nelson’s logic 𝒮 21

Rules

Γ ⇒ (𝜑 ⇒ (𝜓 ⇒ 𝛾))Γ ⇒ (𝜓 ⇒ (𝜑 ⇒ 𝛾)) (P)

𝜑 ⇒ (𝜑 ⇒ (𝜑 ⇒ 𝛾))𝜑 ⇒ (𝜑 ⇒ 𝛾) (C)

Γ ⇒ 𝜑 𝜑 ⇒ 𝛾

Γ ⇒ 𝛾(E)

Γ ⇒ 𝜑 𝜓 ⇒ 𝛾

Γ ⇒ ((𝜑 ⇒ 𝜓) ⇒ 𝛾) (⇒ l) 𝛾

𝜑 ⇒ 𝛾(⇒ r)

𝜑 ⇒ 𝛾

(𝜑 ∧ 𝜓) ⇒ 𝛾(∧l1)

𝜓 ⇒ 𝛾

(𝜑 ∧ 𝜓) ⇒ 𝛾(∧l2) Γ ⇒ 𝜑 Γ ⇒ 𝜓

Γ ⇒ (𝜑 ∧ 𝜓) (∧r) 𝜑 ⇒ 𝛾 𝜓 ⇒ 𝛾

(𝜑 ∨ 𝜓) ⇒ 𝛾(∨l1)

(𝜑 ⇒2 𝛾) (𝜓 ⇒2 𝛾)((𝜑 ∨ 𝜓) ⇒2 𝛾)

(∨l2) Γ ⇒ 𝜑

Γ ⇒ (𝜑 ∨ 𝜓) (∨r1) Γ ⇒ 𝜓

Γ ⇒ (𝜑 ∨ 𝜓) (∨r2)

(𝜑 ∧ ¬𝜓) ⇒ 𝛾

¬(𝜑 ⇒ 𝜓) ⇒ 𝛾(¬ ⇒ l)

Γ ⇒2 (𝜑 ∧ ¬𝜓)Γ ⇒2 ¬(𝜑 ⇒ 𝜓)

(¬ ⇒ r) (¬𝜑 ∨ ¬𝜓) ⇒ 𝛾

¬(𝜑 ∧ 𝜓) ⇒ 𝛾(¬ ∧ l)

Γ ⇒ (¬𝜑 ∨ ¬𝜓)Γ ⇒ ¬(𝜑 ∧ 𝜓) (¬ ∧ r)

(¬𝜑 ∧ ¬𝜓) ⇒ 𝛾

¬(𝜑 ∨ 𝜓) ⇒ 𝛾(¬ ∨ l)

Γ ⇒ (¬𝜑 ∧ ¬𝜓)Γ ⇒ ¬(𝜑 ∨ 𝜓) (¬ ∨ r)

𝜑 ⇒ 𝛾

¬¬𝜑 ⇒ 𝛾(¬¬l) Γ ⇒ 𝜑

Γ ⇒ ¬¬𝜑 (¬¬r)

Table 1 – Rules of 𝒮

In Table 1, following Nelson’s notation, Γ = (𝜑1, . . . , 𝜑𝑛) is an arbitrary finite list

of formulas, and the following abbreviations are used:

Γ ⇒ 𝜑 := 𝜑1 ⇒ (𝜑2 ⇒ (. . . ⇒ (𝜑𝑛 ⇒ 𝜑) . . .)).

In case Γ is empty, then Γ ⇒ 𝜑 is just 𝜑. Moreover, we let

𝜑 ⇒2 𝜓 := 𝜑 ⇒ (𝜑 ⇒ 𝜓)

and

Γ ⇒2 𝜑 := 𝜑1 ⇒2 (𝜑2 ⇒2 (. . . ⇒2 (𝜑𝑛 ⇒2 𝜑) . . .)).

We have fixed obvious typos in the rules (∧l2), (∧r) and (¬ ⇒ r) as they appear in

[Nelson, 1959, p. 214-5]. The original rule (∧l2) in Nelson’s paper was:

(𝜑 ∧ 𝜓) ⇒ 𝛾

𝜓 ⇒ 𝛾(∧l2)

This clearly makes the logic inconsistent. Indeed, taking 𝜑 = 𝛾, we have:

(𝜑 ∧ 𝜓) ⇒ 𝜑

𝜓 ⇒ 𝜑(∧l2)


As (𝜑 ∧ 𝜓) ⇒ 𝜑 is a theorem (Proposition 1.3), 𝜓 ⇒ 𝜑 is a theorem too. Choosing 𝜓 as

an axiom, we have that 𝜑 is a theorem for all formulas 𝜑.

The original rule (∧r) in Nelson’s paper was:

Γ ⇒ (𝜑 ∧ 𝜓)Γ ⇒ 𝜑 Γ ⇒ 𝜓

(∧r)

This rule does not seem consistent with the notation used by Nelson for the others (Nelson

was presenting rules from introduction, this rule is eliming the conjunction). Moreover, it

can be proved from other rules of 𝒮.

Γ ⇒ (𝜑 ∧ 𝜓) (𝜑 ∧ 𝜓) ⇒ 𝜑

Γ ⇒ 𝜑(E)

The other case is analogous.

The rule (¬ ⇒ r) appeared in Nelson’s paper as follows:

Γ ⇒2 ¬(𝜑 ⇒ 𝜓)Γ ⇒2 (𝜑 ∧ 𝜓)

(¬ ⇒ r)

This rule is not even classically valid. Following Nelson’s notation, the correct rule would

have been:

Γ ⇒2 ¬(𝜑 ⇒ 𝜓)Γ ⇒2 (𝜑 ∧ ¬𝜓)

(¬ ⇒ r)

This rule does not seem consistent with the notation used by Nelson for the others (the

⇒ connective should appear on the right-hand side at the bottom, and the ∧ connective

at the top); moreover, it is redundant. To see this notice that, using (¬ ⇒ l), we can show

that the formula ¬(𝜑 ⇒ 𝜓) ⇒ (𝜑∧ ¬𝜓) is a theorem of 𝒮 (that is, it is derivable from an

empty set of premises):

(𝜑 ∧ ¬𝜓) ⇒ (𝜑 ∧ ¬𝜓) (A1)

¬(𝜑 ⇒ 𝜓) ⇒ (𝜑 ∧ ¬𝜓) (¬ ⇒ l)

Now using (E) we have:

Γ ⇒2 ¬(𝜑 ⇒ 𝜓) ¬(𝜑 ⇒ 𝜓) ⇒ (𝜑 ∧ ¬𝜓)Γ ⇒2 (𝜑 ∧ ¬𝜓)

1.2. Nelson’s logic 𝒮 23

Rule (C), called weak condensation by Nelson, replaces (and is indeed a weaker form of)

the standard contraction rule:𝜑 ⇒ (𝜑 ⇒ 𝜓)

𝜑 ⇒ 𝜓

(C) is also known in the literature as 3-2 contraction (see, e.g., [Restall, 1993, p. 389])

and corresponds to the algebraic property of 3-potency (see Section 2.3). Notice also that

the usual rule of modus ponens is an instance of (E) for Γ = ∅:

𝜑 𝜑 ⇒ 𝜓

𝜓(MP)

Lastly, we observe that every rule schema involving Γ is actually a shorthand for a denu-

merably infinite set of rule schemata. For instance, the schema

Γ ⇒ 𝜑 𝜓 ⇒ 𝛾

Γ ⇒ ((𝜑 ⇒ 𝜓) ⇒ 𝛾) (⇒ l)

stands for the following collection of rules:

𝜑 𝜓 ⇒ 𝛾

(𝜑 ⇒ 𝜓) ⇒ 𝛾

𝛾1 ⇒ 𝜑 𝜓 ⇒ 𝛾

𝛾1 ⇒ ((𝜑 ⇒ 𝜓) ⇒ 𝛾)

· · ·

𝛾1 ⇒ (𝛾2 ⇒ (𝛾3 ⇒ 𝜑)) 𝜓 ⇒ 𝛾

𝛾1 ⇒ (𝛾2 ⇒ (𝛾3 ⇒ ((𝜑 ⇒ 𝜓) ⇒ 𝛾)))

· · ·

One of the crucial steps to prove that a logic is algebraizable (in the sense of Blok and

Pigozzi [Blok and Pigozzi, 1989, Definition 2.2]) is to prove that it satisfies certain con-

gruence properties. In our context, this entails checking that 𝜑 ⇔ 𝜓 ⊢𝒮 ¬𝜑 ⇔ ¬𝜓 and

{𝜑1 ⇔ 𝜓1, 𝜑2 ⇔ 𝜓2} ⊢𝒮 (𝜑1 ∙ 𝜑2) ⇔ (𝜓1 ∙ 𝜓2) for each connective ∙ ∈ {∧,∨,⇒}. The

following result will be used to prove it in the next chapter.

Example 1. The following formulas are theorems of 𝒮:

1. 𝜑 ⇒ (𝜑 ∨ 𝜓).


2. 𝜓 ⇒ (𝜑 ∨ 𝜓).

3. (𝜑 ∧ 𝜓) ⇒ 𝜑.

4. (𝜑 ∧ 𝜓) ⇒ 𝜓.

5. (𝜑 ⇒ (𝜓 ⇒ 𝛾)) ⇔ (𝜓 ⇒ (𝜑 ⇒ 𝛾)).

Proof. All derivations are straightforward. We illustrate the first item as an example.

Taking Γ = 𝜑 in rule (∨r1), we have

𝜑 ⇒ 𝜑

𝜑 ⇒ (𝜑 ∨ 𝜓)

Since 𝜑 ⇒ 𝜑 is an axiom, it follows that 𝜑 ⇒ (𝜑 ∨ 𝜓) is a theorem of 𝒮.

25

2 AlgebraizationIn this chapter we prove that 𝒮 is algebraizable in the sense of Blok and Pigozzi

(and, in fact, is implicative [Font, 2016, Definition 2.3]), and we give two equivalent pre-

sentations for its equivalent algebraic semantics (to be called 𝒮-algebras). The first one is

obtained via the algorithm of [Blok and Pigozzi, 1989, Theorem 2.17], while the second

one is closer to the usual axiomatizations of classes of residuated lattices, which are the

algebraic counterpart of many logics in the substructural family. The second presentation

of 𝒮-algebras will allow us to see at a glance that they form an equational class, and also

makes it easier to compare them with other known classes of algebras of substructural

logics.

2.1 𝒮 is algebraizable

Definition 8. An implicative logic is a logic ℒ in a language Σ having a term 𝛼(𝑝, 𝑞) in

two variables that satisfies the following:

IL1 ⊢ℒ 𝛼(𝑝, 𝑝)

IL2 𝛼(𝑝, 𝑞), 𝛼(𝑞, 𝑟) ⊢ℒ 𝛼(𝑝, 𝑟)

IL3 ⋃︀𝑛𝑖=1{𝛼(𝑝𝑖, 𝑞𝑖), 𝛼(𝑞𝑖, 𝑝𝑖)} ⊢ℒ 𝛼(𝜆𝑝1 . . . 𝑝𝑛, 𝜆𝑞1 . . . 𝑞𝑛) for each 𝑛-ary 𝜆 in Σ

IL4 𝑝, 𝛼(𝑝, 𝑞) ⊢ℒ 𝑞

IL5 𝑞 ⊢ℒ 𝛼(𝑝, 𝑞)

Clarifying the notation in IL3, if ar(𝜆) = 1, then the notation 𝛼(𝜆𝜑𝑖 · · ·𝜑𝑛, 𝜆𝜓𝑖 · · ·𝜓𝑛)

means that 𝛼(𝜆𝜑, 𝜆𝜓). If ar(𝜆) = 2, then 𝛼(𝜑1𝜆𝜑2, 𝜓1𝜆𝜓2).

Defining the relations:

𝑝 ≡ 𝑞 if and only if ∅ ⊢ℒ 𝛼(𝑝, 𝑞) 𝑎𝑛𝑑 ∅ ⊢ℒ 𝛼(𝑞, 𝑝)

𝑝 ≤ℒ 𝑞 if and only if ∅ ⊢ℒ 𝛼(𝑝, 𝑞)

∙ According items IL1 and IL2, ≤ℒ is a quasiorder in ℒ and that the relation ≤ℒ

defines an order ≤ in the algebra quotient Fm/≡.

26 Chapter 2. Algebraization

∙ Item IL3 tell us that the relation ≤ℒ is a congruence of the formula algebra Fm

and the quotient Fm/≡ is an algebra of type Σ.

∙ Item IL4 tell us that the set of theorems is an upset, that is, if ∅ ⊢ℒ 𝑝 and 𝑝 ≤ℒ 𝑞,

then ∅ ⊢ℒ 𝑞 and the canonical projection of Fm into Fm/≡ has the following

property: For all 𝑝 ∈ Fm, ∅ ⊢ℒ 𝑝 if and only if 𝑝 ∈ Thm/≡, where Thm is the set

of theorems of ℒ. Moreover, Thm/≡ is an upset of order ≤ in Fm/≡.

∙ Finalizing, item IL5 tell us that all theorems are in the same class in the algebra

Fm/≡.

Definition 9. Let ℒ be an implicative logic in the language Σ. An ℒ-algebra is an algebra

A of type Σ whose carrier has an element 1 ∈ 𝐴 with the following features:

(LALG1) For all Γ ∪ {𝜑} ⊆ Fm and all valuation 𝜐 , if Γ ⊢ℒ 𝜑 and 𝜐(Γ) ⊆ {1}, then

𝜐(𝜑) = 1.

(LALG2) For all 𝑎, 𝑏 ∈ 𝐴, if 𝛼(𝑝, 𝑞) = 1 and 𝛼(𝑞, 𝑝) = 1, then 𝑎 = 𝑏.

The class of ℒ-algebras is denoted by Alg*ℒ.

It will be convenient for us to work with the following definition of algebraizable

logic, which is not the original one [Blok and Pigozzi, 1989, Definition 2.1] but an equiv-

alent so-called intrinsic characterization [Blok and Pigozzi, 1989, Theorem 3.21].

Definition 10. A logic ℒ is algebraizable if and only if there are finite and non-empty

set of equations E(𝑥) ⊆ E𝑞 and formulas Δ(𝑥, 𝑦) ⊆ 𝐹𝑚 such that ℒ satisfies the following

five conditions:

(R) ⊢ℒ Δ(𝜑, 𝜑)

(Sym) Δ(𝜑, 𝜓) ⊢ℒ Δ(𝜓, 𝜑)

(Trans) Δ(𝜑, 𝜓) ∪ Δ(𝜓, 𝛾) ⊢ℒ Δ(𝜑, 𝛾)

(Re) ⋃︀𝑛𝑖=1 Δ(𝜑𝑖, 𝜓𝑖) ⊢ℒ Δ(𝜆𝜑1 · · ·𝜑𝑛, 𝜆𝜓1 · · ·𝜓𝑛) for each 𝑛-ary 𝜆 ∈ Σ

(Alg3) 𝜑 ⊣⊢ℒ Δ(E(𝜑))

2.1. 𝒮 is algebraizable 27

Then E(𝑥) is said to be the set of defining equations and Δ(𝑥, 𝑦) is the set of equivalence

formulas.

Every implicative logic ℒ is algebraizable with respect to the class Alg*ℒ [Font, 2016,

Proposition 3.15], and the algebraizability is witnessed by the defining equation 𝜏(𝜑) :=

{𝜑 ≈ 𝛼(𝜑, 𝜑)} and the equivalence formulas 𝜌(𝜑 ≈ 𝜓) := {𝛼(𝜑, 𝜓), 𝛼(𝜓, 𝜑)}. Since the

term 𝛼(𝜑, 𝜑) denotes an algebraic constant in all ℒ-algebras, it is often denoted simply

by ⊤ or 1 (as we shall also do below). In the case of 𝒮, the term 𝛼(𝑝, 𝑞) can be chosen to

be 𝑝 ⇒ 𝑞.

Theorem 1. The calculus ⊢𝒮 is implicative , and thus algebraizable.

Proof. IL1 follows immediately from axiom (A1), while IL2 follows from rule (E). We

have to prove that ⇒ respects IL3 for each connective ∙ ∈ {∧,∨,⇒,¬}.

(¬) {𝜑 ⇔ 𝜓} ⊢𝒮 ¬𝜑 ⇔ ¬𝜓 holds by axiom (A5) and (MP).

(∧) We must prove that {(𝜑1 ⇔ 𝜓1) ∧ (𝜑2 ⇔ 𝜓2)} ⊢𝒮 (𝜑1 ∧ 𝜑2) ⇔ (𝜓1 ∧ 𝜓2). From

Example 1.3 and 1.4 we have ⊢𝒮 (𝜑1 ∧ 𝜑2) ⇒ 𝜑1 and ⊢𝒮 (𝜑1 ∧ 𝜑2) ⇒ 𝜑2. From rule

(E) we have:(𝜑1 ∧ 𝜑2) ⇒ 𝜑1 𝜑1 ⇒ 𝜓1

(𝜑1 ∧ 𝜑2) ⇒ 𝜓1(E)

and again by (E):

(𝜑1 ∧ 𝜑2) ⇒ 𝜑2 𝜑2 ⇒ 𝜓2

(𝜑1 ∧ 𝜑2) ⇒ 𝜓2(E)

Now, by rule (∧r), we have:

(𝜑1 ∧ 𝜑2) ⇒ 𝜓1 (𝜑1 ∧ 𝜑2) ⇒ 𝜓2

(𝜑1 ∧ 𝜑2) ⇒ (𝜓1 ∧ 𝜓2)(∧r)

The remainder of the proof is similar.

(∨) We must prove that {(𝜑1 ⇔ 𝜓1) ∧ (𝜑2 ⇔ 𝜓2)} ⊢𝒮 (𝜑1 ∨ 𝜑2) ⇔ (𝜓1 ∨ 𝜓2). From

Example 1.1 and 1.2, 𝜓1 ⇒ (𝜓1 ∨ 𝜓2) and 𝜓2 ⇒ (𝜓1 ∨ 𝜓2) are derivable. From the

(E) rule we have:𝜑1 ⇒ 𝜓1 𝜓1 ⇒ (𝜓1 ∨ 𝜓2)

𝜑1 ⇒ (𝜓1 ∨ 𝜓2)(E)


and also:𝜑2 ⇒ 𝜓2 𝜓2 ⇒ (𝜓1 ∨ 𝜓2)

𝜑2 ⇒ (𝜓1 ∨ 𝜓2)(E)

Now from rule (∨l1) we have:

𝜑1 ⇒ (𝜓1 ∨ 𝜓2) 𝜑2 ⇒ (𝜓1 ∨ 𝜓2)(𝜑1 ∨ 𝜑2) ⇒ (𝜓1 ∨ 𝜓2)

(∨l1)

The remainder of the proof is similar.

(⇒) We must prove that {(𝜃 ⇔ 𝜑) ∧ (𝜓 ⇔ 𝛾)} ⊢𝒮 (𝜃 ⇒ 𝜓) ⇔ (𝜑 ⇒ 𝛾). This time, using

rule (⇒ l) we have:𝜑 ⇒ 𝜃 𝜓 ⇒ 𝛾

𝜑 ⇒ ((𝜃 ⇒ 𝜓) ⇒ 𝛾) (⇒ l)

Now, from Example 1.5 and (MP), we have:

𝜑 ⇒ ((𝜃 ⇒ 𝜓) ⇒ 𝛾) (𝜑 ⇒ ((𝜃 ⇒ 𝜓) ⇒ 𝛾)) ⇒ ((𝜃 ⇒ 𝜓) ⇒ (𝜑 ⇒ 𝛾))(𝜃 ⇒ 𝜓) ⇒ (𝜑 ⇒ 𝛾) (MP)

The remainder of the proof is analogous.

Finally, IL4 follows from (MP) and IL5 follows from (⇒ r).

2.2 𝒮-algebras

By Blok-Pigozzi’s algorithm ([Blok and Pigozzi, 1989, Theorem 2.17], we have that

the equivalent algebraic semantics of 𝒮 is the class of algebras given in Definition 11 below.

Let Ax the set of axioms of 𝒮 and Inf R the set the inference rules of 𝒮, we define

the algebraic semantics of 𝒮 as follows:

Definition 11. An 𝒮-algebra is a structure A = ⟨𝐴,∧,∨,⇒,¬, 0, 1⟩ of type ⟨2, 2, 2, 1, 0, 0⟩

that satisfies the following equations and quasiequations:

1. E(𝜙), for each 𝜙 ∈ Ax

2. E(Δ(𝜙, 𝜙))

3.𝑛⋃︀𝑖=1

E(𝛾𝑖) implies E(𝜙) for each 𝛾1, · · · , 𝛾𝑛 ⊢𝒮 𝜙 ∈ Inf R

4. E(Δ(𝜙, 𝜓)) implies 𝜙 ≈ 𝜓

2.2. 𝒮-algebras 29

We shall henceforth denote by E(An) the equation given from Definition 11.1 for

the axiom An (for 1 ≤ n ≤ 5) of 𝒮, and by Q(R) the quasiequation given from Definition

11.3 for the rule R of 𝒮. We will also use the following abbreviations: 𝑎 * 𝑏 := ¬(𝑎 ⇒ ¬𝑏),

𝑎2 := 𝑎*𝑎 and 𝑎𝑛 := 𝑎*(𝑎𝑛−1) for 𝑛 > 2. As the notation suggests, the defined connective

* is intended as a “strong conjunction” in the sense of substructural logics (alternative to

the “weak conjunction” ∧) that will be interpreted as a monoid operation on 𝒮-algebras,

and having the implication ⇒ as residuum. We shall now prove a few properties of 𝒮-

algebras that will indeed allow us to view them as a class of residuated structures.

Proposition 1. Let 𝐴 be an 𝒮-algebra and 𝑎, 𝑏, 𝑐 ∈ 𝐴. Then,

1. 𝑎 ⇒ 𝑎 = 𝑏 ⇒ 𝑏 = 1.

2. The relation ≤ defined by 𝑎 ≤ 𝑏 iff 𝑎 ⇒ 𝑏 = 1, is a partial order with maximum 1

and minimum 0.

3. 𝑎 ⇒ 𝑏 = ¬𝑏 ⇒ ¬𝑎.

4. 𝑎 ⇒ (𝑏 ⇒ 𝑐) = 𝑏 ⇒ (𝑎 ⇒ 𝑐).

5. ¬¬𝑎 = 𝑎 and 𝑎 ⇒ 0 = ¬𝑎.

6. ⟨𝐴, *, 1⟩ is a commutative monoid.

7. (𝑎 * 𝑏) ⇒ 𝑐 = 𝑎 ⇒ (𝑏 ⇒ 𝑐).

8. The pair ⟨*,⇒⟩ is residuated with respect to ≤, i.e., 𝑎 * 𝑏 ≤ 𝑐 iff 𝑏 ≤ 𝑎 ⇒ 𝑐.

9. 𝑎2 ≤ 𝑎3.

10. ⟨𝐴,∧,∨⟩ is a lattice with order ≤.

11. (𝑎 ∨ 𝑏)2 ≤ 𝑎2 ∨ 𝑏2.

Proof. 1. Follows from the fact that 𝒮 is an implicative logic, see [Font, 2016, Lemma

2.6]. In particular, ¬0 = 0 ⇒ 0 = 1.

2. By E(A2) we have that 0 is the minimum element with respect to the order ≤. The rest

easily follows from the fact that 𝒮 is implicative.


3. Follows from E(A5) and item 2 above.

4. By Q(P) and 2 above, we have that 𝑑 ≤ 𝑎 ⇒ (𝑏 ⇒ 𝑐) implies 𝑑 ≤ 𝑏 ⇒ (𝑎 ⇒ 𝑐)

for all 𝑑 ∈ 𝐴. Then, taking 𝑑 = 𝑎 ⇒ (𝑏 ⇒ 𝑐), we have 𝑎 ⇒ (𝑏 ⇒ 𝑐) ≤ 𝑏 ⇒ (𝑎 ⇒ 𝑐) which

easily implies the desired result.

5. ¬¬𝑎 = 𝑎 follows from item 2 above together with Q(¬¬l) and Q(¬¬r). By item 3

above, 𝑎 ⇒ 0 = ¬0 ⇒ ¬𝑎 = 1 ⇒ ¬𝑎 = ¬𝑎. The last equality holds because, on the

one hand, by Q(⇒ l) we have that 1 ≤ 1 and ¬𝑎 ≤ ¬𝑎 implies 1 ⇒ ¬𝑎 ≤ ¬𝑎. On

the other, by item 1 we have ¬𝑎 ⇒ ¬𝑎 ≤ 1 and so we can apply Q(⇒ r) to obtain

1 ⇒ (¬𝑎 ⇒ ¬𝑎) = 1. By item 4, we have 1 ⇒ (¬𝑎 ⇒ ¬𝑎) = ¬𝑎 ⇒ (1 ⇒ ¬𝑎), hence we

conclude that ¬𝑎 ⇒ (1 ⇒ ¬𝑎) = 1 and so, by item 2, ¬𝑎 ≤ 1 ⇒ ¬𝑎.

6. As to commutativity, using items 3 and 5 above, we have 𝑎 * 𝑏 = ¬(𝑎 ⇒ ¬𝑏) =

¬(¬¬𝑏 ⇒ ¬𝑎) = ¬(𝑏 ⇒ ¬𝑎) = 𝑏 * 𝑎. As to associativity, using 3, 5, Q(¬¬r) and Q(¬¬l),

we have (𝑎 * 𝑏) * 𝑐 = ¬(¬(𝑎 ⇒ ¬𝑏) ⇒ ¬𝑐)) = ¬(¬¬𝑐 ⇒ ¬¬(𝑎 ⇒ ¬𝑏)) = ¬(𝑐 ⇒ (𝑎 ⇒

¬𝑏)) = ¬(𝑎 ⇒ (𝑐 ⇒ ¬𝑏)) = ¬(𝑎 ⇒ (𝑏 ⇒ ¬𝑐)) = ¬(𝑎 ⇒ ¬¬(𝑏 ⇒ ¬𝑐)) = 𝑎 * (𝑏 * 𝑐). As to 1

being the neutral element, using item 5 above, we have 𝑎 * 1 = 𝑎 * ¬0 = ¬(𝑎 ⇒ ¬¬0) =

¬(𝑎 ⇒ 0) = ¬¬𝑎 = 𝑎.

7. Using items 2, 3, 5 and 6 above, we have (𝑎 * 𝑏) ⇒ 𝑐 = ¬(𝑎 ⇒ ¬𝑏) ⇒ 𝑐 = ¬𝑐 ⇒

¬¬(𝑎 ⇒ ¬𝑏) = ¬𝑐 ⇒ (𝑎 ⇒ ¬𝑏) = 𝑎 ⇒ (¬𝑐 ⇒ ¬𝑏) = 𝑎 ⇒ (¬¬𝑏 ⇒ ¬¬𝑐) = 𝑎 ⇒ (𝑏 ⇒ 𝑐).

8. By item 2 above, we have 𝑎 * 𝑏 ≤ 𝑐 iff (𝑎 * 𝑏) ⇒ 𝑐 = 1 iff, by item 7, 𝑎 ⇒ (𝑏 ⇒ 𝑐) = 1

iff, by 6, 𝑏 ⇒ (𝑎 ⇒ 𝑐) = 1 iff, by 2 again, 𝑏 ≤ 𝑎 ⇒ 𝑐.

9. By Q(C) we have that 𝑎3 ≤ 𝑐 implies 𝑎2 ≤ 𝑐 for all 𝑐 ∈ 𝐴. Then, taking 𝑐 = 𝑎3,

we have 𝑎2 ≤ 𝑎3.

10. We check that 𝑎 ∧ 𝑏 is the infimum of the set {𝑎, 𝑏} with respect to ≤. First of

all, we have 𝑎∧ 𝑏 ≤ 𝑎 and 𝑎∧ 𝑏 ≤ 𝑏 by Q(∧l1), Q(∧l2) and item 2 above. Then, assuming

𝑐 ≤ 𝑎 and 𝑐 ≤ 𝑏, we have 𝑐 ≤ 𝑎∧ 𝑏 by Q(∧r). A similar reasoning, using Q(∨r1), Q(∨r2)

and Q(∨l1) shows that 𝑎 ∨ 𝑏 is the supremum of {𝑎, 𝑏}.

2.3. 𝒮-algebras as residuated lattices 31

11 By 10 we have that 𝑎2 ≤ 𝑎2 ∨ 𝑏2 and 𝑏2 ≤ 𝑎2 ∨ 𝑏2. Hence, by item 8, we have

𝑎 ≤ 𝑎 ⇒ (𝑎2 ∨ 𝑏2) and 𝑏 ≤ 𝑏 ⇒ (𝑎2 ∨ 𝑏2). By item 2 we have then 𝑎 ⇒ (𝑎 ⇒ (𝑎2 ∨ 𝑏2) =

𝑏 ⇒ (𝑏 ⇒ (𝑎2∨𝑏2) = 1, hence we can use Q(∨l2) to obtain (𝑎∨𝑏) ⇒ ((𝑎∨𝑏) ⇒ (𝑎2∨𝑏2) = 1.

Then items 2 and 8 give us (𝑎 ∨ 𝑏)2 ≤ 𝑎2 ∨ 𝑏2 as required.

2.3 𝒮-algebras as residuated lattices

In this section we introduce an equivalent presentation of 𝒮-algebras which takes

precisely the properties in Proposition 1 as postulates. We begin with the following well-

known definitions (see e.g. [Galatos et al., 2007, p. 185]).

Definition 12. A commutative integral bounded residuated lattice (CIBRL) is an algebra

A = ⟨𝐴,∧,∨, *,⇒, 0, 1⟩ of type ⟨2, 2, 2, 2, 0, 0⟩ such that:

1. ⟨𝐴,∧,∨, 0, 1⟩ is a bounded lattice with ordering ≤, minimum element 0 and maxi-

mum 1.

2. ⟨𝐴, *, 1⟩ is a commutative monoid.

3. The pair ⟨*,⇒⟩ is residuated with respect to ≤, i.e., 𝑎 * 𝑏 ≤ 𝑐 iff 𝑏 ≤ 𝑎 ⇒ 𝑐.

Letting ¬𝑥 := 𝑥 ⇒ 0, we say that a residuated lattice is involutive

[Galatos and Raftery, 2004, p. 186] when ¬¬𝑎 = 𝑎 (in such a case, it follows that 𝑎 ⇒

𝑏 = ¬𝑏 ⇒ ¬𝑎)[Ono, 2010,Lemma 3.1]. We say that a residuated lattice is 3-potent when

it satisfies the equation 𝑥2 ≤ 𝑥3. We have defined earlier * from ⇒, and now * is a prim-

itive operation, but we can show that every CIBRL satisfies 𝑥 * 𝑦 := ¬(𝑥 ⇒ ¬𝑦), see

[Galatos and Raftery, 2004, Lemma 5.1].

Definition 13. An 𝒮 ′-algebra is a three-potent involutive CIBRL.

Since CIBRLs form an equational class [Galatos et al., 2007, Theorem 2.7], it is

clear that 𝒮 ′-algebras are also an equational class; by contrast, it is far from obvious from

Definition 11 whether 𝒮-algebras are equationally axiomatizable or not. By Proposition

1, we immediately have the following result.


Proposition 2. Let A = ⟨𝐴,∧,∨,⇒,¬, 0, 1⟩ be an 𝒮-algebra. Letting 𝑥*𝑦 := ¬(𝑥 ⇒ ¬𝑦),

we have that A = ⟨𝐴,∧,∨, * ⇒, 0, 1⟩ is an 𝒮 ′-algebra.

Lemma 1. 1. Any CIBRL satisfies the equation (𝑥 ∨ 𝑦) * 𝑧 ≈ (𝑥 * 𝑧) ∨ (𝑦 * 𝑧).

2. Any CIBRL satisfies 𝑥2 ∨ 𝑦2 ≈ (𝑥2 ∨ 𝑦2)2.

3. Any 3-potent CIBRL satisfies (𝑥 ∨ 𝑦2)2 ≈ (𝑥 ∨ 𝑦)2.

4. Any 3-potent CIBRL satisfies (𝑥 ∨ 𝑦)2 ≈ 𝑥2 ∨ 𝑦2.

Proof. 1. See [Galatos et al., 2007, Lemma 2.6].

2. Let 𝐿 be a CIBRL and 𝑎, 𝑏 arbitrary elements of this lattice. From 𝑎2 ≤ 𝑎2 ∨ 𝑏2

and 𝑏2 ≤ 𝑎2 ∨ 𝑏2, using monotonicity of *, we have 𝑎4 ≤ (𝑎2 ∨ 𝑏2)2 and 𝑏4 ≤ (𝑎2 ∨ 𝑏2)2.

Using 3-potency, the latter inequalities simplify to 𝑎2 ≤ (𝑎2 ∨ 𝑏2)2 and 𝑏2 ≤ (𝑎2 ∨ 𝑏2)2.

Thus, 𝑎2 ∨ 𝑏2 ≤ (𝑎2 ∨ 𝑏2)2.

3. We have 𝑎∨𝑏2 ≤ 𝑎∨𝑏 from monotonicity of * and supremum of ∨, therefore (𝑎∨𝑏2)2 ≤

(𝑎∨𝑏)2. For the converse, we have that 𝑎*𝑏 ≤ 𝑎, whence 𝑎*𝑏 ≤ 𝑎∨𝑏2. Also, as 𝑎2 ≤ 𝑎 and

𝑏2 ≤ 𝑏 from monotonicity of *, we have that 𝑎2 ≤ 𝑎∨ 𝑏2 and 𝑏2 ≤ 𝑎∨ 𝑏2. By supremum of

∨, 𝑎2 ∨ 𝑎 * 𝑏 ∨ 𝑏2 ≤ 𝑎 ∨ 𝑏2. But 𝑎2 ∨ 𝑎 * 𝑏 ∨ 𝑏2 = (𝑎 ∨ 𝑏)2 by Lemma 1, so (𝑎 ∨ 𝑏)2 ≤ 𝑎 ∨ 𝑏2.

Using monotonicity of *, (𝑎 ∨ 𝑏)4 ≤ (𝑎 ∨ 𝑏2)2 and from 3-potency (𝑎 ∨ 𝑏)2 ≤ (𝑎 ∨ 𝑏2)2.

4. From Lemma 1.2 we have (𝑎2 ∨ 𝑏2) = (𝑎2 ∨ 𝑏2)2, and from Lemma 1.3 we have

(𝑎2 ∨ 𝑏2)2 = (𝑎2 ∨ 𝑏)2 = (𝑏 ∨ 𝑎2)2 = (𝑏 ∨ 𝑎)2.

At this point we are in a position to show that, as anticipated, 𝒮 ′-algebras and

𝒮-algebras can be viewed as two presentations (in slightly different languages) of the

same class of structures. For this, we need to check that any 𝒮 ′-algebra satisfies all

(quasi)equations introduced in Definition 11.

Proposition 3. Let A = ⟨𝐴,∧,∨, *,⇒, 0, 1⟩ be an 𝒮 ′-algebra. Letting ¬𝑥 := 𝑥 ⇒ 0, we

have that A = ⟨𝐴,∧,∨,⇒,¬, 0, 1⟩ is an 𝒮-algebra.

Proof. Let A be an 𝒮 ′-algebra. We first consider the equations corresponding to the ax-

ioms of 𝒮. As 𝑎 ≤ 𝑏 iff 𝑎 ⇒ 𝑏 ≈ 1, we usually write 𝑎 ≤ 𝑏 rather than 𝑎 ⇒ 𝑏 ≈ 1.

2.3. 𝒮-algebras as residuated lattices 33

Equations

The equation E(A1) easily follows from integrality. We have E(A2) from the fact

that 0 is the minimum element of A. From the definition of ¬ in 𝒮 ′ and from E(A1)

follows E(A3). We know that 1 := ¬0 therefore we have E(A4). As A is involutive, follows

E(A5). Remains to prove the equation E(Δ(𝜙, 𝜙)), see that we need to prove the follow-

ing identity (𝜑 ⇒ 𝜑) ∧ (𝜑 ⇒ 𝜑) ≈ 1, we already know that 𝜑 ⇒ 𝜑 ≈ 1, therefore also

(𝜑 ⇒ 𝜑) ∧ (𝜑 ⇒ 𝜑) ≈ 1.

In the next items, for each rule schema involving Γ the proof must be by induction

over the lenght of the finite list (𝜑1, . . . , 𝜑𝑛). From the monotonicty of * in the rules of

type Γ ⇒ 𝜑 we can take Γ = (𝛾) and from 3-potency in the rules of type Γ ⇒2 𝛾 we can

take Γ = (𝛾, 𝛾).

Quasiequations

Q(P) follows from the commutativity of * and from the identity (𝑎*𝑏) ⇒ 𝑐 ≈ 𝑎 ⇒ (𝑏 ⇒ 𝑐).

Q(C) follows from 3-potency: since 𝑎2 ≤ 𝑎3, we have that 𝑎3 ⇒ 𝑏 ≈ 1 implies 𝑎2 ⇒ 𝑏 ≈ 1.

Q(E) follows from the fact that A comprises a partial order ≤ that is determined by

the implication ⇒.

To prove Q(⇒ l), suppose 𝑎 ≤ 𝑏 and 𝑐 ≤ 𝑑. From 𝑐 ≤ 𝑑, as 𝑏 ⇒ 𝑐 ≤ 𝑏 ⇒ 𝑐,

using residuation we have that 𝑏 * (𝑏 ⇒ 𝑐) ≤ 𝑐 ≤ 𝑑, therefore 𝑏 * (𝑏 ⇒ 𝑐) ≤ 𝑑

and therefore 𝑏 ⇒ 𝑐 ≤ 𝑏 ⇒ 𝑑. Note that as 𝑎 ≤ 𝑏, using residuation we have that

𝑎 * (𝑏 ⇒ 𝑑) ≤ 𝑏 * (𝑏 ⇒ 𝑑) ≤ 𝑑, therefore 𝑏 ⇒ 𝑑 ≤ 𝑎 ⇒ 𝑑 and thus 𝑏 ⇒ 𝑐 ≤ 𝑎 ⇒ 𝑑. Now,

since 𝑏 ⇒ 𝑐 ≤ 𝑎 ⇒ 𝑑 iff 𝑎 * (𝑏 ⇒ 𝑐) ≤ 𝑑 iff 𝑎 ≤ (𝑏 ⇒ 𝑐) ⇒ 𝑑, we obtain the desired result.

For Q(⇒ r) we need to prove that if 𝑑 ≈ 1, then 𝑏 ⇒ 𝑑 ≈ 1. This follows immedi-

ately from integrality.

Quasiequations Q(∧l1), Q(∧l2), Q(∧r), Q(∨l1), Q(∨r1) and Q(∨r2) follow straight-


forwardly from the fact that A is partially ordered and the order is determined by the

implication.

To prove Q(∨l2), notice that (𝑏 ∨ 𝑐)2 ≤ 𝑏2 ∨ 𝑐2 by Lemma 1.4. Suppose 𝑏2 ≤ 𝑑 and

𝑐2 ≤ 𝑑, then since A is a lattice, we have 𝑏2 ∨ 𝑐2 ≤ 𝑑 and as (𝑏∨ 𝑐)2 ≤ 𝑏2 ∨ 𝑐2 we conclude

that (𝑏 ∨ 𝑐)2 ≤ 𝑑 and thus (𝑏 ∨ 𝑐)2 ⇒ 𝑑 ≈ 1.

As to Q(¬ ⇒ l), by integrality we have 𝑏 * 𝑐 ≤ 𝑏 and 𝑏 * 𝑐 ≤ 𝑐. Thus 𝑏 * 𝑐 ≤ 𝑏 ∧ 𝑐.

Now, if 𝑏 ∧ 𝑐 ≤ 𝑑, then 𝑏 * 𝑐 ≤ 𝑑.

To prove Q(¬ ⇒ r), suppose 𝑑2 ≤ 𝑏 ∧ 𝑐. Using monotonicity of *, we have 𝑑2 * 𝑑2 ≤

(𝑏∧𝑐)* (𝑏∧𝑐), i.e., 𝑑4 ≤ (𝑏∧𝑐)2. Using 3-potency, we have 𝑑4 ≈ 𝑑2, therefore 𝑑2 ≤ (𝑏∧𝑐)2.

Now, see that 𝑏∧𝑐 ≤ 𝑏 and 𝑏∧𝑐 ≤ 𝑐, using monotonicity of * we have (𝑏∧𝑐)*(𝑏∧𝑐) ≤ 𝑏*𝑐.

Since (𝑏 ∧ 𝑐)2 ≤ 𝑏 * 𝑐, we have 𝑑2 ≤ (𝑏 ∧ 𝑐)2 ≤ (𝑏 * 𝑐), i.e., 𝑑2 ≤ (𝑏 * 𝑐).

Q(¬ ∧ l), Q(¬ ∧ r), Q(¬ ∨ l) and Q(¬ ∨ l) follow from the De Morgan’s Laws

[Galatos et al., 2007, Lemma 3.17].

Finally, we have Q(¬¬l) and Q(¬¬r) from A being involutive.

Remain to prove the quasiequation E(Δ(𝜙, 𝜓)) implies 𝜙 ≈ 𝜓, that is, if ((𝜙 ⇒ 𝜓)∧ (𝜓 ⇒

𝜙)) ≈ 1, then 𝜙 ≈ 𝜓. As 1 is the maximum of the algebra, we have that (𝜙 ⇒ 𝜓) ≈ 1 and

(𝜓 ⇒ 𝜙) ≈ 1, therefore 𝜙 ≤ 𝜓 and 𝜓 ≤ 𝜙, as ≤ is an order relation, follows 𝜙 ≈ 𝜓.

From Propositions 2 and 3 above we obtain the desired result:

Theorem 2. The classes of 𝒮-algebras and of 𝒮 ′-algebras are term equivalent.1

An advantage of the presentation given in Definition 13 is that it makes it straight-

forward to check that, for instance, the three-element MV-algebra [Cignoli et al., 2000]

is a model of Nelson’s logic 𝒮. This in turn allows one to prove that the formulas which

Nelson claims not to be derivable in 𝒮 [Nelson, 1959, p. 213] are indeed not valid.

1 See [Spinks and Veroff, 2008a, p. 329] for a formal definition of term equivalence.

35

3 CalculusWe are now going to introduce a finite Hilbert-style calculus and prove that it is

algebraizable with respect to the class of 𝒮 ′-algebras (hence, w.r.t 𝒮-algebras). This will

give us a finite presentation of 𝒮 that is equivalent to Nelson’s calculus of Section 1.2, but

has the advantage of involving only a finite number of axiom schemata.

Our calculus is an axiomatic extension of the full Lambek calculus with exchange

and weakening (𝐹𝐿𝑒𝑤) of [Spinks and Veroff, 2008b], which will allow us to obtain alge-

braizability of 𝒮 as an easy extension of the corresponding result about 𝐹𝐿𝑒𝑤.

3.1 A finite Hilbert-style calculus for 𝒮 ′

Definition 14. The logic 𝒮 ′ = ⟨Fm,⊢𝒮′⟩ is the sentential logic in the language

⟨∧,∨,⇒, *,⊥,⊤⟩ of type ⟨2, 2, 2, 2, 0, 0⟩ defined by the Hilbert-style calculus with the

following axiom schemata and modus ponens (from 𝜑 and 𝜑 ⇒ 𝜓, infer 𝜓) as the only

rule:

(S1) (𝜙 ⇒ 𝜓) ⇒ ((𝜓 ⇒ 𝛾) ⇒ (𝜙 ⇒ 𝛾))

(S2) (𝜙 ⇒ (𝜓 ⇒ 𝛾)) ⇒ (𝜓 ⇒ (𝜙 ⇒ 𝛾))

(S3) 𝜙 ⇒ (𝜓 ⇒ 𝜙)

(S4) 𝜙 ⇒ (𝜓 ⇒ (𝜙 * 𝜓))

(S5) (𝜙 ⇒ (𝜓 ⇒ 𝛾)) ⇒ ((𝜙 * 𝜓) ⇒ 𝛾)

(S6) (𝜙 ∧ 𝜓) ⇒ 𝜙

(S7) (𝜙 ∧ 𝜓) ⇒ 𝜓

(S8) (𝜙 ⇒ 𝜓) ⇒ ((𝜙 ⇒ 𝛾) ⇒ (𝜙 ⇒ (𝜓 ∧ 𝛾)))

(S9) 𝜙 ⇒ (𝜙 ∨ 𝜓)

(S10) 𝜓 ⇒ (𝜙 ∨ 𝜓)

(S11) (𝜙 ⇒ 𝛾) ⇒ ((𝜓 ⇒ 𝛾) ⇒ ((𝜙 ∨ 𝜓) ⇒ 𝛾))

36 Chapter 3. Calculus

(S12) ⊤

(S13) ⊥ ⇒ 𝜙

(S14) ((𝜙 ⇒ ⊥) ⇒ ⊥) ⇒ 𝜙

(S15) (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))) ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))

Example 2. We can deduce from ⊢𝒮′ the following formula

(S1’) (𝜓 ⇒ 𝛾) ⇒ ((𝜙 ⇒ 𝜓) ⇒ (𝜙 ⇒ 𝛾))

1 (𝜙 ⇒ 𝜓) ⇒ ((𝜓 ⇒ 𝛾) ⇒ (𝜙 ⇒ 𝛾)) (S1)

2 (𝜙 ⇒ 𝜓) ⇒ ((𝜓 ⇒ 𝛾) ⇒ (𝜙 ⇒ 𝛾)) ⇒ (𝜓 ⇒ 𝛾) ⇒ ((𝜙 ⇒ 𝜓) ⇒ (𝜙 ⇒ 𝛾)) (S2)

3 (𝜓 ⇒ 𝛾) ⇒ ((𝜙 ⇒ 𝜓) ⇒ (𝜙 ⇒ 𝛾)) (MP)(1, 2)

Example 3. If ∅ ⊢𝒮′ 𝜙 then ∅ ⊢𝒮′ 𝜓 ⇒ 𝜙.

1 𝜙 hypothesis

2 𝜙 ⇒ (𝜓 ⇒ 𝜙) (S3)

3 (𝜓 ⇒ 𝜙) (MP)(1, 2)

Axioms from (S1) to (S13) are those that axiomatize 𝐹𝐿𝑒𝑤 as presented in

[Spinks and Veroff, 2008b, Section 5], where it is proven that 𝐹𝐿𝑒𝑤 is algebraizable. This

allows us to immediately obtain the following.

Theorem 3. The calculus 𝒮 ′ is algebraizable (with the same defining equation and equiv-

alence formulas as 𝒮) with respect to the class of 𝒮 ′-algebras.

Proof. We know from [Spinks and Veroff, 2008b, Lemma 5.2] that 𝐹𝐿𝑒𝑤 is algebraiz-

able with respect to the class of commutative integral bounded residuated lattices, see

[Spinks and Veroff, 2008b, Lemma 5.3]. 𝒮 ′ is an axiomatic extension of 𝐹𝐿𝑒𝑤, therefore,

by [Font, 2016, Proposition 3.31], it is also algebraizable with the same defining equation

and equivalence formulas. The corresponding class of algebras is a subvariety of 𝐶𝐼𝐵𝑅𝐿

that can be axiomatized by adding the equations corresponding to the new axioms. It

is easy to check that these equations imply precisely that the equivalent semantics of

𝒮 ′ is the class of all involutive (S14) and three-potent (S15) 𝐶𝐼𝐵𝑅𝐿, i.e., the class of

𝒮 ′-algebras.

3.2. Deduction theorem 37

Although the logics 𝒮 and 𝒮 ′ have been initially defined over different propositional

languages (namely ⟨∧,∨,⇒,¬,⊥⟩ for 𝒮 and ⟨∧,∨,⇒, *,⊥,⊤⟩ for 𝒮 ′), we can obviously

expand the language of 𝒮 to include the connectives ⊤ and * defined by ⊤ := ¬⊥ and

𝜑 * 𝜓 := ¬(𝜑 ⇒ ¬𝜓). This allows us to state the following.

Corollary 1. The calculi 𝒮 (in the above-defined extended language) and 𝒮 ′ define the

same logic.

Proof. The result follows straightforwardly from the fact that 𝒮 and 𝒮 ′ are algebraizable (

with the same defining equation and equivalence formulas) with respect to the same class

of algebras. To be more formal one can invoke the algorithm of [Font, 2016, Proposition

3.47] which allows one to obtain an axiomatization of an algebraizable logic from a pre-

sentation of the corresponding class 𝐾 that is the equivalent algebraic semantics; notice

that the algorithm uses only the (quasi)equations that axiomatize 𝐾 and the defining

equations and equivalence formulas witnessing algebraizability.

3.2 Deduction theorem

Working with Nelson’s original presentation of 𝒮, it can be hard to prove some

version of Deduction Metatheorem. Indeed, if we prove it using induction over the structure

of the derivation, we need to apply induction over each rule of system. The advantage of

𝒮 ′, then, is that it has only one rule.

Theorem 4. If Γ ∪ {𝜙} ⊢ 𝜓, then Γ ⊢ 𝜙 ⇒ (𝜙 ⇒ 𝜓).

Proof. We are going to prove it applying the principle of induction on the structure of

the proof of Γ ∪ {𝜙} ⊢ 𝜓.

Base case In this case, our derivation of 𝜓 from Γ ∪ {𝜙} is a sequence with a single

formula, therefore, this formula is 𝜓, so we have 3 cases:

𝜓 is an axiom: In this case, using the axiom (S3) from 𝒮 ′, we have 𝜓 ⇒ (𝜙 ⇒ 𝜓)

and as 𝜓 is axiom, by modus ponens we have 𝜙 ⇒ 𝜓. Now, using axiom (S3)

again, we have (𝜙 ⇒ 𝜓) ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓)) and as we have 𝜙 ⇒ 𝜓 it follows

that (𝜙 ⇒ (𝜙 ⇒ 𝜓)). Notice that we do not use any formula of Γ, therefore

Γ ⊢ 𝜙 ⇒ (𝜙 ⇒ 𝜓).


𝜓 ∈ Γ: This case is like the case above.

𝜓 ∈ {𝜙} : In this case, 𝜓 = 𝜙 and we need to prove 𝜓 ⇒ (𝜓 ⇒ 𝜓) and this is the

axiom (S3).

Inductive step Supposing the result is valid for any derivation sequence of 𝑘 ≤ 𝑛 steps

with 𝑛 > 1, we will prove that the result is valid for any derivation sequence with

𝑛 + 1 formulas. If 𝜓 ∈ Γ ∪ {𝜙} or 𝜓 is an axiom, the proof is as above in the

base case. Suppose then that 𝜓 can be proved from previous formulas in the se-

quence through an aplication of modus ponens, and so this previous formulas are

of type 𝜃 and 𝜃 ⇒ 𝜓, from the inductive hypothesis we have Γ ⊢ 𝜙 ⇒ (𝜙 ⇒ 𝜃)

and Γ ⊢ 𝜙 ⇒ (𝜙 ⇒ (𝜃 ⇒ 𝜓)), thus we have the following proof of Γ ⊢ 𝜙 ⇒ (𝜙 ⇒ 𝜓):

𝑖

𝑖𝑖

...

𝑘 𝜙 ⇒ (𝜙 ⇒ 𝜃) hypothesis...

𝑙 𝜙 ⇒ (𝜙 ⇒ (𝜃 ⇒ 𝜓)) hypothesis

1 (𝜙 ⇒ (𝜃 ⇒ 𝜓)) ⇒ (𝜃 ⇒ (𝜙 ⇒ 𝜓)) (S2)

2 ((𝜙 ⇒ (𝜃 ⇒ 𝜓)) ⇒ (𝜃 ⇒ (𝜙 ⇒ 𝜓))) ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜃 ⇒ 𝜓))) ⇒ (𝜙 ⇒ (𝜃 ⇒ (𝜙 ⇒ 𝜓))) (S1’)

3 (𝜙 ⇒ (𝜙 ⇒ (𝜃 ⇒ 𝜓))) ⇒ (𝜙 ⇒ (𝜃 ⇒ (𝜙 ⇒ 𝜓))) (MP)(1, 2)

4 𝜙 ⇒ (𝜃 ⇒ (𝜙 ⇒ 𝜓)) (MP)(1, 3)

5 (𝜙 ⇒ (𝜃 ⇒ (𝜙 ⇒ 𝜓))) ⇒ (𝜃 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))) (S2)

6 𝜃 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓)) (MP)(4, 5)

7 ((𝜃 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓)))) ⇒ ((𝜙 ⇒ 𝜃) ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))) (S1’)

8 ((𝜙 ⇒ 𝜃) ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))) (MP)(6, 7)

9 ((𝜙 ⇒ 𝜃) ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))) ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜃)) ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓)))) (S1’)

10 (𝜙 ⇒ (𝜙 ⇒ 𝜃)) ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓)))) (MP)(8, 9)

11 𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓))) (MP)(𝑘, 10)

12 𝜙 ⇒ (𝜙 ⇒ (𝜙 ⇒ 𝜓)) (S15)

13 𝜙 ⇒ (𝜙 ⇒ 𝜓) (S15)

Theorem 4 suggests that, defining 𝜙 → 𝜓 := 𝜙2 ⇒ 𝜓, one may obtain in 𝒮 a new

implication-type connective → that enjoys the classical Deduction-Detachment Theorem.

This is precisely what happens in Nelson’s logic 𝒩 3, where in fact → is usually taken as

the primitive implication and ⇒ as a defined one (see Subsection 5.2). Whether a similar

inter-definability may hold for 𝒮 as well is actually an interesting open question, which

we shall discuss in chapter 7. For now what we can say is that the above-defined term →

does indeed behave as an implication operator on 𝒮-algebras, at least in the sense that


it is an example of a weak relative pseudo complementation according to the terminology

introduced by Blok, Köhler and Pigozzi [Blok et al., 1984].

This last paper is the second of a series devoted to varieties of algebras of non-

classical logics, focusing in particular those varieties that enjoy a property called equa-

tionally definable principal congruences or EDPC for short [Blok et al., 1984, p. 338]. It

is well known that a logic that is algebraizable with respect to some variety of algebras

enjoys a (generalized) Deduction-Detachment Theorem1 if and only its associated variety

has EDPC [Font, 2016, Corollary 3.86]. This applies, in particular, to our logic 𝒮 and to

𝒮-algebras.

In the context of varieties of non-classical logic having EDPC, the authors of

[Blok et al., 1984] single out those that possess term-definable operations which can be

viewed as generalizations of intuitionistic conjunction, implication and bi-implication.

These operations are called, respectively, weak meet, weak relative pseudo complementation

and Gödel equivalence. Algebras having them are called weak Brouwerian semilattices with

filter preserving operations or WBSO for short [Blok et al., 1984, Definition 2.1].

Definition 15. Let A be an algebra of type F and Θ an equivalence relation. Then Θ is

congruence on A if it satisfies the following property:

For each 𝜆 ∈ F and 𝑎𝑖, 𝑏𝑖 ∈ A. If 𝑎𝑖Θ𝑏𝑖 then 𝜆(𝑎1, · · · , 𝑎𝑛)Θ𝜆(𝑏1, · · · , 𝑏𝑛)

In the next definiton 𝐶𝑝A denote the lattice of congruences on A which are finitely

generated.

Definition 16. A binary operation ⊕ is called dual relative pseudo complementation if

for every Θ ∈ 𝐶𝑝A, it holds the condition:

Φ ⊕ Ψ ⊆ Θ iff Ψ ⊆ Φ ∨ Θ

In the next definition, Θ(𝑎, 𝑏) denotes the principal congruence generated by the pair 𝑎, 𝑏.

Definition 17. Let A an arbitrary algebra and 1 ∈ 𝐴. Each following term is defined

with respect to 1 and it is called:

1 See e.g. [Font, 2016, Definition 3.76] for a precise definition of generalized Deduction-DetachmentTheorem.


· Weak meet if for all 𝑎, 𝑏 ∈ 𝐴

Θ(𝑎 · 𝑏, 1) = Θ(𝑎, 1) ∨ Θ(𝑏, 1)

→ Weak relative pseudo complementation if ⟨𝐶𝑝A,∨, 𝐼⟩ is dually relatively pseudo com-

plemented and

Θ(𝑎 → 𝑏, 1) = Θ(𝑎, 1) ⊕ Θ(𝑏, 1)

∇ Gödel equivalence if for all 𝑎, 𝑏 ∈ 𝐴

Θ(𝑎, 𝑏) = Θ(𝑎∇𝑏, 1)

In the next definition we shall adopt → instead 𝛼(𝑥, 𝑦) to not overload notation,

but keeping in mind that → is just a notation, → can be any binary term having the

properties in definition below. The same case applies to the other binary terms.

Definition 18. V is a variety of weak Brouwerian semilattices with filter preserving

operations (WBSO) if there exist binary terms →, · and ∇ and a constant 1 such that

the followings identities and quasi-identities hold in V.

1. 𝑥 → 𝑥 = 1

2. 𝑥 → 1 = 1

3. (𝑥 → 𝑦) → ((𝑦 → 𝑧) → (𝑥 → 𝑧)) = 1

4. 1 · 1 = 1

5. (𝑧 → 𝑥) → ((𝑧 → 𝑦) → (𝑧 → (𝑥 · 𝑦))) = 1

6. (𝑥 · 𝑦) → 𝑥 = 1, (𝑥 · 𝑦) → 𝑦 = 1

7. 𝑥∇𝑥 = 1

8. (𝑥∇1) → 𝑥 = 1, 𝑥 → (𝑥∇1) = 1

9. (𝑥∇𝑦) → (𝑦∇𝑥) = 1

10. ((𝑥∇𝑦) · (𝑦∇𝑧)) → (𝑥∇𝑧) = 1


11. For every fundamental operation 𝜆 of V,

(· · · ((𝑥0∇𝑦0) · (𝑥1∇𝑦1)) · · · ) · (𝑥𝑚−1∇𝑦𝑚−1) → 𝜆(𝑥0, · · · , 𝑥𝑚−1)∇𝜆(𝑦0, · · · , 𝑦𝑚−1)

12. 1 → 𝑥 = 1 implies 𝑥 = 1

13. 𝑥∇𝑦 = 1 implies 𝑥 = 𝑦.

In order to relate the latest two definition above, see that [Blok et al., 1984, Lemma

2.7] shows the following lemma:

Lemma 2. V is a WBSO variety iff it has terms →, ·, ∇ such that → is a weak relative

pseudo complement, · is a weak meet, and ∇ is a Gödel equivalence term, all with respect

to 1.

As observed in [Blok et al., 1984, p. 358], the algebraic counterpart of Nelson’s

logic 𝒩 3 is a WBSO variety. The same is true for 𝒮-algebras.

Theorem 5. 𝒮-algebras are a WBSO variety in which a weak meet is given by ∧ (or,

equivalently, by *), weak relative pseudo complementation is given by the term 𝑥2 ⇒ 𝑦

and Gödel equivalence is 𝑥 ⇔ 𝑦.

Proof. Items 1., 2. and 8. follow from Example 3 for being 𝛼2 ⇒ 𝛼 and 𝛼2 ⇒ 1 theorems.

Items 4. and 6. follow from lattice properties.

3. We must prove that (𝑥2 ⇒ 𝑦)2 ⇒ ((𝑦2 ⇒ 𝑧)2 ⇒ (𝑥2 ⇒ 𝑧) = 1, from deduction theorem,

it equations holds iff 𝑥2 ⇒ 𝑦 ⊢𝒮 ((𝑦2 ⇒ 𝑧)2 ⇒ (𝑥2 ⇒ 𝑧) iff {𝑥2 ⇒ 𝑦, 𝑦2 ⇒ 𝑧} ⊢𝒮 𝑥2 ⇒ 𝑧

iff {𝑥2 ⇒ 𝑦, 𝑦2 ⇒ 𝑧, 𝑥} ⊢𝒮 𝑧 and the last deduction follows from modus ponens.

5. In order to prove (𝑧2 ⇒ 𝑥)2 ⇒ ((𝑧2 ⇒ 𝑦)2 ⇒ (𝑧2 ⇒ 𝑥 ∧ 𝑦)) = 1, we use deduction

theorem, 𝑧2 ⇒ 𝑥 ⊢𝒮 ((𝑧2 ⇒ 𝑦)2 ⇒ (𝑧2 ⇒ 𝑥 ∧ 𝑦)) iff {𝑧2 ⇒ 𝑥, 𝑧2 ⇒ 𝑦} ⊢𝒮 𝑧2 ⇒ 𝑥 ∧ 𝑦 iff

{𝑧2 ⇒ 𝑥, 𝑧2 ⇒ 𝑦, 𝑧} ⊢𝒮 𝑥 ∧ 𝑦. The last deduction follows from modus ponens.

7. We know that the partial order is determined by ⇒ and as 𝑥 ≤ 𝑥, follows the equation.

9. It follows from commutativity of ∧ and ⇔.

10. See that ((𝑥 ⇔ 𝑦) ∧ (𝑦 ⇔ 𝑧))2 ⇒ (𝑥 ⇔ 𝑧) = 1 iff (𝑥 ⇔ 𝑦) ∧ (𝑦 ⇔ 𝑧) ⊢𝒮′ (𝑥 ⇔ 𝑧). The

last deduction follows from (S3).

11. See Theorem 1, this item is just the case IL3.

12. It follows from the fact that 1 is the maximum of the lattice.

13. Finishing, it follows from Proposition 1.2.


We have proved it for ∧, the proof for * is in a similar way, observe that

𝑥 * 𝑦 ⇒ 𝑥 ∧ 𝑦 = 1, therefore we can use it with the rule {𝑥 ⇒ 𝑦, 𝑦 ⇒ 𝑧} ⊢𝒮 𝑥 ⇒ 𝑧

for proving the theorem to *.

Finishing the chapter, we remind that as happens with weak meet, weak relative

pseudo complementationd and Gödel equivalence need not be unique. For example, one

can prove that choosing 𝑥2 * 𝑦 as weak meet, (𝑥2 ⇒ (𝑥2 * 𝑦))2 as weak relative pseudo

complementation and (𝑥 ⇔ 𝑦)2 as Gödel equivalence, they satisfy the Definition 18.

43

4 More on 𝒮-algebrasIn this chapter we are going to show some examples of 𝒮-algebras that will allow

us to prove that the formulas which Nelson claims without proof not to be derivable in

𝒮 [Nelson, 1959, p. 213] are actually not valid. To this end, an advantage of the presenta-

tion of Definition 13 is that it makes it easier to check that, for instance, the three-element

MV-chain presented below (and indeed every algebra in the variety it generates), is a

model of 𝒮

4.1 ℒ3 algebra

The three-element linearly ordered MV-algebra [Cignoli et al., 2000, Definition

1.1.1], that we shall call Ł3 (for Łukasiewicz three-valued logic), is defined as follows.

The universe is {0, 12 , 1} in the language {∧,∨, *,⇒,¬, 0, 1}, the operations are given by:

⇒ 0 12 1

0 1 1 112

12 1 1

1 0 12 1

* 0 12 1

0 0 0 012 0 0 1

2

1 0 12 1

¬

0 112

12

1 0

It is well-known that Ł3 is an involutive CIBRL (see, e.g., [Cignoli et al., 2000,

Lemma 1.1.4 and Proposition 1.1.5]). It is also easy to check that Ł3 is three-potent,

therefore it is an 𝒮-algebra. We can thus use it as a counter-model to show that the

formulas below are not 𝒮-theorems.

Proposition 4. The following formulas are not true in ℒ3 with designated set 𝒟 = {1},

consequently not true in 𝒮-algebras and thus can not be proved in the logic 𝒮.

1. 𝑝 ∨ ¬𝑝

2. ¬(𝑝 ∧ ¬𝑝)

3. (𝑝 ∧ ¬𝑝) ⇒ 𝑞

4. (𝑝 ⇒ (𝑝 ⇒ 𝑞)) ⇒ (𝑝 ⇒ 𝑞)

5. (𝑝 ⇒ (𝑞 ⇒ 𝑟)) ⇒ ((𝑝 ∧ 𝑞) ⇒ 𝑟)

44 Chapter 4. More on 𝒮-algebras

6. (𝑝 ∧ ¬𝑞) ⇒ ¬(𝑝 ⇒ 𝑞)

Proof. It is sufficient to find, for each formula 𝜑 above, a valuation 𝜐 : Fm −→ Ł3 such

that 𝜐(𝜑) ̸= 1. The result will then follow by our completeness result (Theorem 3).

1. Letting 𝜐(𝑝) = 12 , we have 𝜐(𝑝 ∨ ¬𝑝) = 𝜐(𝑝) ∨ ¬𝜐(𝑝) = 1

2 ∨ ¬12 = 1

2 ∨ 12 = 1

2 .

2. Letting 𝜐(𝑝) = 12 , we have 𝜐(¬(𝑝 ∧ ¬𝑝)) = ¬(𝜐(𝑝) ∧ ¬𝜐(𝑝)) = ¬(1

2 ∧ ¬12) = ¬(1

2 ∧ 12) =

¬12 = 1

2 .

3. Let 𝜐(𝑝) = 12 and 𝜐(𝑞) = 0. Then 𝜐(𝑝 ⇒ 𝑞) = 𝜐(𝑝) ⇒ 𝜐(𝑞) =1

2 ⇒ 0 = 12 .

4. Let 𝜐(𝑝) = 12 and 𝜐(𝑞) = 0. Then 𝜐((𝑝 ⇒ (𝑝 ⇒ 𝑞)) ⇒ (𝑝 ⇒ 𝑞)) = (𝜐(𝑝) ⇒ (𝜐(𝑝) ⇒

𝜐(𝑞)) ⇒ (𝜐(𝑝) ⇒ 𝜐(𝑞)) = (12 ⇒ (1

2 ⇒ 0)) ⇒ (12 ⇒ 0) = (1

2 ⇒ 12) ⇒ 1

2 = (1 ⇒ 12) = 1

2 .

5. Let 𝜐(𝑝) = 𝜐(𝑞) = 12 and 𝜐(𝑟) = 0, then 𝜐((𝑝 ⇒ (𝑞 ⇒ 𝑟)) ⇒ ((𝑝 ∧ 𝑞) ⇒ 𝑟)) = (1

2 ⇒

(12 ⇒ 0)) ⇒ ((1

2 ∧ 12) ⇒ 0) = (1

2 ⇒ (12 ⇒ 0)) ⇒ (1

2 ⇒ 0) = (12 ⇒ 1

2) ⇒ 12 = 1 ⇒ 1

2 = 12 .

6. Let 𝜐(𝑝) = 𝜐(𝑞) = 12 , then 𝜐((𝑝 ∧ ¬𝑞) ⇒ ¬(𝑝 ⇒ 𝑞)) = (𝜐(𝑝) ∧ ¬𝜐(𝑞)) ⇒ ¬(𝜐(𝑝) ⇒

𝜐(𝑞)) = (12 ∧ ¬1

2) ⇒ ¬(12 ⇒ 1

2) = 12 ⇒ ¬1 = 1

2 ⇒ 0 = 12 .

4.2 Making 𝒮-algebras

We now present an adaptation of the construction introduced in

[Galatos and Raftery, 2004, Section 6] to embed a CIRL into one having an involutive

negation. This will give us a simple way to construct 𝒮-algebras.

Definition 19. Given a CIRL A = ⟨𝐴,∧,∨, *,⇒, 1⟩, let 𝐴′ = {𝑎′ : 𝑎 ∈ 𝐴} be a disjoint

copy of 𝐴, and let 𝐴* = 𝐴∪𝐴′. We extend the lattice order of A to 𝐴* as follows. For all

𝑎, 𝑏 ∈ 𝐴:

1. 𝑎 ≤𝐴* 𝑏 iff 𝑎 ≤𝐴 𝑏.

2. 𝑎′ ≤𝐴* 𝑏.

4.2. Making 𝒮-algebras 45

3. 𝑎′ ≤𝐴* 𝑏′ iff 𝑏 ≤𝐴 𝑎.

For each 𝑥 ∈ 𝐴 ∪ 𝐴′, we define (𝑎′)′ = 𝑎. The behavior of the lattice operations is fixed

according to De Morgan’s laws: 𝑎′ ∧ 𝑏′ := (𝑎 ∨ 𝑏)′ and 𝑎′ ∨ 𝑏′ := (𝑎 ∧ 𝑏)′. The operations *

and ⇒ are extended to 𝐴* as follows para todo a b in A:

𝑎 * 𝑏′ := (𝑎 ⇒ 𝑏)′ 𝑎′ * 𝑏′ := 1′.

𝑎 ⇒ 𝑏′ := (𝑎 * 𝑏)′ 𝑎′ ⇒ 𝑏′ := 𝑏 ⇒ 𝑎 𝑎′ ⇒ 𝑏 := 1.

It is shown in [Galatos and Raftery, 2004, Section 6] that, if A is a CIRL, then

A* is an involutive CIBRL into which A is embedded in the obvious way. Moreover, we

have the following.

Proposition 5. A* is an 𝒮-algebra if and only if A is a three-potent CIRL.

Proof. One direction is immediate: if A* is an 𝒮-algebra, then it is three-potent, hence so

is A as a {∧,∨, *,⇒, 1}-subalgebra of A*. Conversely, if A is a three-potent CIRL, since

we already know that A* is CIBRL, it remains to show that 𝑎2 ≤ 𝑎3 for all 𝑎 ∈ A*. For

𝑎 ∈ 𝐴 the result follows from 3-potency of A. If 𝑎 ∈ 𝐴′, then by Definition 19 we have

𝑎2 = 1′ = 𝑎3.

Corollary 2. If A is an implicative lattice or an 𝒮-algebra, then A* is an 𝒮-algebra.

In fact, it is not difficult to check that if A is an implicative lattice, then A*

is a special 𝒮-algebra known as an 𝒩 3-lattice (we shall deal with these structures in

Section 5.2).

Example 4. The above construction is useful to produce examples of 𝒮-algebras that

witness the failure of further formulas that are not valid in 𝒮. For example, the algebra

(Ł3)*, where Ł3 is the above-introduced MV-algebra, witnesses the failure of

((𝑝 ⇒ 𝑞) ⇒ 𝑞) ⇒ ((𝑞 ⇒ 𝑝) ⇒ 𝑝) (4.1)

which is however valid in three-valued Łukasiewicz logic. The behaviour of implication in

(Ł3)* is shown in the table below.

To show that the above-mentioned formula is not valid, let 𝜐 : Fm −→ (Ł3)* be a

valuation such that 𝜐(𝑝) = 0 and 𝜐(𝑞) = 0′. We have 𝜐(((𝑝 ⇒ 𝑞) ⇒ 𝑞) ⇒ ((𝑞 ⇒ 𝑝) ⇒

46 Chapter 4. More on 𝒮-algebras

⇒ 1′ 12

′ 0′ 0 12 1

1′ 1 1 1 1 1 112

′ 12 1 1 1 1 1

0′ 0 12 1 1 1 1

0 0′ 0′ 0′ 1 1 112

12

′ 0′ 0′ 12 1 1

1 1′ 12

′ 0′ 0 12 1

𝑝))) = (𝜐(𝑝) ⇒ 𝜐(𝑞)) ⇒ 𝜐(𝑞)) ⇒ ((𝜐(𝑞) ⇒ 𝜐(𝑝)) ⇒ 𝜐(𝑝)) = ((0 ⇒ 0′) ⇒ 0′) ⇒ ((0′ ⇒

0) ⇒ 0) = (0′ ⇒ 0′) ⇒ (1 ⇒ 0) = 1 ⇒ 0 = 0.

Together with our previous considerations about Ł3, the preceding example entails

that Łukasiewicz three-valued logic is a proper extension of 𝒮: in fact it is easy to check

that it is precisely the axiomatic extension of 𝒮 obtained by adding the axiom schema

corresponding to (4.1) above. On the other hand, no other logic in the Łukasiewicz family

is comparable with 𝒮, because they all lack 3-potency, whereas 𝒮 does not satisfy (4.1)

which is valid in all of them.

47

5 Relation with 𝒩 3 and 𝒩 4As mentioned earlier, David Nelson is remembered for having introduced, besides

𝒮, two better-known logics: 𝒩 3, which is usually called just Nelson logic [Nelson, 1949],

and 𝒩 4 which is known as paraconsistent Nelson logic [Almukdad and Nelson, 1984].

Both logics are algebraizable with respect to classes of residuated structures (called, re-

spectively, 𝒩 3-lattices, or Nelson algebras, and 𝒩 4-lattices). The question then arises of

what is precisely the relation between 𝒮 and these other logics, or equivalently between

𝒮-algebras and 𝒩 3 and 𝒩 4-lattices).

Can we meaningfully say that one is stronger than the other? By looking at their

algebraic models, it will not be difficult to show that 𝒩 3 (which is known to be an

axiomatic extension of 𝒩 4) can also be viewed as an axiomatic extension of 𝒮, while 𝒩 4

and 𝒮 do not seem to be comparable in any meaningful way.

5.1 𝒩 4

Definition 20. 𝒩 4 = ⟨Fm,⊢𝒩 4⟩ is the sentential logic in the language ⟨∧,∨,→,¬⟩ of

type ⟨2, 2, 2, 1⟩ defined by the Hilbert-style calculus with the following axiom schemata

and modus ponens (from 𝜑 and 𝜑 → 𝜓, infer 𝜓) as the only rule schema.

(N1) 𝜑 → (𝜓 → 𝜑)

(N2) (𝜑 → (𝜓 → 𝛾)) → ((𝜑 → 𝜓) → (𝜑 → 𝛾))

(N3) (𝜑 ∧ 𝜓) → 𝜑

(N4) (𝜑 ∧ 𝜓) → 𝜓

(N5) (𝜑 → 𝜓) → ((𝜑 → 𝛾) → (𝜑 → (𝜓 ∧ 𝛾)))

(N6) 𝜑 → (𝜑 ∨ 𝜓)

(N7) 𝜓 → (𝜑 ∨ 𝜓)

(N8) (𝜑 → 𝛾) → ((𝜓 → 𝛾) → ((𝜑 ∨ 𝜓) → 𝛾))

(N9) ¬¬𝜑 ↔ 𝜑

48 Chapter 5. Relation with 𝒩 3 and 𝒩 4

(N10) ¬(𝜑 ∨ 𝜓) ↔ (¬𝜑 ∧ ¬𝜓)

(N11) ¬(𝜑 ∧ 𝜓) ↔ (¬𝜑 ∨ ¬𝜓)

(N12) ¬(𝜑 → 𝜓) ↔ (𝜑 ∧ ¬𝜓)

Here 𝜑 ↔ 𝜓 abbreviates (𝜑 → 𝜓) ∧ (𝜓 → 𝜑). The implication → in 𝒩 4 is usually called

weak implication, in contrast to the strong implication ⇒ that is defined by the following

term:

𝜑 ⇒ 𝜓 := (𝜑 → 𝜓) ∧ (¬𝜓 → ¬𝜑).

Example 5. We can deduce from ⊢𝒩 4 the following formula 𝜑 → 𝜑.

Example 6. We can deduce from ⊢𝒩 4 the following formula (𝜓 → 𝜓) → (𝜑 → 𝜑).

As the notation suggests, it is the strong implication and not the weak that we

shall compare with the implication of 𝒮. This appears indeed to be the more meaningful

choice, as we shall explain below.

A prominent feature of the weak implication of 𝒩 4 is that on the one hand (unlike

the implication of 𝒮) it enjoys the Deduction-Detachment Theorem in its classical form:

Γ ∪ {𝜙} ⊢𝒩 4 𝜓 if and only if Γ ⊢𝒩 4 𝜙 → 𝜓. On the other hand contraposition fails (𝜙 →

𝜓 ̸⊢𝒩 4 ¬𝜓 → ¬𝜙) which entails that the above-defined bi-implication does not satisfy the

following congruence property (again unlike 𝒮, as mentioned just before our Example 1):

⊢𝒩 4 𝜙 ↔ 𝜓 does not imply ⊢𝒩 4 ¬𝜙 ↔ ¬𝜓. By contrast, the strong implication of 𝒩 4

does not have the Deduction-Detachment Theorem but satisfies contraposition (like the

implication of 𝒮), and the associated bi-implication (𝜑 ⇒ 𝜓) ∧ (𝜓 ⇒ 𝜑) does enjoy the

congruence property. These considerations apply to the logic 𝒩 3 considered in the next

subsection.

It is well known [Rivieccio, 2011, Theorem 2.6] that 𝒩 4 is algebraizable (though

not implicative) with defining equation E(𝜑) := {𝜑 ≈ 𝜑 → 𝜑} and equivalence formulas

Δ(𝜑, 𝜓) := {𝜑 ⇒ 𝜓, 𝜓 ⇒ 𝜑}. The implication in E(𝜑) could as well be taken to be the

strong one, so E(𝜑) := {𝜑 ≈ 𝜑 ⇒ 𝜑} would work too. By contrast, letting Δ(𝜑, 𝜓) :=

{𝜑 → 𝜓, 𝜓 → 𝜑} or the equivalent Δ(𝜑, 𝜓) := {𝜑 ↔ 𝜓} would not work precisely because

of the failure of the above-mentioned congruence property.

5.1. 𝒩 4 49

The equivalent algebraic semantics of 𝒩 4 is the class of 𝒩 4-lattices defined below

[Odintsov, 2008, Definition 8.4.1].

Definition 21. An algebra A = ⟨𝐴,∨,∧,→,¬⟩ is an 𝒩 4-lattice if it satisfies the following

properties:

1. ⟨𝐴,∨,∧,¬⟩ is a De Morgan lattice.

2. The relation ⪯ defined, for all 𝑎, 𝑏 ∈ 𝐴, by 𝑎 ⪯ 𝑏 iff (𝑎 → 𝑏) → (𝑎 → 𝑏) = (𝑎 → 𝑏)

is a pre-order on A.

3. The relation ≡ defined, for all 𝑎, 𝑏 ∈ 𝐴 as 𝑎 ≡ 𝑏 iff 𝑎 ⪯ 𝑏 and 𝑏 ⪯ 𝑎 is a congruence

relation with respect to ∧,∨,→ and the quotient-algebra A◁▷ := ⟨𝐴,∨,∧,→⟩/≡ is

an implicative lattice.

4. For any 𝑎, 𝑏 ∈ 𝐴, ¬(𝑎 → 𝑏) ≡ 𝑎 ∧ ¬𝑏.

5. For any 𝑎, 𝑏 ∈ 𝐴, 𝑎 ≤ 𝑏 iff 𝑎 ⪯ 𝑏 and ¬𝑏 ⪯ ¬𝑎, where ≤ is a lattice order of A.

Example 7. A most simple example of an 𝒩 4-lattice is the four-element one A4 whose

lattice reduct is the four-element diamond De Morgan algebra.

1

𝑛 𝑏

0

The table of A4 is given by:

→ 0 n b 1

0 1 1 1 1

n 1 1 1 1

b 0 n b 1

1 0 n b 1

¬

0 1

n n

b b

1 1

One can check that A4 satisfies all properties of Definition 21 (the quotient A4/≡

mentioned in Definition 21.3 being the two-element Boolean algebra).


Although 𝒩 4 to deduce (𝜓 → 𝜓) → (𝜑 → 𝜑), we cannot deduce (𝜓 ⇒ 𝜓) ⇒

(𝜑 ⇒ 𝜑) or even (𝜓 → 𝜓) ⇒ (𝜑 → 𝜑), it because 𝒩 4 don’t hold 𝜑 ⇒ (𝜓 ⇒ 𝜑). The set

of equivalence formulas in 𝒩 4 is given by {𝜑 ⇒ 𝜓, 𝜓 ⇒ 𝜑}, therefore 𝒩 4-lattices do not

satisfy the equation 𝑥 ⇒ 𝑥 ≈ 𝑦 ⇒ 𝑦, which holds in all 𝒮-algebras. As example, in A4

we have 𝑏 ⇒ 𝑏 = 𝑏 while 0 ⇒ 0 = 1. Furthermore, it is not difficult to check that there

no constant term is definable in A4. In fact, since the singleton {𝑏} is a subalgebra of

A4, this element would be the only possible interpretation for an algebraic constant. But

{0, 1} is also a subalgebra of A4, so this cannot be the case either. This implies that A4

has no term-definable as 𝒮-algebra structure, as well as that no constant term exists in

the whole class of 𝒩 4-lattices.

In order to compare 𝒩 4 and 𝒮 we must fix a common propositional language, an

obvious choice being ⟨∧,∨,→,¬⟩ which is the primitive language of 𝒩 4 as introduced

above. That is, we interpret the implication of 𝒮 (up to now denoted ⇒) as the weak

implication → of 𝒩 4. Under this interpretation, it is easy to check that for instance the

𝒩 4 axiom (N12) is not derivable in 𝒮 (Proposition 4.6). On the other hand, it is well

known that the weak implication of 𝒩 4 does not satisfy the contraposition axiom (A5)

of our Definition 7: (𝜑 → 𝜓) ↔ (¬𝜓 → ¬𝜑). Thus we must conclude that, over this

language, 𝒩 4 and 𝒮 are incomparable.

As mentioned earlier, another possible choice for a common language would be

⟨∧,∨,⇒,¬⟩, interpreting the implication of 𝒮 as the strong implication ⇒ of 𝒩 4. This

is also a sensible option, for it has been recently shown that the whole logic 𝒩 4 can be

equivalently presented in this language: that is, the weak implication is term-definable in

the ⟨∧,∨,⇒,¬⟩-fragment of 𝒩 4.

Under the latter interpretation, the above-mentioned contraposition axiom turns

out to be valid in both logics. However, the fact that the equation 𝑥 ⇒ 𝑥 ≈ 𝑦 ⇒ 𝑦

does not hold in all 𝒩 4-lattices implies (via algebraizability of 𝒩 4) that the formula

(𝜓 ⇒ 𝜓) ⇒ (𝜙 ⇒ 𝜙), which can be proven in 𝒮, is not derivable in 𝒩 4. On the other

hand, the Distributivity axiom (see Subsection 5.2) is valid in 𝒩 4 but not in 𝒮 because

the lattice reduct of 𝒮-algebras need not be distributive. All the above arguments con-

tinue to hold also if we consider conservative expansions of 𝒩 4 such as the logic 𝒩 4⊥

of [Odintsov, 2008].

5.1. 𝒩 4 51

Example 8. The following algebra A8 is a non-distributive 𝒮-algebra.

1

𝑎

𝑐 𝑏

¬𝑏 ¬𝑐

¬𝑎

0

𝑐 ∧ (¬𝑐 ∨ ¬𝑏) = 𝑐 ∧ 𝑎 = 𝑐

(𝑐 ∧ ¬𝑐) ∨ (𝑐 ∧ ¬𝑏) = ¬𝑎 ∨ ¬𝑏 = ¬𝑏

Table of A8.

→ 0 1 𝑐 ¬𝑐 ¬𝑏 𝑏 𝑎 ¬𝑎

0 1 1 1 1 1 1 1 1

1 0 1 𝑐 ¬𝑐 ¬𝑏 𝑏 𝑎 ¬𝑎

𝑐 ¬𝑐 1 1 𝑏 𝑎 𝑏 1 𝑏

¬𝑐 𝑐 1 𝑐 1 𝑐 1 1 𝑐

¬𝑏 𝑏 1 1 𝑏 1 𝑏 1 𝑏

𝑏 ¬𝑏 1 𝑐 𝑎 𝑐 1 1 𝑐

𝑎 ¬𝑎 1 𝑐 𝑏 𝑐 𝑏 1 ¬𝑎

¬𝑎 𝑎 1 1 1 1 1 1 1

* 0 1 𝑐 ¬𝑐 ¬𝑏 𝑏 𝑎 ¬𝑎

0 0 0 0 0 0 0 0 0

1 0 1 𝑐 ¬𝑐 ¬𝑏 𝑏 𝑎 ¬𝑎

𝑐 0 𝑐 ¬𝑏 0 ¬𝑏 ¬𝑎 ¬𝑏 0

¬𝑐 0 ¬𝑐 0 ¬𝑐 0 ¬𝑐 ¬𝑐 0

¬𝑏 0 ¬𝑏 ¬𝑏 0 ¬𝑏 0 ¬𝑏 0

𝑏 0 𝑏 ¬𝑎 ¬𝑐 0 ¬𝑐 ¬𝑐 0

𝑎 0 𝑎 ¬𝑏 ¬𝑐 ¬𝑏 ¬𝑐 𝑎 0

¬𝑎 0 ¬𝑎 0 0 0 0 0 0

Joining these observations, we have the following.

Proposition 6. 𝒩 4 (or any of its conservative expansions) and 𝒮 are incomparable over

either language ⟨∧,∨,→,¬⟩ or ⟨∧,∨,⇒,¬⟩.

In the next section we are going to see that at least in the case of the logic 𝒩 3 the

second choice of language allows us to show that the two logics are indeed comparable,

our 𝒮 being the weaker.


5.2 𝒩 3

Definition 22. Nelson’s logic 𝒩 3 = ⟨Fm,⊢𝒩 3⟩ is the axiomatic extension of 𝒩 4 obtained

by adding the following axiom:

(N13) ¬𝜑 → (𝜑 → 𝜓).

As an axiomatic extension of 𝒩 4, Nelson logic 𝒩 3 is also algebraizable with the

same defining equations and equivalence formulas. 𝒩 3 is in fact implicative, and its equiv-

alent algebraic semantics is the variety of 𝒩 3-lattices, which are just 𝒩 4-lattices satisfying

the equation corresponding to the above axiom (¬𝑥 → (𝑥 → 𝑦) ≈ 𝑥 → 𝑥) or, equivalently,

the equation 𝑥 → 𝑥 ≈ 𝑦 → 𝑦. The latter implies that each non-empty 𝒩 3-lattice has two

algebraic constants given by 1 := 𝑥 → 𝑥 and 0 := ¬1.

In his 1959 paper [Nelson, 1959, p. 215], Nelson mentioned that a calculus for 𝒩 3

(there denoted by 𝑁) could be obtained from his calculus for 𝒮 by removing certain rules

and adding others, thus leaving unclear whether one logic could be viewed as an extension

of the other. At this point our algebraizability result for 𝒮 gives us a way to settle this

issue.

As in the preceding subsection, we may compare 𝒮 and 𝒩 3 over the language

⟨∧,∨,→,¬, 0, 1⟩ or ⟨∧,∨,⇒,¬, 0, 1⟩, this time including the propositional constants which

are term-definable in both logics. The first option yields no new results, for the above

arguments hold for the case of 𝒩 3 too. Thus, 𝒮 and 𝒩 3 are also incomparable over

⟨∧,∨,→,¬, 0, 1⟩. The second one gives us the following.

Proposition 7. 𝒩 3 is a (proper) extension of 𝒮 over the language ⟨∧,∨,⇒,¬, 0, 1⟩.

Proof. It follows from [Spinks and Veroff, 2008a, Theorem 3.12] that (the ⟨∧,∨, *,⇒

,¬, 0, 1⟩-reduct of) every 𝒩 3-lattice satisfies all properties of our Definition 13, and thus

is an 𝒮-algebra. On the other hand, 𝒩 3-lattices (like 𝒩 4-lattices) are distributive, while

𝒮-algebras need not be. Thus, invoking once more algebraizability of 𝒩 3 and of 𝒮, we

have that 𝒩 3 is a proper extension of 𝒮.

Proposition 8. 𝒩 3 is an axiomatic extension of 𝒮 obtained by adding the following two

axioms:

5.2. 𝒩 3 53

(𝜑 ∧ (𝜓 ∨ 𝛾)) ⇒ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝛾)) (Distributivity)((𝜑2 ⇒ 𝜓) ∧ ((¬𝜓)2 ⇒ ¬𝜑)) ⇒ (𝜑 ⇒ 𝜓) (Nelson).

Proof. According [Spinks and Veroff, 2008a, p. 326], 𝒩 3 is definitionally equivalent to the

axiomatic extension of 𝐹𝐿𝑒𝑤 by adding the following four axioms:

¬¬𝜑 ⇒ 𝜑 (Double-negation)(𝜑 ∧ (𝜓 ∨ 𝛾)) ⇒ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝛾)) (Distributivity)𝜑3 ⇒ 𝜑2 (3-Potency)((𝜑2 ⇒ 𝜓) ∧ ((¬𝜓)2 ⇒ ¬𝜑)) ⇒ (𝜑 ⇒ 𝜓) (Nelson)

From Chapter 3 we know that 𝒮 is an axiomatic extension of 𝐹𝐿𝑒𝑤 satisfying

3-potency and double-negation, therefore we just need to add Distributivity and Nelson’s

axiom.

One can, in fact, do even better, showing that an 𝒮-algebra satisfying the equa-

tion corresponding to the axiom dubbed (Nelson) must satisfy (Distributivity) as well

[Busaniche and Cignoli, 2010, Remark 3.7]. Thus we obtain the following.

Proposition 9. 𝒩 3 over the language ⟨∧,∨,⇒,¬, 0, 1⟩ is the axiomatic extension of 𝒮

with the Nelson axiom.

Example 9. It is not difficult to verify that (Distributivity) does not imply (Nelson).

This can be checked in the six-element chain (Ł3)* of our Example 4. This algebra is

obviously distributive, but the equations given from Nelson axiom fails because we have

(((0′)2 ⇒ 12

′) ∧ ((1

2′′)2 ⇒ 0′′)) ⇒ (0′ ⇒ 1

2′) =

((1′ ⇒ 12

′) ∧ (0 ⇒ 0)) ⇒ 1

2 =

(1 ∧ 1) ⇒ 12 = 1

2

Thus, if we add the Distributivity axiom to 𝒮, we obtain a distinct logic that is

intermediate between 𝒮 and 𝒩 3. On the other hand, it is easy to show that the weakest

logic extending both 𝒮 and 𝒩 4 is 𝒩 3 itself. In other words, 𝒩 3 is the join of 𝒮 and 𝒩 4

in the lattice of all extensions of 𝒮.

Proposition 10. 𝒩 3 = 𝒮 ∨ 𝒩 4.

Proof. It is well known that an 𝒩 4-lattice satisfying the equation 𝑥 ⇒ 𝑥 ≈ 𝑦 ⇒ 𝑦

(integrality) must be an 𝒩 3-lattice.


With respect to the relation between 𝒮-algebras and 𝒩 3-lattices, we can employ

the construction introduced in Definition 19 to state an analogue of Proposition 5.

Proposition 11. Let A* be an 𝒮-algebra constructed according to Definition 19. Then,

1. A* is an 𝒩 3-lattice if and only if A is an implicative lattice.

2. A* is an MV-algebra if and only if and only if A is trivial (hence, if and only if A*

is the two-element Boolean algebra).

Proof. 1. Assume A is an implicative lattice, and let us check that the Nelson equation

((𝑥2 ⇒ 𝑦) ∧ ((𝑦′)2 ⇒ 𝑥′)) ⇒ (𝑥 ⇒ 𝑦) ≈ 1 holds in A*. Let 𝑎, 𝑏 ∈ 𝐴. Clearly, the only

non-trivial cases are when either 𝑎 or 𝑏 or both appear negated in the equation. Using

the fact that 𝑎2 = 𝑎 and 𝑏2 = 𝑏, we have ((𝑎2 ⇒ 𝑏′) ∧ ((𝑏′′)2 ⇒ 𝑎′)) ⇒ (𝑎 ⇒ 𝑏′) = ((𝑎 ⇒

𝑏′) ∧ (𝑏 ⇒ 𝑎′)) ⇒ (𝑎 ⇒ 𝑏′) = 1. Similarly, (((𝑎′)2 ⇒ 𝑏) ∧ ((𝑏′)2 ⇒ 𝑎′′)) ⇒ (𝑎′ ⇒ 𝑏) =

(((𝑎′)2 ⇒ 𝑏) ∧ ((𝑏′)2 ⇒ 𝑎′)) ⇒ 1 = 1. Lastly, (((𝑎′)2 ⇒ 𝑏′) ∧ ((𝑏′′)2 ⇒ 𝑎′′)) ⇒ (𝑎′ ⇒ 𝑏′) =

(((𝑎′)2 ⇒ 𝑏′) ∧ (𝑏2 ⇒ 𝑎)) ⇒ (𝑏 ⇒ 𝑎) = (((𝑎′)2 ⇒ 𝑏′) ∧ (𝑏 ⇒ 𝑎)) ⇒ (𝑏 ⇒ 𝑎) = 1.

Conversely, assume A* is an 𝒩 3-lattice. Then, for all 𝑎 ∈ 𝐴, we can show that 𝑎 ⇒ 𝑎2 = 1

by instancing the Nelson equation as follows: ((𝑎2 ⇒ 𝑎2)∧(((𝑎2)′)2 ⇒ 𝑎′)) ⇒ (𝑎 ⇒ 𝑎2) = 1.

Since 𝑏2 = 1′ for all 𝑏 ∈ 𝐴′, the left-hand side gives us ((𝑎2 ⇒ 𝑎2) ∧ (((𝑎2)′)2 ⇒ 𝑎′)) ⇒

(𝑎 ⇒ 𝑎2) = (1 ∧ (1′ ⇒ 𝑎′)) ⇒ (𝑎 ⇒ 𝑎2) = 1 ⇒ (𝑎 ⇒ 𝑎2) = 𝑎 ⇒ 𝑎2 which implies the

desired result. Thus 𝑎 = 𝑎2, which implies that A is an implicative lattice.

2. Assume A* is an MV-algebra. Then A* satisfies the so-called divisibility equation

𝑥 * (𝑥 ⇒ 𝑦) = 𝑥 ∧ 𝑦 [Cignoli et al., 2000, Proposition 1.1.5]. Now let 𝑎 ∈ 𝐴, so that

𝑎′ <𝐴* 𝑎. We have 𝑎′ = 𝑎 ∧ 𝑎′ = 𝑎 * (𝑎 ⇒ 𝑎′) = 𝑎 * (𝑎 * 𝑎)′. But 𝑎 * 𝑎′ = 1′ and so, by

monotonicity, 𝑎 * (𝑎 * 𝑎)′ = 1′. Thus, 𝑎′ = 1′, which implies that 𝐴 = {1}.

The preceding proposition, besides characterizing the algebras of the form A* that

happen to be 𝒩 3-lattices, illustrates the fact that A* turns out to be an MV-algebra (or

Heyting, or Boolean algebra) only in the degenerate case.

The following information on 𝒮-algebras is also obtained as a straightforward con-

sequence of the previous results.

Proposition 12. The variety of 𝒮-algebras is not finitely generated.

5.2. 𝒩 3 55

Proof. Suppose, by contradiction, that the variety of 𝒮-algebras was 𝑉 (𝐾) with 𝐾 a

finite set of finite algebras. Since 𝒮-algebras are congruence-distributive (this follows

from [Burris and Sankappanavar, 1981, Theorem II.12.3] and also from our Theorem 5),

we could apply Jónsson’s lemma [Burris and Sankappanavar, 1981, Corollary IV.6.10] to

conclude that the subdirectly irreducible algebras of 𝑉 (𝐾) are in 𝐻𝑆(𝐾). Thus, there

would be only finitely many subdirectly irreducible 𝒮-algebras. However, it is well known

that there are infinitely many subdirectly irreducible 𝒩 3-lattices (see, e.g., [Odintsov, 2008,

Corollary 9.2.11]), and thus there are infinitely many subdirectly irreducible 𝒮-algebras.

57

6 ConclusionIn order to simplify the logic 𝒮 introduced by Nelson we studied it using the

modern tools of algebraic logic, proved that 𝒮 is algebraizable and therefore we were able

to use well-known results about algebraizable logics. In fact, we did better, we showed

that 𝒮 is implicative. Having these results in hand, we established the first semantics for

𝒮 and simplified it showing the 𝒮-algebras form a variety. Other simplification that we did

concern a Hilbert calculus for 𝒮. Nelson’s original system has finite axioms and infinite

rules, our simplification has finite axioms and only a rule, modus ponens.

Studying what is the relation of 𝒮 with the other well-known Nelson’s logics, we

put 𝒮 inside a theory which already was well studied, like we did showing that 𝒮-algebras

are residuated lattices.

Now that 𝒮 has a finite Hilbert calculus presentation and a variety as semantics, to

answer questions about it is easier. These results open many questions about the variety

that we have introduced, some of these questions being discussed in the next chapter.

59

7 Future workWe have studied 𝒮 in two directions, through a proof-theoretic approach and

through algebraic methods. Concerning the proof-theoretic approach, we gave a Hilbert

calculus for 𝒮. An interesting question that still remains is about other types of calculi. In

this sense we are interested in a sequent calculus for 𝒮 enjoying a cut-elimination theorem

that could be used it to answer wheter 𝒮 is decidable and enjoys the Craig interpolation

theorem.

As observed in Chapter 3, if we define 𝜑 → 𝜓 := 𝜑 ⇒ (𝜑 ⇒ 𝜓), the weak

implication → enjoys a version of deduction theorem. For 𝒩 3-lattices and 𝒩 4-lattices

it is possible to take the strong implication ⇒ as primitive and from it define the weak

implication →, being this result for 𝒩 4 hard to prove1. We can repeat the same question

for 𝒮-algebras. It is possible to axiomatize 𝒮-algebras taking the weak implication as

primitive?

Continuing our algebraic related questions, we can ask ourselves if it is possible

give a semantics for 𝒮 using twist-structures like it is possible to give such a semantics

for 𝒩 3, z [Odintsov, 2008, Definition 8.3.1]. As 𝒩 3 is stronger than 𝒮, we can start our

search by weakening the definition of twist-structure.

1 𝜑 → 𝜓 := (𝜑 ∧ (((𝜑 ∧ (𝜓 ⇒ 𝜓)) ⇒ 𝜓) ⇒ ((𝜑 ∧ (𝜓 ⇒ 𝜓)) ⇒ 𝜓))) ⇒ ((𝜑 ⇒ (𝜓 ⇒ 𝜓)) ⇒ 𝜓).

61

Bibliography

[Abe et al., 2015] Abe, J. M., Akama, S., and Nakamatsu, K. (2015). Introduction to

Annotated Logics. Intelligent Systems Reference Library. Springer. Foundations for

Paracomplete and Paraconsistent Reasoning. Cited on page 17.

[Almukdad and Nelson, 1984] Almukdad, A. and Nelson, D. (1984). Constructible falsity

and inexact predicates. The Journal of Symbolic Logic, 49(1):231–233. Cited 2 times

on pages 17 and 47.

[Blok et al., 1984] Blok, W. J., Köhler, P., and Pigozzi, D. (1984). On the structure

of varieties with equationally definable principal congruences II. Algebra Universalis,

18:334–379. Cited 2 times on pages 39 and 41.

[Blok and Pigozzi, 1989] Blok, W. J. and Pigozzi, D. (1989). Algebraizable Logics, volume

396 of Mem. Amer. Math. Soc. A.M.S., Providence. Cited 6 times on pages 17, 18,

23, 25, 26, and 28.

[Burris and Sankappanavar, 1981] Burris, S. and Sankappanavar, H. (1981). A Course

in Universal Algebra. Springer. Cited on page 55.

[Busaniche and Cignoli, 2010] Busaniche, M. and Cignoli, R. (2010). Constructive logic

with strong negation as a substructural logic. Journal of Logic and Computation,

20(4):761–793. Cited on page 53.

[Cignoli et al., 2000] Cignoli, R., D’Ottaviano, I. M. L., and Mundici, D. (2000). Algebraic

Foundations of Many-Valued Reasoning, volume 7 of Trends in Logic—Studia Logica

Library. Kluwer Academic Publishers, Dordrecht. Cited 3 times on pages 34, 43,

and 54.

[Font, 2016] Font, J. M. (2016). Abstract Algebraic Logic. An Introductory Textbook. Col-

lege Publications. Cited 6 times on pages 25, 27, 29, 36, 37, and 39.

[Galatos et al., 2007] Galatos, N., Jipsen, P., Kowalski, T., and Ono, H. (2007). Resid-

uated Lattices: an algebraic glimpse at substructural logics, volume 151 of Studies in

62 Bibliography

Logic and the Foundations of Mathematics. Elsevier, Amsterdam. Cited 3 times on

pages 31, 32, and 34.

[Galatos and Raftery, 2004] Galatos, N. and Raftery, J. G. (2004). Adding involution to

residuated structures. Studia Logica, 77(2):181–207. Cited 3 times on pages 31, 44,

and 45.

[Kleene, 1945] Kleene, S. C. (1945). On the interpretation of intuitionistic number theory.

The Journal of Symbolic Logic, 10:109–124. Cited on page 17.

[Nelson, 1949] Nelson, D. (1949). Constructible falsity. The Journal of Symbolic Logic,

14:16–26. Cited 2 times on pages 17 and 47.

[Nelson, 1959] Nelson, D. (1959). Negation and separation of concepts in constructive

systems. Studies in Logic and the Foundations of Mathematics, 39:205–225. Cited 7

times on pages 17, 18, 19, 21, 34, 43, and 52.

[Odintsov, 2008] Odintsov, S. P. (2008). Constructive Negations and Paraconsistency.

Springer. Cited 5 times on pages 17, 49, 50, 55, and 59.

[Ono, 2010] Ono, H. (2010). Logics without the contraction rule and residuated lattices.

The Australasian Journal of Logic, 8:50–81. Cited on page 31.

[Restall, 1993] Restall, G. (1993). How to be Really contraction free. Studia Logica,

52:381–391. Cited on page 23.

[Rivieccio, 2011] Rivieccio, U. (2011). Paraconsistent modal logics. Electronic Notes in

Theoretical Computer Science, 278:173–186. Cited on page 48.

[Spinks and Veroff, 2008a] Spinks, M. and Veroff, R. (2008a). Constructive logic with

strong negation is a substructural logic. i. Studia Logica, 88:325–348. Cited 3 times

on pages 34, 52, and 53.

[Spinks and Veroff, 2008b] Spinks, M. and Veroff, R. (2008b). Constructive logic with

strong negation is a substructural logic. II. Studia Logica, 89(3):401–425. Cited 3

times on pages 18, 35, and 36.

63

Index

𝐴*, 42

𝐹𝐿𝑒𝑤, 33

𝒮, 18

𝒮 ′, 33

A4, 47

A8, 49

𝒮-algebra, 26

𝒮 ′-algebra, 29

𝒩 3, 50

𝒩 3-lattices, 50

𝒩 4, 45

𝒩 4-lattices, 47

L-algebra of formulas, 17

Ł3, 41

3-2 contraction, 21

3-potency, 21

3-potent, 29

Alg*ℒ, 24

algebraizable, 24

algebraizable logic, 24

commutative integral bounded residuated

lattice (CIBRL), 29

congruence, 37

contraction, 21

Deduction Metatheorem, 35

defining equations, 25

Distributivity, 51

dual relative pseudo complementation, 37

equationally definable principal congru-

ences, 37

equations, 18

equivalence formulas, 25

evaluation, 17

full Lambek calculus with exchange and

weakening, 33

Gödel equivalence, 38

implicative lattice, 43

implicative logic, 23

involutive, 29

language, 17

logic, 18

modus ponens, 21

Nelson algebras, 45

Nelson logic, 45

Nelson’s Axiom, 51

non-distributive 𝒮-algebra, 49

paraconsistent Nelson logic, 45

strong implication, 46

substitution, 18

weak Brouwerian semilattices with filter

preserving operations (WBSO), 38

weak condensation, 21

weak implication, 46

Weak meet, 37

64 Index

Weak relative pseudo complementation,

38

weak relative pseudo complementation, 37

repositorio.ufrn.br · Catalogação da Publicação na Fonte. UFRN / SISBI / Biblioteca Setorial...

Documents

Transcript of repositorio.ufrn.br · Catalogação da Publicação na Fonte. UFRN / SISBI / Biblioteca Setorial...