Lindenbaum Method

TL;DR

The paper explores Adolf Lindenbaum's contributions to algebraic logic, focusing on Lindenbaum matrices and Tarski algebras, and demonstrates how his method influenced the development of model theory and algebraization of logic.

Contribution

It provides a detailed tutorial on Lindenbaum's concepts, emphasizing their role in algebraic logic and the ongoing development of the field.

Findings

Lindenbaum's method shaped the algebraization of logic.

Lindenbaum-Tarski algebra facilitates algebraic understanding of logic.

The tutorial introduces unexplored directions in algebraic logic.

Abstract

During his brief life, the Polish mathematician and logician Adolf Lindenbaum (1904--1941) contributed to mathematical logic, among other things, by several significant achievements. Some results of Lindenbaum's, which bear his name, were published without proofs by other people from the Lvov--Warsaw School and the proofs later were provided by some others, though the authorship of Lindenbaum has never been challenged. Many may have heard about Lindenbaum's lemma, asserting the existence of Lindenbaum's extension, and Lindenbaum-Tarski algebra; less known is Lindenbaum's logical matrix. This tutorial is devoted to the two last concepts rather than the first one. However, the latter can be understood in a purely algebraic fashion, if one employs the notion of Lindenbaum-Tarski algebra. In general, the notions of Lindenbaum matrix and Lindenbaum-Tarski algebra have paved a way to further algebraization of logic, which had been begun by George Boole in the 19th century, as well as to a new branch of logic, model theory. For this reason, the present tutorial is also a gentle introduction to algebraic logic. A uniting idea of the aforementioned concepts is a special view on the formal judgments of a formal language. It is this view we call the Lindenbaum method. Although Lindenbaum expressed merely a starting viewpoint in the tradition of Polish logic of the time, this viewpoint became a standard ever since and its development goes on until this day, continuing to shape the field of algebraic logic. Our main objective is to demonstrate how this view gave rise to formulating the aforementioned concepts and how it opens door to unexplored paths.

Equations

$$\begin{array}[]{cl}1^{\circ}&\emptyset\in\mathcal{O}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\ X\in\mathcal{O};\\ \\ 2^{\circ}&\text{for any $U_{1},\ldots,U_{n}\in\mathcal{O}$, $U_{1}\cap\ldots\cap U_{n}\in\mathcal{O}$};\\ \\ 3^{\circ}&\text{for any $\{U_{i}\}_{i\in I}\subseteq\mathcal{O}$, $\bigcup\{U_{i}\}_{i\in I}\in\mathcal{O}$}.\end{array}$$

$$\text{P}:=\prod _{i\in I}{X}_i.$$

$${\text{B}}_0:=\{{\rho }_i^{-1}(U)\text{leavevmode}|\text{leavevmode}U\in {\mathcal{O}}_i\text{leavevmode}\text{and}\text{leavevmode}i\in I\}.$$

$${\rho }_{i_1}^{-1}(U_{i_1})\cap \dots \cap {\rho }_{i_k}^{-1}(U_{i_k}),$$

$$\prod _{i\in I}{Z}_i,$$

$$\begin{array}[]{cll}(\text{l}_{1})&i)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge y=y\wedge x,&ii)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\vee y=y\vee x,\\ (\text{l}_{2})&i)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge(y\wedge z)=(x\wedge y)\wedge z,&ii)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\vee(y\vee z)=(x\vee y)\vee z,\\ (\text{l}_{3})&i)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (x\wedge y)\vee y=y,&ii)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge(x\vee y)=x,\\ (\text{l}_{4})&i)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge(y\vee z)=(x\wedge y)\vee(x\wedge z),&ii)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\vee(y\wedge z)=(x\vee y)\wedge(x\vee z).\\ \end{array}$$

$$x\wedge x=x\text{leavevmode}\text{leavevmode}\text{and}\text{leavevmode}\text{leavevmode}x\vee x=x$$

$$\begin{array}[]{rl}x\!\!\!&=x\wedge(x\vee y)\\ &=(x\wedge x)\vee(x\wedge y)\quad[\mbox{according to ($\text{l}_{4}$--$i$)}]\\ &=((x\wedge y)\vee x)\wedge((x\wedge y)\vee x)\quad[\mbox{in virtue of ($\text{l}_{1}$--$ii$) and ($\text{l}_{4}$--$ii$)}]\\ &=x\wedge x.\quad[\mbox{according to ($\text{l}_{3}$--$i$)}]\end{array}$$

$$x\wedge y=x\text{leavevmode}⟺\text{leavevmode}x\vee y=y.$$

$$x\le y\stackrel{\text{df}}{⟺}x\wedge y=x.$$

$$x\le y\text{leavevmode}⟺\text{leavevmode}x\vee y=y.$$

$$\begin{array}[]{cll}(\text{b}_{1})&i)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge\mathbf{1}=x,&ii)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\vee\mathbf{1}=\mathbf{1},\\ (\text{b}_{2})&i)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (x\wedge\neg x)\vee y=y,&ii)\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (x\vee\neg x)\wedge y=y.\\ \end{array}$$

$$x=(1\wedge \neg 1)\vee x=\neg 1\vee x.$$

$$0:=\neg 1,$$

$$\neg \neg x=x.$$

$$1=x\vee \neg x\text{leavevmode}\text{leavevmode}\text{and}\text{leavevmode}\text{leavevmode}0=x\wedge \neg x,$$

$$\text{ctdiagram}\text{ctnohead}\text{ctinnermid}\text{ctel}0,0,0,20:\text{ctv}0,0:\bullet \text{ctv}0,20:\bullet \text{ctv}0,27:1\text{ctv}0,-9:0$$

$$x=\underset{i=1}{\overset{m}{\bigvee }}\underset{j=1}{\overset{n_i}{\bigwedge }}{b}_{ij},$$

$$x=\underset{i=1}{\overset{m}{\bigwedge }}\underset{j=1}{\overset{n_i}{\bigvee }}{b}_{ij},$$

$$\begin{array}[]{cc}(\text{h}_{1})&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge(x\rightarrow y)=x\wedge y,\\ (\text{h}_{2})&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (x\rightarrow y)\wedge y=y,\\ (\text{h}_{3})&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (x\rightarrow y)\wedge(x\rightarrow z)=x\rightarrow(y\wedge z),\\ (\text{h}_{4})&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ x\wedge(y\rightarrow y)=x,\\ (\text{h}_{5})&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \neg\mathbf{1}\vee y=y,\\ (\text{h}_{6})&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \neg x=x\rightarrow\neg\mathbf{1}.\\ \end{array}$$

$$x\leftrightarrow y:=(x\to y)\wedge (y\to x).$$

$$x\to x=1.$$

$$\neg x=x\to 0.$$

$$x\wedge \neg x=0.$$

$$x\le y\to z\text{leavevmode}⟺\text{leavevmode}x\wedge y\le z.$$

$$x\wedge y\le y\wedge (y\to z)=y\wedge z\le z.$$

$$\begin{array}[]{rl}x\leq y\rightarrow x\!\!\!&=(y\rightarrow x)\wedge(y\rightarrow y)=y\rightarrow(x\wedge y)=y\rightarrow(x\wedge y\wedge z)\\ &=(y\rightarrow(x\wedge y))\wedge(y\rightarrow z)\leq y\rightarrow z.\end{array}$$

$$x\le y\text{leavevmode}⟺\text{leavevmode}x\to y=1;$$

$$x=y\text{leavevmode}⟺\text{leavevmode}x\leftrightarrow y=1.$$

$$(x\vee \neg x)\wedge y=(x\to x)\wedge y=y.$$

Full text

1. 1 Preliminaries

2. 1.1 Preliminaries from topology

3. 1.2 Preliminaries from algebra

4. 1.2.1 Distributive lattices and Boolean algebras

5. 1.2.2 Heyting algebras

6. 2 Formal Languages

7. 2.1 Formal languages

8. 2.2 Semantics of formal language

9. 2.2.1 The logic of a two-valued matrix

10. 2.2.2 The Łukasiewicz logic of a three-valued matrix

11. 2.2.3 The Łukasiewicz modal logic of a three-valued matrix

12. 2.2.4 The Gödel $n$-valued logics

13. 2.2.5 The Dummett denumerable matrix

14. 2.2.6 Two infinite generalizations of Łukasiewicz’ $\textsf{{\L}}_{3}$

15. 2.3 Historical notes

16. 3 Logical Consequence

17. 3.1 Consequence relation

18. 3.2 Consequence operator

19. 3.3 Defining consequence relation

20. 3.3.1 Consequence operator (relation) via a closure system

21. 3.3.2 Consequence relation via logical matrices

22. 3.3.3 Consequence relation via inference rules

23. 3.4 Abstract logics defined by modus rules

24. 3.4.1 General characterization

25. 3.4.2 The class of $\mathcal{S}$-models

26. 3.4.3 Modus rules vs. non-finitary rules

27. 3.5 Extensions of abstract logics

28. 4 Matrix Consequence

29. 4.1 Single-matrix consequence

30. 4.2 Finitary matrix consequence

31. 4.3 The conception of separating means

32. 5 Unital Logics

33. 5.1 Unital algebraic expansions

34. 5.2 Unital abstract logics

35. 5.2.1 Definition and some properties

36. 5.2.2 Some subclasses of unital logics

37. 5.3 Lindenbaum-Tarski algebra

38. 5.3.1 Definition and properties

39. 5.3.2 Implicational unital logics

40. 5.3.3 Examples of Lindenbaum-Tarski algebras

Chapter 1 Preliminaries

1.1 Preliminaries from topology

Classic books [Kel75] and [Bou98] are main references in this section.

A topological space (or simply space) is a pair $(X,\mathcal{O})$ (perhaps both $X$ and $\mathcal{O}$ with subscripts), where $\mathcal{O}\subseteq\mathcal{P}(X)$ and such that

[TABLE]

In a topological space $(X,\mathcal{O})$, $X$ is called the carrier of the space and $\mathcal{O}$ is the topology of the space. The elements of $\mathcal{O}$ are called the open sets of the space. The complement of an open set is called closed. The topology $\mathcal{O}$ is called discrete if $\mathcal{O}=\mathcal{P}(X)$. In our applications, we will be assuming that $X\neq\emptyset$. If $X$ is a finite set, any space $(X,\mathcal{O})$ is called finite.

It is customary to apply the term space (or topological space) to $X$, meaning that $X$ is endowed with a family $\mathcal{O}$ of subsets of $X$ satisfying the conditions $1^{\circ}$–$3^{\circ}$. It must be clear that $X$ can be endowed with different families of open sets. Slightly abusing notation, we write $X=(X,\mathcal{O})$.

A family $\{U_{i}\}_{i\in I}\subseteq\mathcal{O}$ is called an open cover of a space $X=(X,\mathcal{O})$ if $\bigcup\{U_{i}\}_{i\in I}=X$. Any subfamily $\{U_{i}\}_{i\in I_{0}}$ with $I_{0}\subseteq I$ is called a subcover of the cover $\{U_{i}\}_{i\in I}$ if $\bigcup\{U_{i}\}_{i\in I_{0}}=X$. A subcover is called finite if $I_{0}$ is a nonempty finite set.

A topological space is called compact if each open cover has a finite subcover.

The following observation is obvious.

Proposition 1.1.1**.**

Any finite discrete topological space is compact.

Let $X$ be a nonempty set. Suppose we have a family $\text{B}_{0}:=\{Y_{i}\}_{i\in I}\subseteq\mathcal{P}(X)$. Assume that we want to define a topology $\mathcal{O}$ on $X$ such that sets $Y_{i}$ are open in $X$ endowed with this topology.

First we form all intersections $Y_{i_{1}}\cap\ldots\cap Y_{i_{n}}$ collecting them in a set B. Then, we define all unions $\bigcup_{j\in J}\{Z_{j}\leavevmode\nobreak\ |\leavevmode\nobreak\ Z_{j}\in\text{B}\}$ collecting them in a set $\mathcal{O}$, to which we add $\emptyset$ and $X$ (if they are not yet there). The sets of the resulting set $\mathcal{O}$ we announce open and define the space $X:=(X,\mathcal{O})$. It is not difficult to check that the conditions $1^{\circ}$–$3^{\circ}$ are satisfied. The family $\text{B}_{0}$ is called a subbase of the space $X$, and the set B is a base of $X$. It is obvious that all sets of the subbase $\text{B}_{0}$ are open in $X$.

Now we employ this way of introducing topology on a set to define the cartesian product of topological spaces. Assume that we have a collection $\{X_{i}\}_{i\in I}$ of topological spaces $X_{i}:=(X_{i},\mathcal{O}_{i})$, where $i\in I$. First, we define the cartesian product of the sets $X_{i}$; that is

[TABLE]

An arbitrary element x of P will be denoted by $(x_{i})_{i\in I}$; that is $\textbf{x}:=(x_{i})_{i\in I}$. Given an $i\in I$, a projection $\rho_{i}:\text{P}\longrightarrow X_{i}$ is defined by the mapping $\rho_{i}:\textbf{x}\mapsto x_{i}$. Now we define:

[TABLE]

Finally, $\text{B}_{0}$ is employed as a subbase to define a product topology (aka Tychonoff topology) on P. Denoting the product topology on P by $\mathcal{O}$, we call the topological space $(\text{P},\mathcal{O})$ a cartesian product of the collection $\{(X_{i},\mathcal{O}_{i})\}_{i\in I}$.

From the definition of the product topology, we see that its base B constituted by the sets of the form

[TABLE]

where $U_{i_{1}}\in\mathcal{O}_{i_{1}},\ldots,U_{i_{k}}\in\mathcal{O}_{i_{k}}$. This means that the sets of this base can be represented as follows:

[TABLE]

where either $Z_{i}\in\mathcal{O}_{i}$, if $i\in I_{0}$, for some $I_{0}\Subset I$, or $Z_{i}=X_{i}$, if $i\notin I_{0}$. If each $X_{i}$ in the cartesian product P is a finite discrete space, then in each representation (1.1) either $Z_{i}\subseteq X_{i}$, whenever $i\in I_{0}$, for some finite subset $I_{0}$ of $I$, or $Z_{i}=X_{i}$.

In our application of cartesian product (Section 4.2) the following proposition is essential.

Proposition 1.1.2** (Tychonoff theorem).**

The cartesian product of a collection of compact topological spaces is compact relative to the product topology.

Corollary 1.1.2.1**.**

The cartesian product of a collection of discrete spaces is compact relative to the product topology.

1.2 Preliminaries from algebra

1.2.1 Distributive lattices and Boolean algebras

Boolean algebras belong to to the class of distributive lattices.

An algebra $\textsf{{L}}=\langle\textsf{L};\wedge,\vee\rangle$ of type $\langle\wedge,\vee\rangle$, where $\wedge$ (meet) and $\vee$ (join) are binary operations, is called a distributive lattice if the identities following equalities hold in L for arbirary elements $x$, $y$ and $z$ of L:

[TABLE]

In any distributive lattice the following identities hold:

[TABLE]

Indeed, for any $x,y\in\textsf{L}$,

[TABLE]

The second idempotent law can be proven in a similar fashion.

We observe that if L is a distributive lattice, then for any $x,y\in\textsf{L}$,

[TABLE]

Indeed, assume that $x\wedge y=x$. Then we have: $x\vee y=(x\wedge y)\vee y=y$.

On the other hand, if $x\vee y=y$, then $x\wedge y=x\wedge(x\vee y)=x$.

The last equivalence induces the following definition. Given a distributive lattice L, we define a binary relation on L as follows:

[TABLE]

According to the last equivalence, we have:

[TABLE]

We also notice that $\leq$ is a partial ordering on L and, according to this ordering, $x\wedge y$ is the greatest lower bound and $x\vee y$ is the least upper bound of $\{x,y\}$, respectively. This, in particular, implies that the operations $\wedge$ and $\vee$ are monotone w.r.t. $\leq$. Namely,

$x\leq y$ implies $x\wedge z\leq y\wedge z$ and $x\vee z\leq y\vee z$.

A Boolean algebra is an algebra $\textsf{{B}}=\langle\textsf{B};\wedge,\vee,\neg,\mathbf{1}\rangle$ of type $\langle\wedge,\vee,\neg,\mathbf{1}\rangle$, where $\wedge$ (meet) and $\vee$ (join) are binary operations, $\neg$ (complementation) is a unary operation and $\mathbf{1}$ (unit) is a 0-ary operation, if the equalities $(\text{l}_{1})$–$(\text{l}_{4})$ above and $(\text{b}_{1})$–$(\text{b}_{2})$ below are satisfied in B for arbitrary elements $x$, $y$ and $z$ of B:

[TABLE]

If we apply the definition (1.1) for B, we realize that $\mathbf{1}$ is the greatest element and $\neg\mathbf{1}$ the least element in B, respectively. Indeed, the former comes from ($\text{b}_{1}$–$i$) and the latter, with the help of ($\text{b}_{2}$–$i$) and ($\text{b}_{1}$–$i$), can be obtained as follows:

[TABLE]

Denoting

[TABLE]

we observe that for any $x\in\textsf{B}$, $\neg x$ is a unique element $y$ such that $x\wedge y=\mathbf{0}$ and $x\vee y=\mathbf{1}$. The element $\neg x$ is called a complement of $x$. Thus any Boolean algebra is a distributive lattice with a greatest element $\mathbf{1}$, a least element $\mathbf{0}$ and a complementation $\neg x$. This implies that, the view of commutativity of $\wedge$ and $\vee$ (the equalities $(\text{l}_{1})$), we can say the $x$ is the complement of $\neg x$, which immediately implies the equality

[TABLE]

We also observe that

[TABLE]

for an arbitrary element $x\in\textsf{B}$.

It is obvious that a Boolean algebra is non-degenerate if, and only if, $\mathbf{0}\neq\mathbf{1}$. This implies that the simplest non-degenerate Boolean algebras consists of two elements — $\mathbf{1}$ and $\mathbf{0}$. Usually, this algebra is depicted by the following diagram.

Proposition 1.2.1**.**

Let a Boolean algebra B be generated by a nonempty finite set $\textsf{B}_{0}$. Then any element $x\in\textsf{B}$ can be represented in the form:

[TABLE]

or in the form:

[TABLE]

where for any $i$ and $j$ either $b_{ij}\in\textsf{B}_{0}$ or $\neg b_{ij}\in\textsf{B}_{0}$.

Proof.

To prove this proposition, it suffices to notice that all elements of $\textsf{B}_{0}$ can be represented in both forms. Then, one shows that all elements represented in the disjunctive normal form constitute a subalgebra of B; and the same is true for the elements represented in the conjunctive normal form; see [RS70], theorem II.2.1, for detail. ∎

As we will see below (Proposition 1.2.2), the class of Boolean algebras can be regarded as a subclass of a larger class of Heyting algebras which are discussed in the next subsection. Therefore, many properties related to Heyting algebras are applicable to Boolean algebras. For example, the properties that are discussed below in Proposition 1.2.3 for Heyting algebras (Section 1.2.2) can be applied to Boolean algebras as well.

1.2.2 Heyting algebras

A Heyting algebra is an algebra $\textsf{{H}}=\langle\textsf{H};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle$ of type $\langle\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle$, where $\wedge$ (meet) and $\vee$ (join), $\rightarrow$ (relative pseudo-complementation) are binary operations, $\neg$ (pseudo-complementation) is a unary operation and $\mathbf{1}$ (unit) is a 0-ary operation, if, besides the equalities ($\text{l}_{1}$)–($\text{l}_{2}$) and ($\text{b}_{1}$) (Section 1.2.1), the following equalities are satisfied for arbitrary elements $x$, $y$, $z$ of H:

[TABLE]

It is customary to denote:

[TABLE]

As in the case of Boolean algebras, in Heyting algebras, in virtue of $(\text{b}_{1})$, the element $\mathbf{1}$ is a greatest element in Heyting algebra. The property $(\text{h}_{4})$ implies that

[TABLE]

Using the notation (1.2) and the property $(\text{h}_{5})$, we conclude that $\mathbf{0}$ is a least element in Heyting algebra. According to $(\text{h}_{6})$, we have:

[TABLE]

Thus, the last identity and $(\text{h}_{1})$ imply the following:

[TABLE]

The following property characterizes pseudo-complementation:

[TABLE]

Indeed, assume first that $x\leq y\rightarrow z$. Then, in view of ($\text{l}_{1}$–$i$), the monotonicity of $\wedge$ w.r.t. $\leq$ and $(\text{h}_{1})$, we have:

[TABLE]

Conversely, suppose that $x\wedge y\leq z$, that is $x\wedge y=x\wedge y\wedge z$. Then, in virtue of $(\text{h}_{2})$, $(\text{h}_{4})$, $(\text{h}_{3})$, we obtain:

[TABLE]

Using (1.6), we receive immediately:

[TABLE]

which in turn implies:

[TABLE]

Proposition 1.2.2**.**

Let $\textsf{{H}}=\langle\textsf{H};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle$ be a Heyting algebra. Then its restriction $\textsf{{B}}=\langle\textsf{H};\wedge,\vee,\neg,\mathbf{1}\rangle$ is a Boolean algebra if the identity $x\rightarrow y=\neg x\vee y$ holds in H. Conversely, if $\textsf{{B}}=\langle\textsf{B};\wedge,\vee,\neg,\mathbf{1}\rangle$ is a Boolean algebra. Then its expansion $\textsf{{H}}=\langle\textsf{B};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle$, where $x\rightarrow y:=\neg x\vee y$, is a Heyting algebra.

Proof.

Let H be a Heyting algebra in which $x\rightarrow y=\neg x\vee y$. We observe that, because of (1.5), the identity ($\text{b}_{2}$–$i$) is true in H. The identity ($\text{b}_{2}$–$ii$) is also true, for we have:

[TABLE]

Now assume that H is an expansion of a Boolean algebra B, where, by definition, $x\rightarrow y=\neg x\vee y$. We aim to show that all the properties $(\text{h}_{1})$–$(\text{h}_{6})$ are valid in H. Indeed, we obtain:

[TABLE]

∎

Corollary 1.2.2.1**.**

Let $\textsf{{B}}=\langle\textsf{H};\wedge,\vee,\neg,\mathbf{1}\rangle$ be a Boolean algebra. Then for an arbitrary $x\in\textsf{B}$, $\neg\neg x\rightarrow x=\mathbf{1}$, where the operation $x\rightarrow y$ is understood as $\neg x\vee y$.

Proof.

Augmenting B with $\rightarrow$ defined as above, we receive a Heyting algebra. Then we use (1.4) and (1.3). ∎

It should be clear that the simplest non-degenerate Boolean algebra (Fig. 1.1) is also the simplest non-generate Heyting algebra.

We will be using Heyting algebras as a basic semantics for the intuitionistic propositional logic (Section 5.3.3). For this purpose, in the sequel, we will need the following propertied of Heyting algebras.

Proposition 1.2.3**.**

Let $\textsf{{H}}=\langle\textsf{H};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle$ be a Heyting algebra. For arbitrary elements $x$, $y$ and $z$ of H the following properties hold:

[TABLE]

Proof.

We obtain successively the following.

(a) follows straightforwardly from $(\text{h}_{2})$.

To prove (b), using (1.6), we have:

[TABLE]

Then, we apply (1.6) again twice to get (b).

We derive (c) immediately from $x\wedge y\leq x\wedge y$.

(d) and (e) are obvious.

To prove (f), we first have:

[TABLE]

Then, we apply (1.6) twice.

To prove (g), applying (1.6) twice, we have:

[TABLE]

which implies that

[TABLE]

It remains to apply (1.6).

Finally, we obtain (h) as follows:

[TABLE]

Then, we apply (1.6). ∎

Chapter 2 Formal Languages and Their Interpretation

2.1 Formal languages

It is commonly accepted that formal logic is an enterprise, in the broad sense of the word, which is characterized, first of all, by the use, study and development of formal languages. One of the grounds for this characterization is that formal language ensures the codification of accepted patterns of reasoning. From the outset, we have to admit that such a representation of the train of thought in argumentation confines it to a framework of the discrete rather than the continuous. From this viewpoint, an explicit argument is represented in a formal language by a sequence of discrete units.

It is also commonly accepted that logic, formal or otherwise, deals with the concept of truth. Each unit in a formally presented reasoning is assumed to bear truth-related content. Yet, the use of formal language for the codification of the units of truth-related contents does not make logic formal; only the realization that the discrete units, called words, of a formal language, constituting a deduction chain, are codes of forms of judgments rather than “formulations of factual, contingent knowledge” (Carnap) does.111Compare with the notion of elementary propositional function in [WR97], section A $\ast 1$.

Thus we arrive at a twofold view on the units of formal language, which are used to form the codes of formally presented deductions. On the one hand, they are words of a given formal language, satisfying some standard requirements; on the other, they are forms that do not possess any factual content but are intended to represent it. Moreover, the content that is meant to be represented by means of a formal unit is intended to generate an assertion, not command, exclamation, question and the like. Having this in mind, we will be calling these formal units (sentential) formulas or terms, depending on which role they play in our analysis.

Concerning formal deduction, or formal reasoning, we will make a distinction, and emphasize it, between what is known in philosophy of logic as the theory of consequence, or dialectic argument, which is rooted in Aristotle’s Analytica Priora, where the central question is ‘What follows from what?’, and what philosophy of logic calls the theory of demonstration, which can be traced to Analytica Posteriora, where the main question is ‘What can be obtained from known (accepted) premises?’. The formulas qualifying to be answers to the latter question will be called theses or (formal) theorems. We note that the class of such theses depends on the set of premises, as well as on the means of the deduction in use. The theory of consequence will be analyzed in terms of a binary relation between the sets of formulas of a given formal language and the formulas of this language. As to “the means of the deduction in use,” it will be our main focus throughout the book.

After these preparatory remarks, we turn to definition of a formal language. Here we face an obstacle. Since each formal language depends on a particular set of symbols, in order to reach some generality, we are to deal with a schematic language which would contain all main characteristics of many particular languages that are in use nowadays; many other languages of this category can be defined in the future. All our formal languages in focus are sentential, that is, they are intended to serve for defining sentential logical systems. However, for technical purposes, we will occasionally be employing predicate languages, which will be introduced as needed.

The schematic language we define in this section will not be the only one we are going to deal with. In order to advance Lindenbaum method, as we understand it, to the limits we are able to envisage, we will discuss it in the framework of some fragments of first order language as well.

A sentential schematic language $\mathcal{L}$ is assumed to contain symbols of the following pairwise disjoint categories:

• •

a nonempty set $\mathcal{V}$ of sentential (or propositional) variables; we will refer to the elements of $\mathcal{V}$ as $p,q,r,\ldots$, using subscripts if needed;

• •

a set $\mathcal{C}$ (maybe, empty) of sentential (or propositional) constants; we will refer to the elements of $\mathcal{C}$ as $a,b,c,\ldots$, using subscripts if necessary; we assume that the cardinality of the set $\mathcal{C}$ is not bounded from above, that is $0\leq\textit{card}(\mathcal{C})$;

• •

a set $\mathcal{F}$ of sentential (or propositional) connectives is nonempty; we will refer to the elements of $\mathcal{F}$ as $F_{0},F_{1},\ldots,F_{\gamma},\ldots$, where $\gamma$ is any ordinal; for each connective $F_{i}$, there is a positive natural number $\#(F_{i})$ called the arity of the connective $F_{i}$. We will be omitting index and write simply $F$, if confusion is unlikely; the cardinality of $\mathcal{F}$ is not bounded from above; that is $0<\textit{card}(\mathcal{F})$.

We repeat: the sets $\mathcal{V}$, $\mathcal{C}$, and $\mathcal{F}$, each consisting of symbols, are pairwise disjoint, and assume also that the elements of each of these sets are distinguishable in such a way that a concatenation of a number of these symbols can be read uniquely; that is, given a word $w$ of $\mathcal{L}$ of the length 1, one can decide whether $w\in\mathcal{V}$ or $w\in\mathcal{C}$ or $w\in\mathcal{F}$; if the word $w$ has the length greater than 1, then, we assume, it is possible to recognize each symbol of $w$ in a unique way.

Thus $\mathcal{L}$ gives space for defining many specific languages. To denote a language defined by a specification within $\mathcal{L}$ we will be using subscripts or other marks attached to $\mathcal{L}$.

The most important concept within a language is that of formula. To refer to formulas formed by the means of $\mathcal{L}$, we use the letters $\alpha,\beta,\gamma,\ldots$ (possibly with subscripts or other marks), calling them $\mathcal{L}$-formulas. Specifically, these symbols play a role of informal metavariables for $\mathcal{L}$-formulas. For specified languages we reserve the right to employ other notations, about which the reader will be advised. For a special purpose (to deal with structural inference rules), we introduce formal metavariables as well.

Given two sentential languages, $\mathcal{L}^{\prime}$ and $\mathcal{L}^{\prime\prime}$ with $\mathcal{V}^{\prime}\subseteq\mathcal{V}^{\prime\prime}$, $\mathcal{C}^{\prime}\subseteq\mathcal{C}^{\prime\prime}$ and $\mathcal{F}^{\prime}\subseteq\mathcal{F}^{\prime\prime}$, $\mathcal{L}^{\prime\prime}$ is called an extension of $\mathcal{L}^{\prime}$ and the latter is a restriction of the former. An extension $\mathcal{L}^{\prime\prime}$ of a language $\mathcal{L}^{\prime}$ is called primitive if $\mathcal{C}^{\prime}=\mathcal{C}^{\prime\prime}$ and $\mathcal{F}^{\prime}=\mathcal{F}^{\prime\prime}$, that is, when $\mathcal{L}^{\prime\prime}$ is obtained only by adding new variables, if any, to $\mathcal{V}^{\prime}$.

Definition 2.1.1** ($\mathcal{L}$-formulas).**

The set $\textbf{Fm}_{\mathcal{L}}$ of $\mathcal{L}$-formulas is formed inductively according to the following rules$:$

[TABLE]

We will find useful the notion of the degree of a (given) formula $\alpha$, according to the following clauses:

[TABLE]

It is easy to see that the degree of a formula $\alpha$ equals the number of occurrences of the sentential connectives that are contained in $\alpha$.

As can be seen from the last definition, the degree of a formula is an estimate of its “depth.” Also, in the last definition, it is assumed that if $\alpha=F_{i}\alpha_{1}\ldots\alpha_{n}$, that is if $\alpha\notin\mathcal{V}\cup\mathcal{C}$, it begins with some sentential connective ($F$ with $\#(F)=n$ in our case). But then, the words $\alpha_{1},\ldots,\alpha_{n}$ must be recognizable as formulas. Thus it is important to note that for any given word $w$ of the language $\mathcal{L}$, one can decide whether $w$ is an $\mathcal{L}$-formula or not. One of the ways, by which it can be done, is the construction of a formula tree for the formula in question.

Technically, it is convenient to have the notion of metaformula associated with a given language $\mathcal{L}$.

Definition 2.1.2** ($\mathcal{L}$-metaformulas).**

Given a language $\mathcal{L}$, the set $\textit{{Mf}}_{\mathcal{L}}$ of $\mathcal{L}$-metaformulas is defined inductively by the clauses$:$

[TABLE]

The notion of the degree of metaformula is similar to that of formula.

The intended interpretation of metavariables is $\mathcal{L}$-formulas.

Now we turn again to formulas. We will be using the following notation: Given an $\mathcal{L}$-formula $\alpha$,

[TABLE]

It will be assumed that the set $\mathcal{V}$ is decidable and the sets $\mathcal{C}$ and $\mathcal{F}$ are decidable when they are countable; that is, for any $\mathcal{L}$-word $w$ of the length 1, there is an effective procedure which decides whether $w\in\mathcal{V}$, whether $w\in\mathcal{C}$, or whether $w\in\mathcal{F}$. In this case, it is also effectively decidable whether any $\mathcal{L}$-word is an $\mathcal{L}$-formula or not.

The cardinality of a language $\mathcal{L}$, symbolically $\textit{card}(\mathcal{L})$, is $\textit{card}(\textit{{Fm}}_{\mathcal{L}})$. We will be using both notations. We note that for any language $\mathcal{L}$, $\textit{card}(\mathcal{L})\geq\aleph_{0}$.

The notion of a subformula of a (given) formula is defined inductively through the notion of the set $\mathbf{Sub}(\alpha)$ of all subformulas of a (given) formula $\alpha$ as follows:

[TABLE]

A subformula $\beta$ of a formula $\alpha$ is called proper if $\beta\in\mathbf{Sub}(\alpha)$ and $\beta\neq\alpha$.

A useful view on a subfomula of a formula is that the former is a subword of the latter and is a formula itself.

The formula tree for a formula $\alpha$ is a finite directed edge-weighted labeled tree where each node is labeled by a subformula of the initial formula $\alpha$. The node labeled by $\alpha$ is the root of the tree; that is its indegree equals 0. Suppose a node is labeled by $\beta\in\mathbf{Sub}(\alpha)$. If $\beta\in\mathcal{V}\cup\mathcal{C}$, we call this node a leaf; its outdegree equals 0. Now assume that $\beta=F_{i}\beta_{1}\ldots\beta_{n}$, that is $\#(F_{i})=n$. Then outdegree of this node is $n$. Since $\alpha$ may have more than one occurrence of a subformula $\beta$, all nodes labeled by the last formula will have outdegree equal to $\#(F_{i})$. Then, $n$ directed edges will connect this node to $n$ nodes labeled by the subformulas $\beta_{1},\ldots,\beta_{n}$, wherein the weight $i$ is assigned to the edge connecting $\beta$ with $\beta_{i}$. These $n$ nodes are distinct from one another even if some of $\beta_{1},\ldots,\beta_{n}$ may be equal. We note that each occurrence of every subformula of $\alpha$ is a label of a formula tree for $\alpha$. Also, we observe that the degree of each $\beta_{i}$ is less than the degree of $\beta$. A formula tree for a given formula $\alpha$ is completed if each complete path from the root ends with a leaf. This necessarily happens, for the degree of a formula is a nonnegative integer.

We note that we use weighted edges only in order to identify a (unique) path from the root of a tree to a particular node.

It should be obvious that all formula trees for a given formula are isomorphic as graphs. So one can speak of the formula tree for a given formula.

Let us illustrate the last definition for the formula $F_{i}F_{j}app$ with $\#(F_{i})=\#(F_{j})=2$. Below we identify the nodes with their labels.

It should be clear that the formula tree for an initial formula allows us to work with each occurrence of every subformula of this formula separately and also to follow through the subformula relation even within a designated occurrence of a subformula of the initial formula. This observation will be used in the operation of replacement below.

Let us consider any leaf of the formula tree of Figure 2.1, say the one labeled by $a$. We observe that the nodes of the path from the root to the selected leaf consist of all subformulas of the initial formula which contain $a$ as their subformula. Now let us color the first occurrence of $p$ in red and the second in blue so that we obtain

[TABLE]

We use color only for the sake of clarity to identify the path we are working with at the moment (see below); we could use weights of edges instead.

Next we consider the two paths: the first,

[TABLE]

corresponds to the red occurrence of $p$ in the sense that its nodes constitute all subformulas of the initial formula, which contain this red occurrence of $p$; the second path,

[TABLE]

corresponds to the blue occurrence of $p$ and satisfies the same property regarding this occurrence. Now we substitute for both occurrences of $p$ in the initial formula any formula $\alpha$ so that we obtain the formula

[TABLE]

Instead of the tree of Figure 1 we will get the new tree:

If $\alpha\notin\mathcal{V}\cup\mathcal{C}$, the tree of Figure 2.2 is not a formula tree. However, the last tree shows that the $\mathcal{L}$-word $F_{i}F_{j}a\alpha\alpha$ obtained by this substitution is an $\mathcal{L}$-formula. Instead of the paths (red) and (blue) we observe the following paths:

[TABLE]

and

[TABLE]

And again, we notice the same property: the nodes of (red $\alpha$) form the set of subsets of the red occurrence of $\alpha$ in the formula (red-blue $\alpha$); the same property regarding the blue occurrence of $\alpha$ is true for the path (blue $\alpha$).

This observation will help us discuss a syntactic transformation which is vital for the theory of sentential logic. Essentially, this transformation makes speak of logic as a system of forms of judgments rather than that of individual judgments about facts.

First we define a transformation related to a formula $\alpha$ and a sentential variable $p$, denoting this operation by $\sigma^{\alpha}_{p}$. Before proceeding, we note that the initial formula $F_{i}F_{j}app$ was chosen rather arbitrarily; it might be that it does not contain $p$. Having this in mind, given any $\mathcal{L}$-formula $\alpha$ and any sentential variable $p$, we define a unary substitution $\sigma^{\alpha}_{p}:\textit{{Fm}}_{\mathcal{L}}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$ as follows:

[TABLE]

At first sight, it may seem that unary substitution is not powerful enough. For example, let us take a formula $F_{i}F_{j}apq$, where connectives $F_{i}$ and $F_{j}$ have the arity equal to 2. Assume that we want to produce a formula $F_{i}F_{j}a\alpha\beta$. Suppose we first obtain:

[TABLE]

And we face a problem if $\alpha$ contains $q$, for then we get

[TABLE]

which is not necessarily equal to $F_{i}F_{j}a\alpha\beta$. To overcome this difficulty, we select a variable which occurs neither in $\alpha$ nor in the initial formula $F_{i}F_{j}apq$. Suppose this variable is $r$. Then, we first produce:

[TABLE]

Now the desirable formula can be obtained in two steps:

[TABLE]

Thus we observe:

[TABLE]

This leads to the conclusion that the composition of two and more unary substitutions may result in substitution of a different kind; namely, we can obtain the formula $F_{i}F_{j}a\alpha\beta$ from the formula $F_{i}F_{j}apq$ by substituting simultaneously the formulas $\alpha$ and $\beta$ for the variables $p$ and $q$, respectively. Thus we arrive at the following definition.

Definition 2.1.3** (substitution).**

A syntactic transformation $\sigma:\textit{{Fm}}_{\mathcal{L}}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$ is called a uniform $($or simultaneous$)$ substitution $($or simply a substitution or $\mathcal{L}$-substitution$)$ if it is an extension of a map $\sigma_{0}:\mathcal{V}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$, satisfying the following conditions$\,:$

[TABLE]

Given a substitution $\sigma$ and a formula $\alpha$, $\sigma(\alpha)$ is called a substitution instance of $\alpha$.

For a set $X$ of $\mathcal{L}$-formulas and an $\mathcal{L}$-substitution $\sigma$, we denote:

[TABLE]

Thus, for any substitution $\sigma$,

[TABLE]

Also, we observe:

[TABLE]

(Exercise 2.1.2)

We leave for the reader to prove that, given a fixed formula $\alpha$, any simultaneous substitution applied to $\alpha$ results in the composition of singular substitutions applied to $\alpha$. (See Exercise 2.1.3.)

Proposition 2.1.1**.**

For any map $\sigma_{0}:\mathcal{V}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$, there is a unique substitution $\sigma:\textit{{Fm}}_{\mathcal{L}}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$ extending $\sigma_{0}$.

Proof is left to the reader. (Exercise 2.1.4.)

The last proposition allows us to think of a substitution simply as a map $\sigma:\mathcal{V}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$, which will be convenient when we want to define a particular substitution. On the other hand, the property (b) of Definition 2.1.3 allows us to look at any substitution as a mapping satisfying a special algebraic property, which will also be convenient when we want to use this property.

For now, we want to note that composition of finitely many substitutions is a substitution. Moreover, for any substitutions $\sigma_{1}$, $\sigma_{2}$ and $\sigma_{3}$,

[TABLE]

(We leave this property for the reader; see Exercise 2.1.5.) This implies that the set of all substitutions, related to a language $\mathcal{L}$, along with composition $\circ$ constitute a monoid with the identity element

[TABLE]

which will be calling the identity substitution. It must be clear that for any formula $\alpha$,

[TABLE]

Because of (2.1), any grouping in

[TABLE]

leads to the same result. For this reason, parentheses can be omitted, if we do want to be specific.

We will call a set $F\subseteq\textit{{Fm}}_{\mathcal{L}}$ closed under substitution if for any $\mathcal{L}$-formula $\alpha$ and substitution $\sigma$,

[TABLE]

We have already noted that the tree of Figure 2.2 is not a formula tree if $\alpha\notin\mathcal{V}\cup\mathcal{C}$. However, we can build the formula tree for $\alpha$. It does not matter how it looks; so we depict it schematically as follows:

Attaching two copies of the last tree to the tree of Figure 2.2, we obtain the tree for $F_{i}F_{j}a\alpha\alpha$.

We will call one copy of the formula tree for $\alpha$ the tree for red $\alpha$ and the other copy the tree for the blue $\alpha$.

Now let us take any formula $\beta$ and construct the formula tree for it depicted as follows:

Now in the path

[TABLE]

of the tree of Figure 2.4, we replace all red occurrences of $\alpha$ by $\beta$ and replace the tree for red alpha by the tree for $\beta$ (Figure 2.5), arriving thus at the following tree:

This is the formula tree for $F_{i}F_{j}a\beta\alpha$. The syntactic transformation just described shows that replacing a designated subformula of a formula, we obtain a formula. Such a transformation is called replacement. Designating a subformula $\beta\in\mathbf{Sub}(\alpha)$, we write $\alpha[\beta]$. The result of the replacement of this particular subformula $\beta$ with a formula $\gamma$, we denote by $\alpha[\gamma]$.

Before going over examples of some sentential languages, we discuss how any metaformula can be seen in the light of the notion of substitution. It must be clear that the intended interpretation of any metaformula $\phi$ is the set of formulas of a particular shape.

Similar to Definition 2.1.3, any map $\bm{\sigma}_{0}:\textit{{Mv}}_{\mathcal{L}}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$ can uniquely be extended to $\bm{\sigma}:\textit{{Mf}}_{\mathcal{L}}\longrightarrow\textit{{Fm}}_{\mathcal{L}}$. We will call both $\bm{\sigma}_{0}$ and its extension $\bm{\sigma}$ a realization, or instantiation, of metaformulas in $\mathcal{L}$. The following observation will be useful in the sequel. An instantiation $\bm{\sigma}$ is called simple if it is the extension of $\bm{\sigma}_{0}:\textit{{Mv}}_{\mathcal{L}}\longrightarrow\mathcal{V}_{\mathcal{L}}$.

Proposition 2.1.2**.**

Let $\phi$ be an $\mathcal{L}$-metaformula and $\Sigma_{\phi}$ be the class of all instantiations of $\phi$. Then for any $\mathcal{L}$-substitution $\sigma$ and any $\mathcal{L}$-formula $\alpha$,

[TABLE]

Proof is leaft to the reader. (Exercise 2.1.6)

Below we give examples of languages that are specifications of the schematic language $\mathcal{L}$. All these languages include a denumerable set $\mathcal{V}$ as the set of sentential variables.

$\mathcal{L}_{A}$:

In this language, there is no sentential constants; there are four (assertoric) logical connectives: $\wedge$ (conjunction), $\vee$ (disjunction), $\rightarrow$ (implication or conditional), and $\neg$ (negation), having the arities $\#(\wedge)=\#(\vee)=\#(\rightarrow)=2$ and $\#(\neg)=1$. It is customary to use an infix notation for this language; however, the use of infix notation for this language requires two additional symbols: “(” and “)” called the left and right parenthesis, respectively. Accordingly, the definition of formula will be different: $(\alpha\wedge\beta)$, $(\alpha\vee\beta)$, $(\alpha\rightarrow\beta)$ and $\neg\alpha$ are formulas, whenever $\alpha$ and $\beta$ are. The parentheses do not apply to atomic formulas and negations. Sometimes, we will not employ all the connectives of $\mathcal{L}_{A}$ but some of them, continuing to call this restricted language $\mathcal{L}_{A}$. Sometimes, $\mathcal{L}_{A}$ is considered in its extended version, when a connective $\leftrightarrow$ is added; if not, then the last connective is used as an abbreviation:

[TABLE]

$\mathcal{L}_{B}$:

This language extends $\mathcal{L}_{A}$ by adding to it two constants: $\top$ (truth or verum) and $\bot$ (falsehood or falsity or falsum or absurdity). Sometimes, only one of these constants will be employed. The parentheses do not apply to atomic formulas, negations and to the constants $\top$ and $\bot$. We will call all these variants by $\mathcal{L}_{B}$, indicating every time the list of constants.

$\mathcal{L}_{C}$:

This language extends either $\mathcal{L}_{A}$ or $\mathcal{L}_{B}$ with two sentential connectives (modalities): $\Box$ (necessity) and $\Diamond$ (possibility) both of the arity 1, that is $\#(\Box)=\#(\Diamond)=1$. In addition to the corresponding requirements above, the parentheses do not apply to the formulas that start with the modalities $\Box$ and $\Diamond$. Sometimes, when only one of these modalities is employed, we continue to call this language $\mathcal{L}_{C}$.

In the sequel we will employ more formal languages, which do not fit the proposed framework but closely related to it.

Exercises 2.1

Here we give another definition of a formula tree. This new definition is convenient when we deal with an algorithmic problem, in which case the sets $\mathcal{V}$, $\mathcal{C}$ and $\mathcal{F}$ are regarded countable and effectively decidable. One of such problems will be raised below as an exercise. We note that in this definition a designated path can be identified exclusively by the nodes it comprises.

The formula tree for a formula $\alpha$ is a finite directed labeled tree where each node is labeled with a pair $\langle n,\beta\rangle$, where $n$ is a natural number and $\beta$ is a subformula of $\alpha$.

There is a unique node, called the root, labeled by $\langle\textit{{p}}_{0},\alpha\rangle$, the ingdegree of which is [math].222We remind the reader that $\textit{{p}}_{0},\textit{{p}}_{1},\textit{{p}}_{2},\ldots$ is the sequence of prime numbers. The ingdegree of all other nodes of the tree, if any, equals $1$. Let a node $v$ be labeled with $\langle n,\beta\rangle$, where $\beta\in\mathcal{V}\cup\mathcal{C}$. Then the outdegree of $v$ is always [math]. Such nodes are called leaves. (As the reader will see below, leaves are always present in a formula tree.) Thus if $\alpha\in\mathcal{V}\cup\mathcal{C}$, the formula tree of $\alpha$ consists of only one node, the root, which is also a leaf. Assume that $\beta=F\beta_{1}\ldots\beta_{k}$ with $F\in\mathcal{F}$ is a proper subformula of $\alpha$ and a node $v$ is labeled with $\langle n,\beta\rangle$. Suppose that $\textit{{p}}_{j}$ is the greatest prime number that divides $n$. Then the outdegree of $v$ is $\#(F)$, that is in our case, equals $k$. And then $v$ will be connected via $k$ edges to $k$ different nodes, $v_{1},\ldots,v_{k}$. (The direction of each such edge is from $v$ to $v_{i}$.) We label $v_{i}$ with $\langle n\cdot\textit{{p}}_{j+i},\beta_{i}\rangle$. Thus, if $\beta_{i}=\beta_{j}$, then the two distinct nodes, $v_{i}$ and $v_{j}$, will be labeled with labels distinct in their first place and equal in the second. Also, we note that the degree of each $\beta_{i}$ is less than the degree of $\beta$.

Use the new definition of formula tree to prove the following.

There is a mechanical procedure $($an algorithm$)$ which, given a list of pairs $\langle n_{1},\alpha_{1}\rangle,\ldots,\langle n_{k},\alpha_{k}\rangle$, where each $n_{i}$ is a positive integer, can assemble a formula tree, where the pairs are regarded as the nodes of the tree, or states that such a tree does not exist. 2. 2.

Prove the inclusions (2.0). 3. 3.

Prove that $(a)$ for any fixed formula $\alpha$ and any fixed substitution $\sigma$, there are unary substations $\sigma_{1},\ldots,\sigma_{n}$ such that $\sigma(\alpha)=\sigma_{1}\circ\ldots\circ\sigma_{n}(\alpha)$; however, $(b)$ for any fixed substitution $\sigma$, there is no finitely many fixed unary substitutions $\sigma_{1},\ldots,\sigma_{n}$ such that for any formula $\alpha$, $\sigma(\alpha)=\sigma_{1}\circ\ldots\circ\sigma_{n}(\alpha)$. 4. 4.

Prove Proposition 2.1.1. 5. 5.

Prove (2.1). 6. 6.

Prove Proposition 2.1.2.

2.2 Semantics of formal language

One of our concerns in this book is to show how truth can be transmitted through formulas of a formal language by formally presented deduction. Calling a formula true, we will mean a kind of truth which does not depend on any factual content. Moreover, sharing the view of the multiplicity of the nature of truth, we will be dealing rather with degrees of truth, calling them truth values. Then, the idea of truth will find its realization in the idea of validity.

Concerning the independence of any factual, contingent content in relation to truth values, let us consider the following two sentences — ‘Antarctica is large’ and ‘Antarctica is large or Antarctica is not large’. If our formal language contains a symbol for the grammatical disjunction “$\ldots_{1}\leavevmode\nobreak\ \text{or}\leavevmode\nobreak\ \ldots_{2}$”, say “$\ldots_{1}\vee\ldots_{2}$” (as in the languages $\mathcal{L}_{A}$–$\mathcal{L}_{C}$ of Section 2.1), and a symbol for creating the denial of sentence, say “$\neg\ldots$” (also as in $\mathcal{L}_{A}$–$\mathcal{L}_{C}$), we can write in symbolic form the first sentence as $p$ and the second as $p\vee\neg p$. From the viewpoint of Section 2.1, both formal expressions are formulas of the language $\mathcal{L}_{A}$. Now, depending on familiarity with geography, as well as of personal experience, one can count $p$ true or false. The second formula $p\vee\neg p$, however, in some semantic systems takes steadily the truth value true, regardless of any personal relation towards $p$. The universality of this kind will be stressed in the idea of validity.

From the last example, it should be clear the distinction between the statements, the truth value of which (understood as the degree of trust or that of informativeness) is dependent on the contingency of facts, the level of knowledge or personal beliefs, and the formal judgments, which obtain their logical status or meaning determined by semantic rules. These rules will allow us to interpret the formal judgments of a language in abstract structures, reflecting the structural character of these judgments, as well as the universal character of their validity, thereby understanding their invalidity as the failure to satisfy this universality.

In this book, semantics will play pragmatic rather than explanatory role;333However, since we state validity conditions for formal judgments, these conditions generate the meanings of the judgments, according to the point of view that has been emphasized by Wittgenstein in Tractatus; cf. [Wit01], 4.024. Also, compare with Curry’s statement that “the meaning of a concept is determined by the conditions under which it is introduced into discourse;” cf. [Cur66], section II.2. namely we will be stressing the use of semantic structures as separating means. This will be explained in Section 4.3. Moreover, we want to emphasize that in our approach to semantics we adhere to the relativistic position, according to which a single formal judgment can be valid according to one semantic system and invalid with respect to another.

Now we turn to the definition of semantics of the schematic language $\mathcal{L}$ exemplified by the languages $\mathcal{L}_{A}$–$\mathcal{L}_{C}$ in Section 2.1. Depending on one’s purposes, or depending on the lines, along which the semantics in question can be employed, the semantics we propose can use the items of the following two categories — the algebras of type $\mathcal{L}$ and expansions of the latter called logical matrices. Later on, we will generalize the notion of logical matrix, when we discuss consequence relation in Chapter 3.

The following semantic concepts will be specified later on as needed.

Definition 2.2.1** (algebra of type $\mathcal{L}$).**

An algebra of type $\mathcal{L}$ $($or an $\mathcal{L}$-algebra or simply an algebra when a type is specified ahead and confusion is unlikely$)$ is a structure $\textsf{{A}}=\langle\textsf{A};\mathcal{F},\mathcal{C}\rangle$, where A is a nonempty set called the carrier $($or universe$)$ of A; $\mathcal{F}$, which in the notion of $\mathcal{L}$-formulas represents logical connectives, now represents a set of finitary operations on A of the corresponding arities; and $\mathcal{C}$, which is a set of logical constants, now represents a set of nullary operations on A. As usual, we use the notation $|\textsf{{A}}|=\textsf{A}$. The part $\langle\mathcal{F},\mathcal{C}\rangle$ of the structure A is called its signature. Thus, referring to an algebra A, we can say that it is an algebra of signature $\langle\mathcal{F},\mathcal{C}\rangle$ or of signature $\mathcal{F}$, if $\mathcal{C}=\emptyset$.

Thus any $\mathcal{L}$-formula in relation to any algebra of type $\mathcal{L}$ becomes a term. Naturally, the sentential variables of a formula understood as term become the individual variables of this term. Since each algebraic term of, say, $n$ variables can be read as an $n$-ary derivative operation in an algebra of type $\mathcal{L}$, so can be understood any $\mathcal{L}$-formula containing $n$ sentential variables.

Definition 2.2.2** (inessential expansion of an algebra, equalized algebras).**

Given an algebra $\textsf{{A}}=\langle\textsf{A};\mathcal{F},\mathcal{C}\rangle$, we obtain an inessential expansion of A if we add to $\mathcal{F}$ one or more terms regarding them as new signature operations, or if we add to $\mathcal{C}$ one or more symbols with their intended interpretation as elements of A. Two algebras $($or their signatures$)$ are called equalized if they have inessential expansions of one and the same type.

The central notion of Lindenbaum method is that of formula algebra associated with a particular language. The formula algebra of type $\mathcal{L}$ has $\textit{{Fm}}_{\mathcal{L}}$ as its carrier and the signature operations as defined in Definition 2.1.1. This algebra is denoted by $\mathfrak{F}_{\mathcal{L}}$. Thus we have:

[TABLE]

Analogously, the set of $\mathcal{L}$-metaformulas along with the set $\mathcal{C}$ regarded as nullary operations and the set $\mathcal{F}$ regarded as non-nullary operations constitute a metaformula algebra $\mathfrak{M}_{\mathcal{L}}$ of type $\mathcal{L}$.

A relation between the $\mathcal{L}$-formulas and the algebras of type $\mathcal{L}$ is established through the following notion.

Definition 2.2.3** (valuation, value of a formula in an algebra).**

Let A be an algebra of type $\mathcal{L}$. Then any map $v:\mathcal{V}\longrightarrow|\textsf{{A}}|$ is called a valuation $($or an assignment$)$ in the algebra A. Then, given a valuation $v$, the value of an $\mathcal{L}$-formula $\alpha$ with respect to $v$, in symbols $v[\alpha]$, is defined inductively as follows$\,:$

[TABLE]

If $\mathcal{V}^{\prime}\subset\mathcal{V}$, then a map $v:\mathcal{V}^{\prime}\longrightarrow|\textsf{{A}}|$ is called a $\mathcal{V}^{\prime}$-valuation, or a valuation restricted to $\mathcal{V}^{\prime}$.

It makes sense to denote the mapping

[TABLE]

by the same letter $v$. The following observation is a justification for this usage.

Proposition 2.2.1**.**

Let $v$ be a valuation in an algebra A. Then the mapping $v:\alpha\mapsto v[\alpha]$ defines a homomorphism $\mathfrak{F}_{\mathcal{L}}\longrightarrow\textsf{{A}}$. Conversely, each homomorphism $\mathfrak{F}_{\mathcal{L}}\longrightarrow\textsf{{A}}$ is a valuation.

Proof of the first part is based on the clauses (a)–(c) of Definition 2.2.3. The second part is obvious.

Thus, given a valuation $v$ in A and a formula $\alpha(p_{1},\ldots,p_{n})$ where $p_{1},\ldots,p_{n}$ are all variables occurring in $\alpha$, we observe that

[TABLE]

Grounding on the last observation base in turn on Proposition 2.2.1, very often a valuation is defined as a homomorphism $\mathfrak{F}_{\mathcal{L}}\longrightarrow\textsf{{A}}$.

Comparing (b)–(c) of Definition 2.2.3 with (a)–(b) of Definition 2.1.3, we obtain the following.

Proposition 2.2.2**.**

Any substitution is a valuation in $\mathfrak{F}_{\mathcal{L}}$ and vice versa. Hence any substitution is an endomorphism $\mathfrak{F}_{\mathcal{L}}\longrightarrow\mathfrak{F}_{\mathcal{L}}$.

The converse of the last conclusion is also true: any endomorphism $\mathfrak{F}_{\mathcal{L}}\longrightarrow\mathfrak{F}_{\mathcal{L}}$ can be regarded as a substitution. (Exercise 2.2.1.)

Now we turn to a central notion of any semantics — the notion of* validity*.444W. and M. Kneale note, “[…] logic is not simply valid argument but the reflection upon principles of validity;” [KK62], section I.1. This notion in turn is defined in the framework of the notion of logical matrix.

Definition 2.2.4** (logical matrix of type $\mathcal{L}$).**

A logical matrix $($or simply a matrix$)$ of type $\mathcal{L}$ is a structure $\textsf{{M}}=\langle\textsf{{A}},D(x)\rangle$, where A is a nontrivial algebra of type $\mathcal{L}$, which, if considered as part of M, is called an M-algebra, and $D(x)$ is a predicate on $|\textsf{{A}}|$. We will also denote a matrix as a structure $\langle\textsf{A};\mathcal{F},\mathcal{C},D(x)\rangle$ or as a structure $\langle\textsf{A};\mathcal{F},D(x)\rangle$, if $\mathcal{C}=\emptyset$. We will also denote a matrix as $\langle\textsf{{A}},D\rangle$ or as $\langle\textsf{A};\mathcal{F},D\rangle$ or as $\langle\textsf{A};\mathcal{F},D\rangle$, if $\mathcal{C}=\emptyset$, where $D\subseteq|\textsf{{A}}|$. In the last three notations $D$ is called the set of designated elements or a logical filter $($or simply a filter$)$ in $($or of$)$ M.

We should remark that using “logical” in the last two definitions was a bit hasty, for the first connection with logic emerges, at least in the case of logical matrices, in the next definition when we separate semantically valid $\mathcal{L}$-formulas from the other formulas.

Definition 2.2.5**.**

Let $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be a logical matrix of type $\mathcal{L}$. Then a formula $\alpha$ is satisfied by a valuation $v$ in A if $v[\alpha]\in D$, in which case we say that $v$ satisfies $\alpha$ in M; further, $\alpha$ is semantically valid $($or simply valid$)$ in M, symbolically $\textsf{{M}}\models\alpha$ or $\models_{\textbf{M}}\alpha$, if for any valuation $v$ in A, $v[\alpha]\in D$. If a formula is not valid in a matrix, it is called invalid in this matrix or is rejected by the matrix or one can say that this matrix rejects the formula. If $v[\alpha]\notin D$ in M, $v$ is a valuation rejecting or refuting $\alpha$. The set of all formulas valid in a matrix M is denoted by $L\textsf{{M}}$ and is called the logic of M.

Proposition 2.2.3**.**

Let $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be a matrix $($of type \mathcal{L}$$). Then for any substitution $\sigma$, if $\textsf{{M}}\models\alpha$, so is $\textsf{{M}}\models\sigma(\alpha)$.

Proof.

Let $v$ be any valuation in A. According to Propositions 2.2.2 and 2.2.1, $\sigma:\mathfrak{F}_{\mathcal{L}}\longrightarrow\mathfrak{F}_{\mathcal{L}}$ and $v:\mathfrak{F}_{\mathcal{L}}\longrightarrow\textsf{{A}}$ are homomorphisms. Then $v\circ\sigma$ is also a homomorphism $\mathfrak{F}_{\mathcal{L}}\longrightarrow\textsf{{A}}$ and hence, by Proposition 2.2.1, is a valuation. Therefore, $\textsf{{M}}\models\alpha$ implies that $v[\sigma(\alpha)]\in D$. ∎

The last proposition induces a way of how, given a matrix, to obtain a matrix on the formula algebra so that both matrices validate the same set of formulas.

Let $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be a matrix. We denote

[TABLE]

and then define a matrix

[TABLE]

We observe that for any formula $\alpha$,

[TABLE]

Indeed, let $\textsf{{M}}_{\textit{Fm}}\models\alpha$. Then for any substitution $\sigma$ (which, according to Proposition 2.2.2, is a valuation in $\mathfrak{F}_{\mathcal{L}}$), $\sigma(\alpha)\in D_{\textsf{M}}$; in particular, $\iota(\alpha)=\alpha\in D_{\textsf{M}}$, that is $\textsf{{M}}\models\alpha$.

Now suppose that $\textsf{{M}}\models\alpha$, that is $\alpha\in D_{\textsf{M}}$. In virtue of Proposition 2.2.3, $D_{\textsf{M}}$ is closed under substitution. This completes the proof of the equivalence above.

Next let us consider $\textsf{{M}}=\langle\mathfrak{F}_{\mathcal{L}},D\rangle$. We observe that if $\alpha\in D_{\textsf{M}}$, that is $\textsf{{M}}\models\alpha$, then, since, by virtue of Proposition 2.2.2, each substitution is a valuation in $\mathfrak{F}_{\mathcal{L}}$ and vice versa, $\alpha\in D$.

Now let $D^{\prime}\subseteq D$ and $D^{\prime}$ be closed under substitution. Assume that $\alpha\in D^{\prime}$. Then, obviously, $\textsf{{M}}\models\alpha$ and hence $\alpha\in D_{\textsf{M}}$.

Thus we have obtained the following.

Proposition 2.2.4**.**

For any matrix M, there is a matrix on the formula algebra, namely $\textsf{{M}}_{\textit{Fm}}$, such that both matrices validate the same set of $\mathcal{L}$-formulas. Moreover, given a matrix $\textsf{{M}}=\langle\mathfrak{F}_{\mathcal{L}},D\rangle$, the filter of the matrix $\textsf{{M}}_{\textit{Fm}}=\langle\mathfrak{F}_{\mathcal{L}},D_{\textsf{M}}\rangle$ is the largest subset of $D$ closed under substitution. Thus, if $D$ itself is closed under substitution, then $D=D_{\textsf{M}}$.

The importance of the last proposition for what follows is that it shows that the matrices of the form $\langle\mathfrak{F}_{\mathcal{L}},D\rangle$, where a filter $D$ is closed under substitution, suffice for obtaining all sets of valid $\mathcal{L}$-formulas, which can be obtained individually by the matrices of type $\mathcal{L}$. This observation will be clarified below as Lindenbaum’s Theorem; see Proposition 3.3.4.

Now we turn to some special matrices which have played their important role in the development of sentential logic. In all these matrices, the filter of designated elements consists of one element. In this connection, we note the following equivalence, which will be used throughout: If $D=\{c\}$, then

[TABLE]

In the sequel, we find useful the following property.

Proposition 2.2.5**.**

Let $\textsf{{M}}_{1}=\langle\textsf{{A}}_{1},D_{1}\rangle$ and $\textsf{{M}}_{2}=\langle\textsf{{A}}_{2},D_{2}\rangle$ be matrices of the same type. Also, let $h$ be an epimorphism of $\textsf{{A}}_{1}$ onto $\textsf{{A}}_{2}$ such that $h[D_{1}]\subseteq D_{2}$. Then $L\textsf{{M}}_{1}\subseteq L\textsf{{M}}_{2}$

Proof.

Let $v$ be a valuation in $\textsf{{A}}_{2}$. Since $h$ is an epimorphisms, for each variable $p_{\gamma}$, there is an element $x_{\gamma}\in|\textsf{{A}}_{1}|$ such that $h(x_{\gamma})=v[p_{\gamma}]$. We define a valuation $v^{\prime}$ in $\textsf{{A}}_{1}$ as follows: $v^{\prime}[p_{\gamma}]=x_{\gamma}$, for any variable $p_{\gamma}$. It is obvious that $h(v^{\prime}[p_{\gamma}])=v[p_{\gamma}]$. Assume that $\alpha\in L\textsf{{M}}_{1}$; in particular, $v^{\prime}[\alpha]\in D_{1}$. This implies that $v[\alpha]\in D_{2}$. ∎

2.2.1 The logic of a two-valued matrix

We begin with a well-known matrix of the so-called “two-valued logic.” The significance of this matrix in the history of logic is difficult to overestimate. The two-valued matrix was assumed, first, to distinguish true statements from false ones; and, second, to validate only the former. As we will see below, the main logic laws such as, for example, the law of identity, the law of contradiction, the law of the excluded middle (see below) and others can be demonstrated as valid formulas in this matrix. For this reason, it is worth considering this matrix first. Later on, we will explain another significance of this matrix, purely algebraic in nature, which leads to a very important view on this matrix as a refuting and separating means.

The two-valued matrix assumes two main variants of formulation — as a matrix of type $\mathcal{L}_{A}$ and as that of type $\mathcal{L}_{B}$. As will be seen below, the difference between these variants concerns only semantic rules and does not affect essentially the set of valid formulas in the corresponding matrices. For this reason, we denote both variants by $\textsf{{B}}_{2}$. The elements of $\textsf{{B}}_{2}$ are denoted by $\mathbf{0}$ (false) and $\mathbf{1}$ (true), which constitute a Boolean algebra with $\mathbf{0}$ as the least element and $\mathbf{1}$ as the greatest with respect to the partial ordering $\mathbf{0}\leq\mathbf{1}$. According to the intended interpretation, $\mathbf{1}$ represents a truth value true, $\mathbf{0}$ represents false. Being viewed as a 2-element Boolean algebra of type $\mathcal{L}_{A}$, the connectives $\wedge$, $\vee$ and $\neg$ are interpreted as meet, join and complementation, respectively, while

[TABLE]

This leads to the familiar truth tables:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

We observe that for any $x,y\in|\textsf{{B}}_{2}|$,

[TABLE]

If one regards $\textsf{{B}}_{2}$ (more exactly, its counterpart) as an algebra of type $\mathcal{L}_{B}$, two nullary operations, $\mathbf{0}$ and $\mathbf{1}$, should be added to the signature, along with the intended interpretation of $\bot$ and $\top$ as $\mathbf{0}$ and $\mathbf{1}$, respectively. Making of $\textsf{{B}}_{2}$ a logical matrix, we add a logical filter $\{\mathbf{1}\}$. Thus a formula $\alpha$ of type $\mathcal{L}_{A}$ (or of type $\mathcal{L}_{B}$) is valid in $\textsf{{B}}_{2}$ if for any valuation $v$,

[TABLE]

We denote both, the algebra and the matrix, grounded on this algebra, by $\textsf{{B}}_{2}$. It must be clear that any $\mathcal{L}_{A}$-formula is valid in the matrix $\textsf{{B}}_{2}$ of type $\mathcal{L}_{B}$ if and only if it is valid in $\textsf{{B}}_{2}$ of type $\mathcal{L}_{A}$.

A formula $\alpha$ valid in $\textsf{{B}}_{2}$ is called a classical tautology. It is not difficult to see that the following formulas are classical tautologies:

[TABLE]

as well as the following:

[TABLE]

The above tautologies had been known from ancient times. In modern times, such tautologies as the following have been in focus:

[TABLE]

By the two-valued logic, one usually means the set of all classical tautologies.

2.2.2 The Łukasiewicz logic of a three-valued matrix

Perhaps, the “Łukasiewicz 3-valued logic” is the best-known of all multiple-valued systems alternative to the set of classical tautologies. The matrix which defines this “logic” has three values, $\mathbf{0}$ (false), $\bm{\tau}$ (indeterminate) and $\mathbf{1}$ (true), which are arranged by a linear ordering as follows: $\mathbf{0}\leq\bm{\tau}\leq\mathbf{1}$. On this carrier, an algebra of type $\mathcal{L}_{A}$ is defined in such a way that $\wedge$ and $\vee$ are interpreted as meet and join in the 3-element distributive lattice; then, $\neg$ and $\rightarrow$ are defined according to the following tables:

[TABLE]

[TABLE]

We denote this algebra by $\textsf{{\L}}_{3}$. Actually, when we have defined $\neg$ in $\textsf{{\L}}_{3}$ as above, the operation $\rightarrow$ can be defined according to (2.3). Moreover, the following identities can be easily checked:

[TABLE]

(Exercise 2.2.6.) Also, we note that, as algebras of type $\mathcal{L}_{A}$, $\textsf{{B}}_{2}$ is a subalgebra $\textsf{{\L}}_{3}$. (See Exercise 2.2.7.)

Now taking $\{\mathbf{1}\}$ as a logical filter, we obtain the Łukaciewicz 3-valued matrix which is also denoted by $\textsf{{\L}}_{3}$.

We note that the law of the excluded middle and Peirce’s law, which are tautologies of the two-valued logic, fail to be tautologous in $\textsf{{\L}}_{3}$. (Exercise 2.2.8.) The law of contradiction is also invalid in $\textsf{{\L}}_{3}$, for the set $\{\bm{\tau}\}\subseteq|\textsf{{\L}}_{3}|$ is closed under $\wedge$ and $\neg$.

By the Łukasiewicz 3-valued logic one means the set of formulas which are validated by $\textsf{{\L}}_{3}$. These formulas are called $\textsf{{\L}}_{3}$-tautologies. It should be clear that the set $\textsf{{\L}}_{3}$-tautologies is a proper subset of the set of classical tautologies. (Exercise 2.2.9.) One time, it had been assumed that the matrix $\langle\textsf{{\L}}_{3},\{\bm{\tau},\mathbf{1}\}\rangle$ validates the classical tautologies and only them. If the first part of the last statement is obviously true, the second is false. The following counterexample is due to A. R. Turquette: the formula $\neg(p\rightarrow\neg p)\vee\neg(\neg p\rightarrow p)$ is a classical tautology but is refuted in the last matrix by the assignment $v[p]=\bm{\tau}$.

2.2.3 The Łukasiewicz modal logic of a three-valued matrix

Both the algebra and matrix $\textsf{{\L}}_{3}$ can be expanded to type $\mathcal{L}_{C}$ as follows:

[TABLE]

The last definitions of the modalities $\Box$ and $\Diamond$ are not independent of the other assertoric connectives, for in the expanded algebra $\textsf{{\L}}_{3}$ the following identities hold:

[TABLE]

We leave for the reader to check this. (See Exercise 2.2.12.)

We observe that the formulas

[TABLE]

are valid in the expanded matrix, while their converses,

[TABLE]

are rejected by it. (See Exercise 2.2.13.)

2.2.4 The Gödel $n$-valued logics

As in the case $\textsf{{\L}}_{3}$, let us consider the three distinct “truth values,” $\mathbf{0}$, $\bm{\tau}$ and $\mathbf{1}$, arranged by a linear ordering as follows: $\mathbf{0}\leq\bm{\tau}\leq\mathbf{1}$. Regarding this chain as a Heyting algebra with $\wedge$, $\vee$, $\rightarrow$ and $\neg$ as meet, join, relative pseudo-complementation and pseudo-complementation, respectively, we get an algebra $\textsf{{G}}_{3}$ of type $\mathcal{L}_{A}$. Thus we arrive at the following truth tables:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

We notice that all properties (2.3) are satisfied in $\textsf{{G}}_{3}$.

Taking into account the relation $\leq$, the above truth tables can be read through the following equalities.

[TABLE]

Taking $\{\mathbf{1}\}$ as a logical filter, we obtain a logical matrix $\textsf{{G}}_{3}$. The last matrix can be generalized if instead of 3 elements we take 4 and more elements and use (2.6) to define the same signature operations as in $\textsf{{G}}_{3}$. Thus we obtain Gödel’s $n$-valued logics $\textbf{G}_{n}$, where $n\geq 3$. We note that (2.6) are also valid in $\textsf{{B}}_{2}$; therefore, it is sometimes convenient to rename the algebra $\textsf{{B}}_{2}$ by $\textbf{G}_{2}$.

The matrices $\textbf{G}_{n}$, $n\geq 2$, have been in particular important in investigation of the lattice of intermediate logics, that is the logics the valid formulas of which contain all intuitionistic tautologies and are included into the set of classical tautologies. In particular, all the matrices $\textbf{G}_{n}$, $n\geq 3$, fail Peirce’s law, the double negation law, as well as both De Morgan’s laws. (Exercise 2.2.14.)

2.2.5 The Dummett denumerable matrix

An denumerable generalization of $\textbf{G}_{n}$, $n\geq 2$, can be obtained if we take take a denumerable set and arrange it by a linear ordering $\leq$ according to type $1+\omega^{\ast}$. We denote the least element by $\mathbf{0}$ and the greatest by $\mathbf{1}$. (We note: the ordinal notation of the former is $\omega$ and of the latter is [math].) Then, introducing the operations $\wedge$, $\vee$, $\rightarrow$ and $\neg$ as meet, join, relative pseudo-complementation and pseudo-complementation, respectively, of a Heyting algebra and equipping the latter algebra with a logical filter $\{\mathbf{1}\}$, we receive the Dummett denumerable matrix LC. As for $\textsf{{G}}_{3}$, the algebra of the Dummett matrix satisfies the properties (2.3) and also (2.6). We note that LC validates the formula

[TABLE]

The set of all formulas valid in this matrix, $L\textsf{{LC}}$, is called the Dummett logic.

M. Dummett shows in [Dum59], theorem 2, that

[TABLE]

In the sequel, we will need another logical matrix whose logic coincides with the Dummett logic LC.

Let us consider a denumerable set arranged linearly according to type $\omega+1$. We treat this structure as a Heyting algebra with a least element $\mathbf{0}$, greatest element $\mathbf{1}$ and operations $\wedge$, $\vee$, $\rightarrow$ and $\neg$ that are defined according to (2.6). Announcing $\{\mathbf{1}\}$ a logical filter, we define the logical matrix $\textbf{LC}^{\ast}$.

Proposition 2.2.6**.**

$L\textbf{LC}=L\textbf{LC}^{\ast}$.

Proof.

We show that

[TABLE]

It is clear that for any $n\geq 2$, the algebra of $\textsf{{G}}_{n}$ is a homomorphic image of the algebra of $\textsf{{LC}}^{\ast}$; see Section 1.2.2. In virtue of Proposition 2.2.5, $L\textsf{{LC}}^{\ast}\subseteq\bigcap_{n\geq 2}L\textsf{{G}}_{n}$.

Now, assume that a valuation $v$ in $\textsf{{LC}}^{\ast}$ refutes a formula $\alpha$, that is $\alpha\notin L\textsf{{LC}}^{\ast}$. Let $\beta_{1},\ldots,\beta_{n}$ be all subformulas of $\alpha$. Then, according to (2.6), the set $\{v[\beta_{1}],\ldots,v[\beta_{n}],\mathbf{0},\mathbf{1}\}$ is the carrier of a subalgebra of the $\textsf{{LC}}^{\ast}$-algebra, which in turn is isomorphic to a $\textsf{{G}}_{n}$-algebra, for some $n\geq 2$. This implies that $\alpha\notin\bigcap_{n\geq 2}L\textsf{{G}}_{n}$. ∎

2.2.6 Two infinite generalizations of Łukasiewicz’ $\textsf{{\L}}_{3}$

The Łukasiewicz algebra $\textsf{{\L}}_{3}$ can be easily generalized if we take for a carrier the interval $[0,1]$ or the rational scale $\mathbb{Q}$ or on the real scale $\mathbb{R}$ arranged in both cases by the ordinary less-than-or-equal relation $\leq$. The set of designated elements in both cases is $\{1\}$. The operations $\neg$ and $\rightarrow$ are defined as follows:

[TABLE]

then, the other operations are defined according to (2.4). This leads to the identities

[TABLE]

which can be taken as definitions of $\wedge$ and $\vee$ as well.

The set of formulas valid in the first matrix, that is when $[0,1]$ is considered in the rational scale, is denoted by $\textsf{{\L}}_{\aleph_{0}}$ and the formulas valid in the second matrix by $\textsf{{\L}}_{\aleph_{1}}$.

So far, we have discussed the semantic rules for the language $\mathcal{L}$. As we introduce other schematic languages later on, we will have to adjust these rules for them. However, although semantic rules allow us to distinguish valid formulas from refuted ones, they, taken alone, do not suffice to analyze reasoning. This echoes the remark due to Aristotle that “it is absurd to discuss refutation (ἔλεγχος) without discussing reasoning (ςνλλογιςμ´ος);” cf. [KK62], section I.4. We discuss the relation of formal deduction between $\mathcal{L}$-formulas in the form of consequence relation. This is a topic of the next chapter.

Exercises 2.2

Show that any endomorphism $f:\mathfrak{F}_{\mathcal{L}}\longrightarrow\mathfrak{F}_{\mathcal{L}}$ can be regarded as a substitution; that is $f$ is a unique extension of $v:\mathcal{V}\longrightarrow\mathfrak{F}_{\mathcal{L}}$ such that $v(p)=f(p)$, for any $p\in\mathcal{V}$. 2. 2.

Prove the second part of Proposition 2.2.1. 3. 3.

Prove that the laws of identity, of contradiction, of the excluded middle, as well as Peirce’s and double negation laws are tautologies in $\textsf{{B}}_{2}$. 4. 4.

Prove the properties (2.3). 5. 5.

Show that for any two $\mathcal{L}_{A}$-formulas $\alpha$ and $\beta$, $\alpha\leftrightarrow\beta$ is a classical tautology if and only if for any $\textsf{{B}}_{2}$-valuation $v$, $v[\alpha]=v[\beta]$. 6. 6.

Prove the identities (2.4). 7. 7.

Prove that $\textsf{{B}}_{2}$ is a subalgebra of $\textsf{{\L}}_{3}$. 8. 8.

Show that the law of the excluded middle and Peirce’s law are not tautologous in $\textsf{{\L}}_{3}$. 9. 9.

Prove that the set of $\textsf{{\L}}_{3}$-tautologies is properly included in the set of classical tautologies. 10. 10.

Prove that the “paradoxes of material implications” (p. 2.3) are $\textsf{{\L}}_{3}$-tautologous. 11. 11.

Show that the following formulas are $\textsf{{\L}}_{3}$-tautologies.

[TABLE] 12. 12.

Prove that the identities (2.5) hold the algebra $\textsf{{\L}}_{3}$ expanded by the modalities $\Box$ and $\Diamond$. 13. 13.

Show that the logical matrix of type $\mathcal{L}_{C}$ of Section 2.2.3 validates the formulas $\Box p\rightarrow p,\leavevmode\nobreak\ p\rightarrow\Diamond p\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\ \Box p\rightarrow\Diamond p$ and rejects their converses $p\rightarrow\Box p,\leavevmode\nobreak\ \Diamond p\rightarrow p\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\ \Diamond p\rightarrow\Box p$. 14. 14.

Show that Peirce’s law, the double negation law and both De Morgan’s laws can be refuted in $\textsf{{G}}_{3}$. 15. 15.

Let us designate on the algebra $\textsf{{G}}_{3}$ the logical filter $\{\bm{\tau},\mathbf{1}\}$. We denote the new matrix by $\textsf{{G}}_{3}^{\prime}$. Show that $\textsf{{G}}_{3}^{\prime}$ validates a formula $\alpha$ if and only if $\alpha$ is a classical tautology.

2.3 Historical notes

The idea that logic, as the science of reasoning, deals with the universal rather than the particular can be traced back to Plato and Aristotle. According to the Platonic doctrine of Forms, a single Form is associated with each group of things to which a common name can be applied. Plato believed that each Form differs from the particulars it represents but, at the same time, is a particular of its own kind. Applying this doctrine to reasoning, he believed that correct reasoning is based on the connections of the involved Forms. This is how W. Kneale and M. Kneale summarize Plato’s view on reasoning.

“For Plato necessary connexions hold between Forms, and inference is presumably valid when we follow in thought the connexions between Forms as they are. How is this view related to the theory which assigns truth and falsity to sentences made up of nouns and verbs? Plato seems to hold that a sentence is true if the arrangement of its parts reflects or corresponds to connexion between Forms.” ([KK62], section I.5.)

However, what Plato wrote about correct thinking can be regarded as philosophy of logic rather than logic itself. The first construction of formal logic we encounter in Aristotle. Although Aristotle was influenced by Plato’s doctrine of Forms, he rejected it. Nevertheless, we dare to assert that Aristotle’s doctrine of the syllogism is formal in the Platonic sense. Namely Aristotle was the first to introduce variables into logic. In his influential book on Aristotle’s syllogistic J. Łukasiewicz makes the following comment about this fact.

“It seems that Aristotle regarded his invention as entirely plain and requiring no explanation, for there is nowhere in his logical works any mention of variables. It was Alexander who first said explicitly that Aristotle presents his doctrine in letters, ςτοιχει̂α, in order to show that we get the conclusion not in consequence of the matter of the premisses, but in consequence of their form and combination; the letters are marks of universality and show that such a conclusion will follow always and for any term we may choose.” ([Łuk57], § 4.)

Although in the course of the development of logic, when after Aristotle the generalized nature of formal judgments was reflected in the use of letters, and the latter were perceived, at least gradually, as sentential variables, and therefore it would be natural to consider the uniform substitution, as defined above, as a legitimate operation that would apply to all formal judgments, however, the uniform substitution was first proposed as an inference rule, that is, only in conjunction with (and for constructing) logical inferences.

Nonetheless, the realization, though implicit and at least for propositional languages such as $\mathcal{L}$-languages above, of that the set of formulas is closed under substitution and that the notion of validity should be defined in such a way to maintain this closedness for the formulas identified as valid one can find in George Boole. As to the first part of this observation, Boole puts it as follows.

“Let us imagine any known or existing language freed from idioms and divested of superfluity and let us express in that language any given proposition in a manner the most simple and literal […] The transition from such a language to the notation of analysis would consist of no more than the substitution of one set of signs for another, without essential change either in form or character.” ([Boo03], chapter 11, section 15.)

As to the second, he writes:

“I shall in some instances modify the premises by […] substitution of some new proposition, and shall determine how by such change the ultimate conclusions are affected.” ([Boo03], chapter 13, section 1.)

It appears that this idea has become fully realized by the 1920s in the Lvov-Warsaw School, for without this, Lindenbaum’s Theorem (Proposition 3.3.4) would be impossible. Although we can only guess, but it seems plausible to suggest that the confusion between the concepts of predicate and propositional term was an obstacle for such a long delay.

With merely some reservation, one can say that George Boole was the first who interpreted symbolic expressions representing “laws of thought” as algebraic terms. However, his algebraic treatment of logic was merely the beginning of a long way. This is how T. Hailperin estimates Boole’s contribution.

“Boole wrote his Laws of Thought before the notion of an abstract formal system, expressed within a precise language, was fully developed. And, at that time, still far in the future was the contemporary view which makes a clear distinction between a formal system and its realization or models. Boole’s work contributed to bringing these ideas to fruition.” ([Hai86], chapter 1, § 1.0.)

We find interpretation of formal judgments in an abstract logical matrix in, namely $\textsf{{B}}_{2}$, Wittgenstein’s Tractatus; cf. [Wit01], 4.441 and further. Also, Wittgenstein used the term tautology, applying it to any classical tautology. Later on, logical matrices turned to be a natural way to define numerous deductive systems. We owe to Alfred Tarski a systematic approach to deductive systems through logical matrices.

At first matrices were employed in the search for an independent axiomatic system for the set of classical tautologies; cf. [Ber26] and [Łuk64], section 6. Also, J. C. C. McKinsey [McK39] used matrices to prove independence of logical connectives in intuitionistic propositional logic.

The idea of the use of a 3-valued matrix was expressed by Jan Łukasiewicz in his inaugural address as Chancellor of the University of Warsaw in 1922. In 1961, a revised version of this speech was published, where one can read:

“I maintain that there are propositions which are neither true nor false but indeterminate. All sentences about future facts which are not yet decided belong to this category. Such sentences are neither true at the present moment, for they have no real correlate, nor are they false, for their denials too have no real correlate. If we make use of philosophical terminology which is not particularly clear, we could say that ontologically there corresponds to these sentences neither being nor non-being but possibility. Indeterminate sentences, which ontologically have possibility as their correlate, take the third truth-value.” ([Łuk70], p. 126.)

Technically, however, Łukasiewicz proposed $\textsf{{\L}}_{3}$ already in 1920; cf. [Łuk20]. In [Łuk30] he expands $\textsf{{\L}}_{3}$ to include modalities and thus obtain the matrix of Section 2.2.3. In fact, he defines only $\Diamond$, but it is easy to check that the definition

[TABLE]

gives operation $\Box$ as introduced in Section 2.2.3 directly.

It is worth noting that Lukasiewicz’s interest in ”multivalued logic” (in the sense of logical matrices having more than two values) was motivated by his interest in modal contexts, and not vice versa. Indeed, he wrote:

“I can assume without contradiction that my presence in Warsaw at a certain moment of next year, e.g. at noon on 21 December, is at the present time determined neither positively nor negatively, Hence it is possible, but not necessary, that I shall be present in Warsaw at the given time. On this assumption the proposition ‘I shall be in Warsaw at noon on 21 December of next year’, can at the present time be neither true nor false. For if it were true now, my future presence in Warsaw would have to be necessary, which is contradictory to the assumption. If it were false now, on the other hand, my future presence in Warsaw would have to be impossible, which is also contradictory to the assumption. Therefore the proposition considered is at the moment neither true nor false and must possess a third value, different from ‘0’ or falsity and ‘1’ or truth. This value we can designate by ‘$\frac{1}{2}$’. It represents ‘the possible’, and joins ‘the true’ and ‘the false’ as a third value.” ([Łuk30], § 6; cf. English translation in [Me67], pp. 40–65.)

The logical matrix $\textbf{L}_{\aleph_{1}}$ and its logic for the first time were discussed by Łukasiewicz in his address delivered at a meeting of the Polish Philosophical Society in Lvov on October 14, 1922. The report of this lecture was published in Ruch Filozoficzny, vol. 7 (1923), no. 6, pp. 92–93; see English translation in [Łuk70], pp. 129–130. According to this report, Łukasiwicz’s motivation for this matrix was as follows.

“The application of this interpretation is twofold: 1) It can be demonstrated that if those verbal rules, or directives, which are accepted by the authors of Principia Mathematica (the rule of deduction and the rule of substitution) are adopted, then no set of the logical laws that have the numerical value 1 can yield any law that would have a lesser numerical value. 2) If 0 is interpreted as falsehood, 1 as truth, and other numbers in the interval 0–1 as the degrees of probability corresponding to various possibilities, a many-valued logic is obtained, which is an expansion of three-valued logic and differs from the latter in certain details.” ([Łuk70], p. 130.)

It is clear that $\textbf{L}_{\aleph_{0}}$ is an obvious simplification of $\textbf{L}_{\aleph_{1}}$.

Answering a question of Hahn, Kurt Gödel considered [Göd32] (see English translation in [Göd86]) an infinite series of finite logical matrices and their logics, where the matrix $\textsf{{B}}_{2}$ was the second and $\textsf{{G}}_{3}$ the third in the series. All these matrices were partially ordered chains with the maximal element designated. Gödel’s goal was twofold: to show that 1) the intuitionistic propositional calculus cannot be determined by a single matrix; and that 2) there are at least countably many logics between the intuitionistic and classical logics. (These logics will be descussed in more detail in Chapter 3.)

The aforementioned series of Gödel’s matrices produces a descending chain of logics all containing the intuitionistic propositional logic. Michael Dummett showed [Dum59] that LC equals the intersection of all Gödel’s logics. He also gave an axiomatization of LC, which will be discussed in Chapter 3.

Chapter 3 Logical Consequence

The conception of logical consequence which we discuss in this chapter can be traced back to Aristotle’s distinction between demonstrative and dialectical argument. The essence of their difference lies in the status of the premises of the argument in question. In a demonstrative argument, its premises are regarded as true. Aristotle called the argument with such premises “didactic” and compared them with what a teacher lays down as a starting point of the development of his subject. We would call such premises the axioms of a theory. In a dialectical argument, according to Aristotle, any assumptions can be employed for premises. More than that, in the reductio ad absurdum argument one starts with a premise which is aimed to be proven false.

Thus, the focus in the dialectical reasoning is transferred on the argument itself. This involves considering such an argumentation as a binary relation between a set of premises and what can be obtained from them in the course of this argumentation. And the first question raised by this point of view is this: What characteristics of the dialectical argument could qualify it as sound?

3.1 Consequence relation

From the outset, we are faced with a choice between two paths each addressing one of the questions: Should consequence relation state determination between a set of premises (which can be empty) and a set of conclusions (which can also be empty), or should it do it between a set of premises (possibly the empty one) and a single formula? In this text, we address the first option. The framework of this option is known as single-conclusion, while that of the second as multiple-conclusion or poly-conclusion consequence relation.

Talking about consequence relation in general, we denote it by “$\vdash$” and equip this sign with subscript when referring to a specific consequence relation.

In the context of consequence relation, we use the following notation:

[TABLE]

for any sets $X,Y,\ldots,Z$ of $\mathcal{L}$-formulas and any $\mathcal{L}$-formulas $\alpha,\ldots,\beta$.

Definition 3.1.1** (single-conclusion consequence relation).**

A relation $\vdash\subseteq\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$ is an $\mathcal{L}$-single-conclusion consequence relation $($or simply an $\mathcal{L}$-consequence relation or just a consequence relation when consideration occurs in a fixed, perhaps unspecified, formal language$)$ if the following conditions are satisfied$\,:$

[TABLE]

for any sets $X$, $Y$ and $Z$ of $\mathcal{L}$-formulas.

In case $Y=\{\beta\}$, the property (c) reads:

[TABLE]

A consequence relation $\vdash$ is called nontrivial if

[TABLE]

otherwise it is trivial.

A consequence relation $\vdash$ is called finitarity if

[TABLE]

where here and on $Y\Subset X$ means that $Y$ is a finite (maybe empty) subset of $X$.

The last notion can be generalized as follows. Let $\kappa$ be an infinite cardinal. A consequence relation $\vdash$ is called $\kappa$-compact if

[TABLE]

Thus finitariness is simply $\aleph_{0}$-compactness.

A consequence relation $\vdash$ is structural if

[TABLE]

for any set $X\cup\{\alpha\}\subseteq\textit{{Fm}}$ and any $\mathcal{L}$-substitution $\sigma$.

We will be using the term sequent for a statement “$X\vdash\alpha$”.

Note on monotonicity of $\vdash$. The property (b) of Definition 3.1.1 characterizes the category of monotone consequence relations as opposed to that of non-monotone consequence relations when the property (b) does not hold. In this book we consider only the first category of consequence relations. (End of note.)

Other, specific, properties in addition to (a)–(c) have been considered in literature. For instance, for the language $\mathcal{L}_{B}$ and its expansions the following property is typical for many consequence relations:

[TABLE]

We will be using indices to distinguish in the same formal language either two different consequence relations or two equal consequence relation that are defined differently. The following three propositions will be used in the sequel.

Proposition 3.1.1**.**

Let $\{\vdash_{i}\}_{i\in I}$ be a family of consequence relations in a language $\mathcal{L}$. Then the relation $\vdash$ defined by $\bigcap_{i\in I}\{\vdash_{i}\}$ is also a consequence relation. Moreover, if each $\vdash_{i}$ is structural, so is $\vdash$. In addition, if $I$ is finite and each $\vdash_{i}$ is finitary, then $\vdash$ is also finitary.

Proof is left to the reader. (See Exercise 3.1.2.)

Given a consequence relation $\vdash$ and a set $X_{0}$ of $\mathcal{L}$-formulas. We define a relation as follows:

[TABLE]

Proposition 3.1.2**.**

For any consequence relation $\vdash$ and arbitrary fixed set $X_{0}$, $\vdash_{X_{0}}$ is a consequence relation such that

[TABLE]

Proof is left to the reader. (Exercise 3.1.3)

For any consequence relation $\vdash$, we define:

[TABLE]

Proposition 3.1.3**.**

Let $\vdash$ be a consequence relation. Then $\vdash^{\circ}$ is also a consequence relation. In addition, if $\vdash$ is structural, $\vdash^{\circ}$ is also structural; further, if $\vdash$ is $\kappa$-compact, so is $\vdash^{\circ}$.

Proof is left to the reader. (Exercise 3.1.4)

As is seen from the Proposition 3.1.1, Definition 3.1.1 is essentially extensional, because it does not show how the transition from premises to conclusion can be carried out. However, before addressing this issue, we will discuss how the concept of single-conclusion consequence relation can be represented purely in terms of sets of $\mathcal{L}$-formulas.

Exercises 3.1

Consider the properties (a), (b) and (c) of Definition 3.1.1. Show that (a) and (c) imply (b). 2. 2.

Prove Proposition 3.1.1. 3. 3.

Prove Proposition 3.1.2. 4. 4.

Prove Proposition 3.1.3.

3.2 Consequence operator

Let $\vdash$ be a consequence relation for $\mathcal{L}$-formulas. Then, we define:

[TABLE]

for any set $X$ of $\mathcal{L}$-formulas. We observe the following connection:

[TABLE]

The last equivalence induces the following definition.

Definition 3.2.1**.**

A map $\textbf{Cn}:\mathcal{P}(\textit{{Fm}})\longrightarrow\mathcal{P}(\textit{{Fm}})$ is called a consequence operator if it satisfies the following three conditions:

[TABLE]

for any sets $X$ and $Y$ of $\mathcal{L}$-formulas.

A consequence operator Cn is called finitary (or compact) if

[TABLE]

As in case of consequence relation, we generalize the last notion for any infinite cardinal $\kappa$: an consequence operator Cn is $\kappa$-compact if

[TABLE]

And a consequence operator Cn is called structural, if for any set $X$ and any substitution $\sigma$,

[TABLE]

Note on monotonicity of Cn. A consequence operator as defined in Definition 3.2.1 is called monotone as opposed to non-monotone consequence operators. (End of note.)

A set $X$ of formulas is called closed, or is a theory, (w.r.t. Cn) if $X=\textbf{Cn}(X)$. This, in view of $(\text{a}^{{\dagger}})$ and $(\text{c}^{{\dagger}})$, any set $\textbf{Cn}(X)$ is a theory; we call it the theory generated by $X$ (w.r.t. Cn).

We observe the following.

Proposition 3.2.1**.**

Given a consequence operator Cn, any set $\bigcap_{i\in I}\{\textbf{Cn}(X_{i})\}$ is closed.

Proof is left to the reader. (See Exercise 3.2.1.) Compare this proposition with Proposition 3.1.1.

The next proposition establishes connection between the notion of consequence relation and that of consequence operator.

Proposition 3.2.2**.**

Let $\vdash$ be a consequence relation. The operator Cn defined by (3.2) is a consequence operator. Conversely, for a given consequence operator Cn, the corresponding relation defined by (3.3) is a consequence relation. Moreover, Cn is finitary ($$\kappa-compact$)$ if, and only if, so is $\vdash$. In addition, Cn is structural if, and only if, so is $\vdash$.

Proof can be obtained by routine check and is left to the reader. (See Exercise 3.2.2.)

Proposition 3.2.2 allows us to use the notion of consequence relation and that of consequence operator interchangeably.

The next observation confirms the last remark; it just mirrors Proposition 3.1.1

Proposition 3.2.3**.**

Let $\{\textbf{Cn}_{i}\}_{i\in I}$ be a family of consequence operators in a language $\mathcal{L}$. Then the operator Cn defined by the equality

[TABLE]

is also a consequence operator. Moreover, if each $\textbf{Cn}_{i}$ is structural, so is Cn. In addition, if $I$ is finite and each $\textbf{Cn}_{i}$ is finitary, then Cn is also finitary.

Proof is left to the reader. (Exercise 3.2.5)

Besides the properties $(\text{a}^{{\dagger}})$–$(\text{c}^{{\dagger}})$, finitariness and $\kappa$-compactness, other properties of a map $\textbf{Cn}:\mathcal{P}(\textit{{Fm}})\longrightarrow\mathcal{P}(\textit{{Fm}})$ related to logical consequence have been considered in literature. These are some of them.

[TABLE]

Proposition 3.2.4**.**

Let Cn be a map from $\mathcal{P}(\textit{{Fm}})$ into $\mathcal{P}(\textit{{Fm}})$, Then the following implications hold$\,:$

[TABLE]

Proof.

We prove $(vi)$, $(xi)$ and $(xii)$, in this order, and leave the rest to the reader. (See Exercise 3.2.6.)

Suppose $X\subseteq\textbf{Cn}(Y)$, Then, by virtue of $(\text{a}^{\dagger})$, $X\cup Y\subseteq\textbf{Cn}(Y)$. According to $(\text{b}^{\dagger})$ and $(\text{c}^{\dagger})$, we have: $\textbf{Cn}(X\cup Y)\subseteq\textbf{Cn}(\textbf{Cn}(Y))\subseteq\textbf{Cn}(Y)$.

To prove $(xi)$, we assume that $\alpha\notin\textbf{Cn}(X)$, for some set $X$.

Let us denote

[TABLE]

We aim to show that $C_{\alpha}$ contains a maximal set.

First, we observe that $C_{\alpha}$ is nonempty, for $X\in C_{\alpha}$. Regarding $C_{\alpha}$ as a partially ordered set with respect to $\subseteq$, we consider a chain $\{Y_{i}\}_{i\in I}$ in $C_{\alpha}$. That is, either $Y_{i}\subseteq Y_{j}$ or $Y_{i}\subseteq Y_{j}$, and $\alpha\notin Y_{i}$, for any $i\in I$. Next we denote

[TABLE]

We aim to show that $\alpha\notin\textbf{Cn}(Y_{0})$. For contradiction, assume that $\alpha\in\textbf{Cn}(Y_{0})$. Then, by $(\text{d}^{{\dagger}})$, there is a set $Y^{\prime}\Subset Y_{0}$ such that $\alpha\in\textbf{Cn}(Y^{\prime})$. We note that $Y^{\prime}\neq\emptyset$, for otherwise, by $(\text{b}^{{\dagger}})$, we would have that $\alpha\in\textbf{Cn}(X)$. Since $Y^{\prime}$ is finite, there is ${i_{0}}\in I$ such that $Y^{\prime}\subseteq Y_{i_{0}}$. Then, by virtue of $(\text{b}^{{\dagger}})$, $\alpha\in\textbf{Cn}(Y_{i_{0}})$. We have obtained a contradiction. Thus $C_{\alpha}$ satisfies the conditions of Zorn’s lemma, according to which $C_{\alpha}$ contains a maximal set.

Finally, to prove ($xii$), we assume that $X\subseteq Y$ and $\alpha\in\textbf{Cn}(X)$. In virtue of $(\text{d}^{\dagger})$, there is a finite $Y^{\prime}\subseteq X$ such that $\alpha\in\textbf{Cn}(Y^{\prime})$. We note that, by premise, $Y^{\prime}\Subset Y$. Then, by $(\text{h}^{\dagger})$, $\alpha\in\textbf{Cn}(Y)$. ∎

Exercises 3.2

Prove Proposition 3.2.1. 2. 2.

Prove Proposition 3.2.2. 3. 3.

Prove that a consequence operator Cn is structural if, and only if, $\textbf{Cn}(\sigma(\textbf{Cn}(X)))=\textbf{Cn}(\sigma(X))$, for any set $X$ and any substitution $\sigma$. 4. 4.

Let Cn be a structural operator. Prove that a set $\sigma(\textbf{Cn}(X))$ is closed (or is a theory) if, and only if, $\sigma(\textbf{Cn}(X))=\textbf{Cn}(\sigma(X))$, for any set $X$ and any substitution $\sigma$. 5. 5.

Prove Proposition 3.2.3. 6. 6.

Complete the proof of Proposition 3.2.4.

3.3 Defining consequence relation

In order to distinguish consequence relations or consequence operators we will be using the symbols $\vdash$ and Cn with subscripts. Quite often, we employ a letter ‘$\mathcal{S}$’, calling a consequence relation $\vdash_{\mathcal{S}}$ and the corresponding consequence operator $\textbf{Cn}_{\mathcal{S}}$ an abstract logic $\mathcal{S}$. Thus, given an abstract logic $\mathcal{S}$, for any sets $X$ of $\mathcal{L}$-formulas and any $\mathcal{L}$-formula $\alpha$, we have:

[TABLE]

Further, we denote

[TABLE]

and call the elements of the latter set theorems, or theses, of $\mathcal{S}$, or simply $\mathcal{S}$-theorems, or $\mathcal{S}$-theses. Any set $\textbf{Cn}_{\mathcal{S}}(X)$ is call the $\mathcal{S}$-theory generated by a set $X$. Thus $\bm{T}_{\mathcal{S}}$ is the least $\mathcal{S}$-theory with respect to $\subseteq$.

A set $X$, as well as the theory $\textbf{Cn}_{\mathcal{S}}(X)$, is called inconsistent (relative to $\mathcal{S}$) if $\textbf{Cn}_{\mathcal{S}}(X)=\textit{{Fm}}$; otherwise both are consistent. An abstract logic $\mathcal{S}$ is trivial if $\vdash_{\mathcal{S}}$ is trivial, and otherwise is nontrivial. We observe that any structural $\mathcal{S}$ is trivial if, and only if, for any arbitrary variable $p$, $p\in\textbf{Cn}_{\mathcal{S}}(\emptyset)$. (Exercise 3.3.1) We note that for any nontrivial abstract logic $\mathcal{S}$, $\bm{T}_{\mathcal{S}}\subset\textit{{Fm}}$. (Exercise 3.3.2) ) We also note that a theory is not required to be closed under substitution. A bit more we can say about substitution in the structural abstract logics: every theory of a structural abstract logic is closed under substitution if, and only if, this theory is generated by a set itself closed under substitution. (Exercise 3.3.3)

We denote

[TABLE]

and

[TABLE]

3.3.1 Consequence operator (relation) via a closure system

A set $\mathcal{A}\subseteq\mathcal{P}(\textit{{Fm}})$ which contains Fm and is closed under any nonempty intersections in $\mathcal{P}(\textit{{Fm}})$ is called a closure system over Fm. That is, for any closure system $\mathcal{A}$, $\textit{{Fm}}\in\mathcal{A}$ and for any $I\neq\emptyset$,

[TABLE]

All operators in this subsection are considered over a fixed language $\mathcal{L}$.

Proposition 3.3.1**.**

Let $\mathcal{A}$ be a closure system. Then the operator

[TABLE]

is a consequence operator and $\mathcal{A}=\{X\leavevmode\nobreak\ |\leavevmode\nobreak\ X=\textbf{Cn}_{\mathcal{A}}(X)\}$. Conversely, if Cn is a consequence operator and $\mathcal{A}_{\textbf{Cn}}$ is the family of its closed sets, then $\textbf{Cn}=\textbf{Cn}_{\mathcal{A}_{\textbf{Cn}}}$.

Proof.

Assume that $\mathcal{A}$ is a closure system. It is easy to check that the operator $\textbf{Cn}_{\mathcal{A}}$ satisfies the properties $(\text{a}^{{\dagger}})$ and $(\text{b}^{{\dagger}})$ of Definition 3.2.1. We prove that it also satisfies $(\text{c}^{{\dagger}})$. For this, given a set $X$, we denote

[TABLE]

and suppose that $\alpha\in\textbf{Cn}_{\mathcal{A}}(X_{0})$. Aiming to show that $\alpha\in X_{0}$, we note that

[TABLE]

Thus, we assume that $X\subseteq Y$, for an arbitrary $Y\in\mathcal{A}$. In virtue of $(\text{b}^{\dagger})$, $X_{0}\subseteq\textbf{Cn}_{\mathcal{A}}(Y)$ and hence $\textbf{Cn}(X_{0})\subseteq Y$, for $Y\in\mathcal{A}$. This implies that $\alpha\in Y$ and, using the equivalence above, we obtain that $\alpha\in X_{0}$.

Finally, one can easily observe that

[TABLE]

Conversely, suppose Cn is a consequence operator and

[TABLE]

Assume that $\{X_{i}\}_{i\in I}\subseteq\mathcal{A}_{\textbf{Cn}}$ and denote

[TABLE]

Since $X_{0}\subseteq X_{i}$, for each $i\in I$, $\textbf{Cn}(X_{0})\subseteq\textbf{Cn}(X_{i})=X_{i}$, also for each $i\in I$. Hence $\textbf{Cn}(X_{0})\subseteq X_{0}$, that is $X_{0}\in\mathcal{A}_{\textbf{Cn}}$.

Finally, we show that for any formula $\alpha$ and any set $X$ of formulas,

[TABLE]

First, we notice that

[TABLE]

Then, in virtue of $(\ast)$, we have:

[TABLE]

Now we suppose that $\alpha\in\textbf{Cn}(X)$, $X\subseteq Y$ and $\textbf{Cn}(Y)=Y$. From the second premise, we derive that $\textbf{Cn}(X)\subseteq\textbf{Cn}(Y)$ and hence $\textbf{Cn}(X)\subseteq Y$. Thus $\alpha\in Y$. Since $Y$ is an arbitrary set satisfying the aforementioned conditions, using $(\ast)$, we conclude that $\alpha\in\textbf{Cn}_{\mathcal{A}_{\textbf{Cn}}}(X)$. ∎

Given an abstract logic $\mathcal{S}$, we remind the notation:

[TABLE]

We conclude with the following observation.

Proposition 3.3.2** (Brown-Suszko theorem).**

An abstract logic $\mathcal{S}$ in a language $\mathcal{L}$ is structural if, and only if, for any set $X\subseteq\textit{{Fm}}$ and any substitution $\sigma$, the following holds:

[TABLE]

Proof.

Suppose $\mathcal{S}$ is structural. Let $\sigma$ be a substitution and $X\in\Sigma_{\mathcal{S}}$. Assume that $\sigma^{-1}(X)\vdash_{\mathcal{S}}\alpha$. Since $\mathcal{S}$ is structural, we have: $\sigma(\sigma^{-1}(X))\vdash_{\mathcal{S}}\sigma(\alpha)$. In virtue of (2.0–$i$), $X\vdash_{\mathcal{S}}\sigma(\alpha)$, that is $\sigma(\alpha)\in X$. This means that $\alpha\in\sigma^{-1}(X)$.

To prove the converse, we assume that the conditional above holds. Then we, with help of (2.0–$ii$), obtain that $X\subseteq\sigma^{-1}(\sigma(X))\subseteq\sigma^{-1}(\textbf{Cn}_{\mathcal{S}}(\sigma(X)))$. This implies that $\textbf{Cn}_{\mathcal{S}}(X)\subseteq\textbf{Cn}_{\mathcal{S}}(\sigma^{-1}(\textbf{Cn}_{\mathcal{S}}(\sigma(X))))$. Applying the assumption, we get that $\textbf{Cn}_{\mathcal{S}}(X)\subseteq\sigma^{-1}(\textbf{Cn}_{\mathcal{S}}(\sigma(X)))$. Thus, if $X\vdash_{\mathcal{S}}\alpha$, that is $\alpha\in\textbf{Cn}_{\mathcal{S}}(X)$, then $\alpha\in\sigma^{-1}(\textbf{Cn}_{\mathcal{S}}(\sigma(X)))$, that is $\sigma(X)\vdash_{\mathcal{S}}\sigma(\alpha)$. ∎

3.3.2 Consequence relation via logical matrices

Given a (logical) matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$, we define a relation $\models_{\textbf{M}}$ on $\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$ as follows:

[TABLE]

where

[TABLE]

Let $\mathcal{M}$ be a nonempty class of matrices. We define the relation of matrix consequence (w.r.t. a class $\mathcal{M}$) as follows:

[TABLE]

Accordingly, the relation $\models_{\textbf{M}}$ is called a single-matrix consequence, or M-consequence for short. If a class $\mathcal{M}$ is known, we call a matrix consequence associated with a class $\mathcal{M}$ an $\mathcal{M}$-consequence. Given a nonempty set of matrices $\mathcal{M}$, we denote the $\mathcal{M}$-consequence by $\mathcal{S}_{\mathcal{M}}$ and say that an abstract logic $\mathcal{S}$ is determined by $\mathcal{M}$ if $\mathcal{S}=\mathcal{S}_{\mathcal{M}}$.

The justification for the terminology ‘$\mathcal{M}$-consequence’ and ‘M-consequence’ is the following.

Proposition 3.3.3**.**

Any matrix consequence is a structural consequence relation.

Proof.

Let $\mathcal{M}=\{\textbf{M}_{i}\}_{i\in I}$ be a nonempty set of matrices. We have to check that the conditions (a)–(c) of Definition 3.1.1 are satisfied for the relation $\models_{\mathcal{M}}$. In addition, we have to show that this consequence relation is structural. We leave this routine check to the reader. (Exercise 3.3.4) ∎

Let $\mathcal{S}$ be an abstract logic and $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be a matrix. Accordingly, we have the consequence relation $\vdash_{\mathcal{S}}$ and a single-matrix consequence $\models_{\textbf{M}}$. If $\vdash_{\mathcal{S}}\subseteq\models_{\textbf{M}}$, we call the filter $D$ an $\mathcal{S}$-filter, in which case the matrix M is called an $\mathcal{S}$-matrix (or an $\mathcal{S}$-model).

Definition 3.3.1** (Lindenbaum matrix).**

Let $\mathcal{S}$ be a structural abstract logic and $D_{\mathcal{S}}$ be an $\mathcal{S}$-theory. The matrix $\langle\mathfrak{F}_{\mathcal{L}},D_{\mathcal{S}}\rangle$ is called a Lindenbaum matrix $($relative to \mathcal{S}$$). For an arbitrary $X\subseteq\textit{{Fm}}$, we denote:

[TABLE]

and

[TABLE]

The reader is advised to remember that (Proposition 2.2.2)

any $\mathcal{L}$-substitution is a valuation in $\mathfrak{F}_{\mathcal{L}}$ and vice versa.

Proposition 3.3.4** (Lindenbaum’s theorem).**

Let $\mathcal{S}$ be a structural abstract logic. Then $\textsf{{Lin}}_{\,\mathcal{S}}$ is an $\mathcal{S}$-model. Also, if a set $X\subseteq\textit{{Fm}}$ is closed under arbitrary $\mathcal{L}$-substitution, then for any $\mathcal{L}$-formula $\alpha$,

[TABLE]

in particular,

[TABLE]

Proof.

Let us take any set $X\cup\{\alpha\}\subseteq\textit{{Fm}}$ such that $X\vdash_{\mathcal{S}}\alpha$. Then, for an arbitrary $\mathcal{L}$-substitution $\sigma$, $\sigma(X)\vdash_{\mathcal{S}}\sigma(\alpha)$. Therefore, if $\sigma(X)\subseteq\textbf{Cn}_{\mathcal{S}}(\emptyset)$, then $\sigma(\alpha)\in\textbf{Cn}_{\mathcal{S}}(\emptyset)$. Thus $\textsf{{Lin}}_{\,\mathcal{S}}$ is an $\mathcal{S}$-model.

Now, if, in addition, $\sigma(X)\subseteq X$, then $\sigma(\alpha)\in\textbf{Cn}_{\mathcal{S}}(X)$. Since $\sigma$ is an arbitrary $\mathcal{L}$-substitution, we have that $\models_{\textsf{{Lin}}_{\,\mathcal{S}}[X]}\alpha$.

Conversely, if $\models_{\textsf{{Lin}}_{\,\mathcal{S}}[X]}\alpha$, then, in particular, $\iota(\alpha)\in\textbf{Cn}_{\mathcal{S}}(X)$, that is $X\vdash_{\mathcal{S}}\alpha$.

The second equivalence is a specification of the first. ∎

We say that a matrix is weakly adequate for an abstract logic $\mathcal{S}$ if this matrix validates all $\mathcal{S}$-theorems and only them. Thus, by virtue of the last equivalence of Proposition 3.3.4, we obtain the following.

Corollary 3.3.4.1**.**

Let $\mathcal{S}$ be structural abstract logic. Then any Lindenbaum matrix relative to $\mathcal{S}$ is an $\mathcal{S}$-model. Moreover, $\textsf{{Lin}}_{\,\mathcal{S}}$ is weakly adequate for $\mathcal{S}$.

Proof is left to the reader. (Exercise 3.3.5)

Proposition 3.3.4 can be generalized as follows.

Proposition 3.3.5**.**

Given a structural abstract logic $\mathcal{S}$, let $\mathcal{M}_{\mathcal{S}}$ be the set of all Lindenbaum matrices relative to $\mathcal{S}$. Then $\vdash_{\mathcal{S}}\,=\,\models_{\mathcal{M}_{\mathcal{S}}}$; that is for any set $X$ of formulas and any formula $\alpha$,

[TABLE]

Proof.

First we suppose that $X\vdash_{\mathcal{S}}\alpha$. Let us take any $\langle\mathfrak{F}_{\mathcal{L}},D_{\mathcal{S}}\rangle$. Assume that for some substitution $\sigma$, $\sigma(X)\subseteq D_{\mathcal{S}}$. Since $\mathcal{S}$ is structural, $\sigma(X)\vdash_{\mathcal{S}}\sigma(\alpha)$. This implies that $\sigma(\alpha)\in\textbf{Cn}_{\mathcal{S}}(\sigma(X))$ and hence $\sigma(\alpha)\in D_{\mathcal{S}}$.

Conversely, assume that $X\not\vdash_{\mathcal{S}}\alpha$. This means (see (3.3)) that $\alpha\notin\textbf{Cn}_{\mathcal{S}}(X)$. Let us denote $\textbf{M}:=\langle\mathfrak{F}_{\mathcal{L}},\textbf{Cn}_{\mathcal{S}}(X)\rangle$ and take the identity substitution $\iota$. It is obvious that $\iota(X)\subseteq\textbf{Cn}_{\mathcal{S}}(X)$ but $\iota(\alpha)\notin\textbf{Cn}_{\mathcal{S}}(X)$; that is $X\not\models_{\textbf{M}}\alpha$. ∎

The last proposition inspires us for the following (complex) definition.

Definition 3.3.2**.**

A $($nonempty$)$ family $\mathcal{B}=\{\langle\textsf{{A}}_{i},D_{i}\rangle\}_{i\in I}$ of matrices of type $\mathcal{L}$ is called a bundle if for any $i,j\in I$, the algebras $\textsf{{A}}_{i}$ and $\textsf{{A}}_{j}$ are isomorphic. A pair $\langle\textsf{{A}},\{D_{i}\}_{i\in I}\rangle$, where each $D_{i}$ is a logical filter in $($or of$)$ A, is called an atlas. By definition, the matrix consequence relative to an atlas $\langle\textsf{{A}},\{D_{i}\}_{i\in I}\rangle$ is the same as the matrix consequence related the bundle $\{\langle\textsf{{A}},D_{i}\rangle\}_{i\in I}$, which in turn is defined in the sense of (3.3). Given an abstract logic $\mathcal{S}$, the bundle $\{\langle\mathfrak{F}_{\mathcal{L}},D\rangle\}_{D\in\Sigma_{\mathcal{S}}}$, where $\Sigma_{\mathcal{S}}$ is the set of all $\mathcal{S}$-theories, is called the Lindenbaum bundle relative to $\mathcal{S}$ and the atlas $\textsf{{Lin}}[\Sigma_{\mathcal{S}}]:=\langle\mathfrak{F}_{\mathcal{L}},\Sigma_{\mathcal{S}}\rangle$, is called the Lindenbaum atlas relative to $\mathcal{S}$.

We say that a given matrix (bundle or atlas) is adequate for an abstract logic $\mathcal{S}$ if $\vdash_{\mathcal{S}}$ and the corresponding matrix relation coincide.

We denote:

[TABLE]

for any $X\cup\{\alpha\}\subseteq\textit{{Fm}}$.

Thus we conclude with the following.

Corollary 3.3.5.1**.**

The Lindenbaum atlas relative to a structural abstract logic is adequate for this logic. That is, for any $X\cup\{\alpha\}\subseteq\textit{{Fm}}$,

[TABLE]

Proof is left to the reader. (Exercise 3.3.6)

Corollary 3.3.5.2**.**

Let $\mathcal{S}$ be a structural abstract logic and $\mathcal{M}$ be the set of all $\mathcal{S}$-models. Then $\mathcal{S}=\mathcal{S}_{\mathcal{M}}$.

Proof is left to the reader. (Exercise 3.3.7)

3.3.3 Consequence relation via inference rules

Since we perceive the sentential formulas as forms of judgments (Section 2.1), our understanding of a rule of inference, at least in one important case, will be a relation in the class of forms of formulas. As in the first event, where substitution plays a key role in seeing any sentential formula as an abstract representation of infinitely many judgments, it will play a similar role in the concept of inference rule, at least in this important class of inference rules. It is a way, by which we create an abstraction of infinitely many instances of one element that falls under the name of structural inference rule.

An inference rule is a set $R\subseteq\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$. An inference rule receives its significance, when it is a subset of some consequence relation, say $\vdash$. We say that a rule $R$ is sound w.r.t. $\vdash$ if for any $\langle\Gamma,\alpha\rangle\in R$, $\Gamma\vdash\alpha$.

Let $\mathcal{R}$ be a set of inference rules. Taking into account that $\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$ is the trivial consequence relation (relative to a language $\mathcal{L}$), we define

[TABLE]

(We note that the right-hand set is nonempty.)

It is not difficult to see that $\vdash_{[\mathcal{R}]}$ is a consequence relation. (Exercise 3.3.8) We say that an abstract logic $\mathcal{S}$ is determined by a set $\mathcal{R}$ of inference rules if $\vdash_{\mathcal{S}}\,=\,\vdash_{[\mathcal{R}]}$. Given an abstract logic $\mathcal{S}$, one can treat the consequence relation $\vdash_{\mathcal{S}}$ as an inference rule that determines $\mathcal{S}$.

Now we turn to structural rules.

Let us consider a pair $\langle\Gamma,\phi\rangle\in\mathcal{P}(\textit{{Mf}}_{\mathcal{L}})\times\textit{{Mf}}_{\mathcal{L}}$. We call the set

[TABLE]

a structural rule (in $\mathcal{L}$) with the premises $\Gamma$ and conclusion $\phi$. Each pair $\langle\bm{\sigma}(\Gamma),\bm{\sigma}(\phi)\rangle$ is an instance of the rule $R_{\langle\Gamma,\phi\rangle}$ (with the premises $\bm{\sigma}(\Gamma)$ and conclusion $\bm{\sigma}(\phi)$). It is convenient (and we follow this practice) to identify the rule $R_{\langle\Gamma,\phi\rangle}$ with its label $\langle\Gamma,\phi\rangle$, using them interchangeably. It is customary to write a structural rule $\langle\Gamma,\phi\rangle$ in the forms $\Gamma/\phi$ or $\frac{\Gamma}{\phi}$. (It is customary to omit the set-builder notation “$\{\ldots\}$”, when a set of premises is finite, and leave the space blank if $\Gamma=\emptyset$.)

Given an abstract logic $\mathcal{S}$, specifically, a structural rule $\langle\Gamma,\phi\rangle$ is sound w.r.t. $\mathcal{S}$ if for any instantiation $\bm{\sigma}$, $\bm{\sigma}(\Gamma)\vdash_{\mathcal{S}}\bm{\sigma}(\phi)$.

A structural rule is called finitary (or a modus or modus rule) if $\Gamma\Subset\textit{{Mf}}_{\mathcal{L}}$. If an abstract logic $\mathcal{S}$ is determined by a finite set of modus rules, one says that set of modus rules is a calculus for $\mathcal{S}$. An abstract logic may be defined by more than one calculus, if any. An example of a modus rule is modus ponens which is the rule $\bm{\alpha},\bm{\alpha}\rightarrow\bm{\beta}/\bm{\beta}$.

Not all useful inference rules are structural.

Let $\sigma$ be a fixed $\mathcal{L}$-substitution. Then we define

[TABLE]

Then the rule of substitution is the set

[TABLE]

Each $\langle\alpha,\sigma(\alpha)\rangle$ is called an application of the substitution $\sigma$ to $\alpha$. A customary utterance is: $\sigma(\alpha)$ is obtained from $\alpha$ by substitution $\sigma$.

Although substitution is an important component of any structural rule (see Proposition 2.1.2), the rule of substitution itself is not structural, providing that $\mathcal{L}$ contains sentential connectives.

Indeed, for contradiction, we assume that

[TABLE]

for some $\Gamma\cup\{\phi\}\subseteq\textit{{Mf}}_{\mathcal{L}}$. Let us fix an arbitrary $p\in\mathcal{V}_{\mathcal{L}}$. By definition, it is clear that for any $\alpha\in\textit{{Fm}}$, $\langle\{p\},\alpha\rangle\in R_{\text{sub}}$. This implies that for any $\alpha\in\textit{{Fm}}$, there is an instantiation $\bm{\xi}_{\alpha}$ such that $\bm{\xi}_{\alpha}(\Gamma)=\{p\}$ and $\bm{\xi}_{\alpha}(\phi)=\alpha$. Thus, we conclude that $\Gamma\cup\{\phi\}\subseteq\textit{{Mv}}_{\mathcal{L}}$ and $\Gamma\cap\{\phi\}=\emptyset$; moreover, it must be clear that $\Gamma$ cannot have more than one metavariables, because if it were otherwise, the claim $\langle\{p\},\alpha\rangle\in R_{\langle\Gamma,\phi\rangle}$ would not be true. Thus, $\langle\Gamma,\phi\rangle=\langle\{\gamma\},\beta\rangle$, for two distinct metavariables $\gamma$ and $\beta$. Then, providing that $\mathcal{L}$ contains sentential connectives, there is an instantiation $\bm{\xi}$ such that the degree of $\bm{\xi}(\gamma)$ is greater than the degree of $\bm{\xi}(\beta)$. A contradiction.

We will not discuss here non-structural rules, except substitution.111However, we note that the hyperrules introduced below, strictly speaking, are also not structural.

Proposition 3.3.6**.**

Let $\mathcal{S}$ be a structural abstract logic in $\mathcal{L}$. Then there is a set of structural rules that determines $\mathcal{S}$.

Proof.

Since $\textit{card}(\mathcal{V}_{\mathcal{L}})\leq\textit{card}(\textit{{Mv}}_{\mathcal{L}})$, there is a one-one map $\mathcal{V}_{\mathcal{L}}\longrightarrow\textit{{Mv}}_{\mathcal{L}}$ which can, obviously, be extended to $f:\mathfrak{F}_{\mathcal{L}}\longrightarrow\mathfrak{M}_{\mathcal{L}}$. (We employ the same notation for both maps.)

Next, we define:

[TABLE]

It must be clear that any rule $R\in\mathcal{R}$ is structural. And if $R=\langle f(X),f(\alpha)\rangle$, then there is an instantiation $\bm{\xi_{0}}$ such that $\bm{\xi_{0}}(f(X))=X$ and $\bm{\xi_{0}}(f(\alpha))=\alpha$. This implies that any rule $R\in\mathcal{R}$ is sound w.r.t. $\mathcal{S}$. Hence $\vdash_{[\mathcal{R}]}\subseteq\vdash_{\mathcal{S}}$.

Now we assume that any rule $R\in\mathcal{R}$ is sound w.r.t. some $\mathcal{S}^{\prime}$. Suppose $X\vdash_{\mathcal{S}}\alpha$. Then $\langle f(X),f(\alpha)\rangle\in\mathcal{R}$. Therefore, for any instantiation $\bm{\eta}$, $\bm{\eta}(f(X))\vdash_{\mathcal{S}^{\prime}}\bm{\eta}(f(\alpha))$. In particular, $\bm{\xi_{0}}(f(X))\vdash_{\mathcal{S}^{\prime}}\bm{\xi_{0}}(f(\alpha))$. Hence $X\vdash_{\mathcal{S}^{\prime}}\alpha$. ∎

For defining consequence relations, especially structural consequence relations, sometimes even more powerful machinery is convenient. We mean the use of hyperrules.

An (n+1)-tuple

[TABLE]

where $\Gamma_{1}\cup\ldots\cup\Gamma_{n}\cup\Delta\cup\{\phi_{1},\ldots\phi_{n},\psi\}\subseteq\textit{{Mf}}_{\mathcal{L}}$, is called a (structural) hyperrule.

A hyperrule $\Theta$ is sound w.r.t. an abstract logic $\mathcal{S}$ if for any $\mathcal{L}$-instantiation $\bm{\xi}$ and any set $X\subseteq\textit{{Fm}}$,

[TABLE]

If a hyperrule $\Theta$ is employed in relation to an abstract logic $\mathcal{S}$, it is customary to write this hyperrule in the following form:

[TABLE]

Next, using rules and hyperrules (not all of them for each example but selectively), we define several consequence relations in language $\mathcal{L}_{A}$ (Section 2.1) and discuss their properties.

Inference rules:

[TABLE]

Hyperrules:

[TABLE]

where $\vdash$ in the hyperrules above denotes a fixed binary relation on $\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$.

First we define a relation $\vdash_{1}$ on $\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$ and then prove that it is a consequence relation. Then, we do the same for relations $\vdash_{2}$ and $\vdash_{3}$. In all three definitions, we use the concept of (formal) derivation (or formal proof). The relations being defined are written as $X\vdash_{i}\alpha$, where $i=1,2,3$. (For convenience we call $X\vdash_{i}\alpha$ a sequent, even when we may not know yet that $\vdash_{i}$ is a consequent relation.) If $X\vdash_{i}\alpha$ is justified according to the clauses below, we say that $X$* derives $\alpha$, or $\alpha$ is derivable from $X$* (all w.r.t. $\vdash_{i}$). It is for such a justification we use the notion of derivation.

Relation $\vdash_{1}$

Given a set $X$ of $\mathcal{L}_{A}$-formulas and an $\mathcal{L}_{A}$-formula $\alpha$, derivation confirming (or establishing or justifying) a sequent $X\vdash_{1}\alpha$ is a finite (nonempty) list of $\mathcal{L}_{A}$-formulas

[TABLE]

such that

[TABLE]

It is easy to see that $\vdash_{1}$ satisfies the properties (a)–(c) of Definition 3.1.1 and thus is a consequence relation. Moreover, this relation is obviously finitary and structural. One peculiarity of it is that the set of the theses of this relation is empty. Another property of $\vdash_{1}$ is that

[TABLE]

where $\models_{\textbf{B}_{2}}$ is a single-matrix consequence w.r.t. matrix $\textbf{B}_{2}$ (Section 2.2.1). To prove (3.6), one needs to show that each rule of (a)–(b) preserves validity in $\textbf{B}_{2}$. We leave this task to the reader. (Exercise 3.3.10)

Clearly, the converse of (3.6) is not true, for if $\alpha$ is a classical tautology, then $\emptyset\models_{\textbf{B}_{2}}\alpha$ but $\emptyset\not\vdash_{1}\alpha$.

Relation $\vdash_{2}$

Our next example, relation $\vdash_{2}$, is a modification of $\vdash_{1}$. Namely we define:

[TABLE]

where $L\textbf{B}_{2}$ is the logic of matrix $\textbf{B}_{2}$ (Definition 2.2.5), that is the set of classical tautologies. According to Proposition 3.1.2, $\vdash_{2}$ is a consequence relation whose set of theses is $L\textbf{B}_{2}$.

In addition, we claim that

[TABLE]

The proof of (3.7) follows from the proof of (3.6), where we have to add one more (obvious) case — when $\alpha_{i}$ in (3.5) is a classical tautology, that is $\alpha_{i}\in L\textbf{B}_{2}$.

The converse of (3.7) is also true, that is

[TABLE]

To prove (3.8), we first prove that the consequence relation $\models_{\textbf{B}_{2}}$ is finitary. Indeed, the premise $X\models_{\textbf{B}_{2}}\alpha$ is equivalent to that the set $X\cup\{\neg\alpha\}$ is not satisfiable in $\textbf{B}_{2}$, that is for any valuation $v$ in $\textbf{B}_{2}$, $v[X\cup\{\neg\alpha\}]\not\subseteq\{\mathbf{1}\}$. Then, by compactness theorem,222Cf. [Bar77], J. Barwise, An introduction to first-order logic, theorem 4.2. See also [CK90], corollary 1.2.12. $X\cup\{\neg\alpha\}$ is not finitely satisfiable in $\textbf{B}_{2}$, that is, there is $X_{0}\Subset X$ such that $X_{0}\cup\{\neg\alpha\}$ is not satisfiable in $\textbf{B}_{2}$. The latter is equivalent to $X_{0}\models_{\textbf{B}_{2}}$.333We will consider this argument in a more general setting in Section 4.2.

In the next step, having $X_{0}\models_{\textbf{B}_{2}}\alpha$ with $X_{0}\Subset X$, we show that $X_{0}\vdash_{2}\alpha$.

If $X_{0}=\emptyset$, then $\alpha$ is a classical tautology and the conclusion is obvious. Assume that

[TABLE]

We denote

[TABLE]

and observe that $\wedge X_{0}\rightarrow\alpha$ is a classical tautology, that is $\wedge X_{0}\rightarrow\alpha\in L\textbf{B}_{2}$. Further, it is easy to see that $X_{0}\vdash_{2}\wedge X_{0}$. The two last observations imply that $X_{0}\vdash_{2}\alpha$ and hence $X\vdash_{2}\alpha$.

According to Proposition 3.3.3 and the consideration above, $\models_{\textbf{B}_{2}}$, as well as $\vdash_{2}$, is a finitary structural consequence relation.

Relation $\vdash_{3}$

For the next example, we employ the hyperrules (c). We state that $X\vdash_{3}\alpha$ when the latter can be confirmed by one of the following types of confirmation or their combination. A formal definition is the following.

$1^{\circ}$ The first type is a derivation of $\alpha$ from $X$ by using steps determined by ($\text{d}_{1}$)–($\text{d}_{2}$), that is a derivation confirming $X\vdash_{1}\alpha$.

$2^{\circ}$ The second type is when confirmed premises of one of the hyperrules (c) are satisfied for $\vdash_{3}$, we can confirm the conclusion of this hyperrule. (This means an application of the hyperrule in question.)

$3^{\circ}$ The third type consists in the following. When we have confirmed $X\vdash_{3}\alpha_{1},\ldots,X\vdash_{3}\alpha_{n}$, we confirm $X\vdash_{3}\alpha$ if $X,\alpha_{1},\ldots,\alpha_{n}\vdash_{1}\alpha$.

Thus, for any set $X$ of $\mathcal{L}_{A}$-formulas and any $\mathcal{L}_{A}$-formula $\alpha$, $X\vdash_{3}\alpha$ is true if, and only if, there is a consecutive finite number of confirmations of the types of $1^{\circ}$–$3^{\circ}$. In particular,

[TABLE]

We illustrate the last definition on the following example. Using $X=\{\alpha,\beta\}$ (for concrete formulas $\alpha$ and $\beta$), we confirm $X\vdash_{3}\alpha\wedge\beta$ by the derivation

[TABLE]

Then, we rewrite the last sequent as $\{\alpha\},\beta\vdash_{3}\alpha\wedge\beta$ and apply (c-$i$) to obtain $\{\alpha\}\vdash_{3}\beta\rightarrow(\alpha\wedge\beta)$ (confirmation of the second type). Now, we rewrite the last sequent as $\emptyset,\alpha\vdash_{3}\beta\rightarrow(\alpha\wedge\beta)$ and apply this hyperrule one more time. The resulting sequent is $\emptyset\vdash_{3}\alpha\rightarrow(\beta\rightarrow(\alpha\wedge\beta))$, or simply $\vdash_{3}\alpha\rightarrow(\beta\rightarrow(\alpha\wedge\beta))$.

It should be clear that the relation $\vdash_{3}$ is monotone; that is

[TABLE]

At the point, we do not know yet if $\vdash_{3}$ is a consequence relation. Our aim is to prove this. More than that, we shall show that $\vdash_{3}$ and $\vdash_{2}$ are equal as relations, though defined differently. We discuss advantage and disadvantage of $\vdash_{3}$ in relation to $\vdash_{2}$ at the end of this subsection.

Aiming to prove $\vdash_{3}\,=\,\vdash_{2}$, we notice that the relation $\vdash_{3}$ enjoys the following variant of cut (the property $(\text{c}^{\ast})$ from Definition 3.1.1).

[TABLE]

Indeed, applying the hyperrule of (c-$i$), we confirm that $X\vdash_{3}\beta\rightarrow\alpha$. Using (3.10), we obtain that $X\vdash_{3}\beta$. Finally, we use a confirmation of type $3^{\circ}$ to conclude that $X\vdash_{3}\alpha$.

On the next step, we prove that

[TABLE]

Our proof of (3.12) is based on the following observation.

[TABLE]

To prove (3.13), first, we show that for any $\mathcal{L}_{A}$-formula $\alpha$,

[TABLE]

Indeed,444The following steps 1–6 are the adaptation of the proof of $51^{\ast}$ from [Kle52], § 27.

[TABLE]

Also, we will use lemma 13 of [Kle52], § 29, which we formulate in a paraphrased form as follows.

Let $\alpha$ be an $\mathcal{L}_{A}$-formula in the distinct propositional variables $p_{1},\ldots,p_{n}$; let $v$ be a valuation in $\textbf{B}_{2}$; and let a sequence of $\mathcal{L}_{A}$-formulas is produced according to the rule: if $v(p_{j})=\mathbf{1}$, then $\beta_{j}=p_{j}$, and if $v(p_{j})=\mathbf{0}$, then $\beta_{j}=\neg p_{j}$. Then $\beta_{1},\ldots,\beta_{n}\vdash_{3}\alpha$ or $\beta_{1},\ldots,\beta_{n}\vdash_{3}\neg\alpha$, according as for the given valuation $v$ $\alpha$ takes the value $\mathbf{1}$ or the value $\mathbf{0}$.

Now, to prove  (3.13), we assume that $\alpha\in L\textbf{B}_{2}$ and $p_{1},\ldots,p_{n}$ are all variables that occur in $\alpha$. Then, according to the last property, $p_{1},\ldots,p_{n}\vdash_{3}\alpha$ and $p_{1},\ldots,\neg p_{n}\vdash_{3}\alpha$. This, in virtue of (c-$iii$), implies that $p_{1},\ldots,p_{n-1},p_{n}\vee\neg p_{n}\vdash_{3}\alpha$. Since, by (3.11), $\vdash_{3}p_{n}\vee\neg p_{n}$, we obtain that $p_{1},\ldots,p_{n-1}\vdash_{3}\alpha$. Continuing the elimination of the variables $p_{j}$, we come to the conclusion that $\vdash_{3}\alpha$.

Now we obtain the proof of (3.12) as follows.

Assume that $X\vdash_{2}\alpha$; that is for some $\alpha_{1},\ldots,\alpha_{n}\in L\textbf{B}_{2}$, $X,\alpha_{1},\ldots,\alpha_{n}\vdash_{1}\alpha$. According to (3.9), $X,\alpha_{1},\ldots,\alpha_{n}\vdash_{3}\alpha$, where for each $\alpha_{j}$, in virtue of (3.13), $\vdash_{3}\alpha_{j}$. Using (3.11) $n$ times, we obtain that $X\vdash_{3}\alpha$.

Finally, we show that

[TABLE]

The last implication will be proven if we show that

[TABLE]

and then apply (3.8).

We note that (3.16) will be proven if we establish that every rule of (a)–(b) and every hyperrule of (c) preserves the truth value $\mathbf{1}$. Let us check this property for the hyperrules.

We begin with (c-$i$). Assume that for any valuation $v^{\prime}$ in $\textbf{B}_{2}$,

[TABLE]

Suppose for some valuation $v$, $v[X]\subseteq\{\mathbf{1}\}$. We observe that if $v[\alpha]=\mathbf{0}$, then $v[\alpha\rightarrow\beta]=\mathbf{1}$, regardless of the value of $v[\beta]$. However, if $v[\alpha]=\mathbf{1}$, then $v[\alpha\rightarrow\beta]=\mathbf{1}$, by premise.

Now we turn to (c-$ii$). Suppose that for any valuation $v^{\prime}$ in $\textbf{B}_{2}$,

[TABLE]

It is clear that this premise is equivalent to that for any valuation $v^{\prime}$ in $\textbf{B}_{2}$,

[TABLE]

Thus, if for some valuation $v$, $v[X]\subseteq\{\mathbf{1}\}$, then obviously $v[\alpha]=\mathbf{0}$, that is $v[\neg\alpha]=\mathbf{1}$.

To prove this preservation property for (c-$iii$), we suppose that for any valuation $v^{\prime}$ in $\textbf{B}_{2}$, both

[TABLE]

hold. Now assume that for some valuation $v$, $v[X,\alpha\vee\beta]\subseteq\{\mathbf{1}\}$. It is clear that either $v[\alpha]=\mathbf{1}$ or $v[\beta]=\mathbf{1}$ (or both). In each case, we obtain that $v[\gamma]=\mathbf{1}$.

Thus we have obtained the equality $\vdash_{2}\,=\,\vdash_{3}$. As a byproduct of this equality, we conclude that $\vdash_{3}$ is a structural consequence relation.

Comparison of $\vdash_{2}$ and $\vdash_{3}$

We begin with the remark that neither $\vdash_{2}$ nor $\vdash_{3}$ is a calculus; the later is not because of the presence of hyperrules, the former because of the factual presence of the infinite set $L\textbf{B}_{2}$ of classical tautologies. However, $\vdash_{2}$ can be reformulated in such a way that in a new formulation, let us call it $\vdash_{2^{\circ}}$, the latter is a calculus. First of all, we remove from the definition of $\vdash_{2}$ all rules except $\alpha,\alpha\rightarrow\beta/\beta$ (known as modus ponens or detachment). The removed rules are actually replaced with rules without premises, that is rules of type $\emptyset/\varphi$, where $\varphi$ is one of the following forms of formulas (which are called axiom schemata):

[TABLE]

We will not prove that $\vdash_{2^{\circ}}\,=\,\vdash_{2}$, but we state that $\vdash_{2^{\circ}}$ is a calculus.

However, the aforementioned removal of rules is not necessary; it would suffice to add to the rules (a)–(b) nine new rules of type $\emptyset/\varphi$, where $\varphi$ is one of the schemata ax1–ax10; in this case, the notion of derivation should be modified from $\vdash_{1}$ (namely the clause ($\text{d}_{2}$)) by including the new rules. We treat the forms ax1–ax10 as premiseless modus rules.

Although $\vdash_{3}$ is not a calculus, it is very convenient in confirming sequents that are true w.r.t. $\vdash_{2^{\circ}}$. For instance, we show that the schema ax8 above is a thesis of $\vdash_{3}$. Indeed, we have:

[TABLE]

However, there is a price for such a convenience. While in proving $X\vdash_{2}\alpha$ (or in proving $X\vdash_{2^{\circ}}\alpha$) a set $X$ stays the same in each application of a rule; in proving $X\vdash_{3}\alpha$, when we need to apply a hyperrule, the set “$X$” in the premise(s) of a hyperrule may differ from the original $X$ in the sequent we are proving. In addition, in each application of a hyperrule, the $X$ in its premise(s) may vary from hyperrule to hyperrule or from one application to another of the same hyperrule.

The idea of semantic completeness

The equalities like $\vdash_{2}\,=\,\models_{\textbf{B}_{2}}$ or $\vdash_{2^{\circ}}\,=\,\models_{\textbf{B}_{2}}$ or $\vdash_{3}\,=\,\models_{\textbf{B}_{2}}$, but not $\vdash_{2}\,=\,\vdash_{2^{\circ}}$ or $\vdash_{2}\,=\,\vdash_{3}$, (see Section 3.3) are typical examples of semantic completeness. That is, a completeness result is claimed when one and the same consequence relation admits two different definitions — one purely syntactic and the other with the help of semantic concepts, such as, e.g., logical matrices. The former is regarded as a convenient way to define an abstract logic, say $\mathcal{S}$, the latter as an effective way to show that for a particular set $X$ and formula $\alpha$, the sequent $X\vdash_{\mathcal{S}}\alpha$ does not hold. This issue will be further discussed in the next chapter (Section 4.3).

To demonstrate, e.g., the validity of $\vdash_{2}\,=\,\models_{\textbf{B}_{2}}$, we proved the properties (3.7) and (3.8). The former is known in literature as soundness, the latter as (properly) semantic completeness. Thus we can state that the abstract logic $\vdash_{2}$ is complete w.r.t. the logical matrix $\mathbf{B}_{2}$, or that $\vdash_{2}$ is determined by $\mathbf{B}_{2}$.

Although the main concept of this book is consequence relation, the equalities like

[TABLE]

(compare with the LC completeness above) will attract our attention too. We call them also completeness results but in a weaker sense of the term “completeness”.

Exercises 3.3

Prove that a structural logic $\mathcal{S}$ is trivial if, and only if, for any arbitrary variable $p$, $p\in\textbf{Cn}_{\mathcal{S}}(\emptyset)$. 2. 2.

Prove that for any abstract logic $\mathcal{S}$, $\mathcal{S}$ is trivial if, and only if, $\bm{T}_{\mathcal{S}}$ is inconsistent. 3. 3.

Let $\mathcal{S}$ be a structural abstract logic. Prove that an $\mathcal{S}$-theory is closed under substitution if, and only if, this theory is generated by a set closed under substitution. Prove that $\bm{T}_{\mathcal{S}}$ is the least $\mathcal{S}$-theory closed under any substitution. 4. 4.

Prove Proposition 3.3.3. 5. 5.

Prove Corollary 3.3.4.1. 6. 6.

Prove Corollary 3.3.5.1 7. 7.

Prove Corollary 3.3.5.2 8. 8.

Show that $\vdash_{[\mathcal{R}]}$ is a consequence relation. 9. 9.

Prove that for any abstract logic $\mathcal{S}$, the consequence relation $\vdash_{\mathcal{S}}$ is determined by $\{\vdash_{\mathcal{S}}\}$. 10. 10.

Prove (3.6). 11. 11.

Show that the schemata ax1–ax7 and ax9–ax10 are theses of $\vdash_{3}$. 12. 12.

Although for any consequence operator Cn, $\textbf{Cn}(X\cap Y)\subseteq\textbf{Cn}(X)\cap\textbf{Cn}(Y)$ for any sets $X$ and $Y$, the converse inclusion is not necessarily true. Define such an abstract logic $\mathcal{S}$ that $\textbf{Cn}_{\mathcal{S}}(X)\cap\textbf{Cn}_{\mathcal{S}}(Y)\not\subseteq\textbf{Cn}_{\mathcal{S}}(X\cap Y)$ for some sets $X$ and $Y$.

3.4 Abstract logics defined by modus rules

When we use or investigate calculi, we inevitably deal with modus rules. As we will see below (Corollary 3.4.1.2), for a structural logic to be finitary and defined as calculus, are equivalent properties. On the other hand, the modus rules are naturally modeled in first order logic.

3.4.1 General characterization

If $\mathcal{R}$ is a set of modus rules, there is an effective way to determine the consequence relation $\vdash_{[\mathcal{R}]}$ defined in (3.4) (Section 3.3.3). For this, we define a relation $\vdash_{\mathcal{R}}$ on $\mathcal{P}(\textit{{Fm}})\times\textit{{Fm}}$, by generalizing (for $\mathcal{L}$-formulas) the notion of derivation which earlier was defined for $\mathcal{L}_{A}$-formulas via ($\text{d}_{1}$)–($\text{d}_{2}$).

The relation $X\vdash_{\mathcal{R}}\alpha$ holds, by definition, if there is a list

[TABLE]

(the list $\alpha_{1},\ldots,\alpha_{n}$ can be empty), where each formula on (3.17) is

[TABLE]

We note that so defined $\vdash_{\mathcal{R}}$ is finitary. About (3.17), we say that it is an $\mathcal{R}$-derivation of $\alpha$ from $X$.

Proposition 3.4.1**.**

Let $\mathcal{R}$ be a set of modus rules. Then $\vdash_{\mathcal{R}}\,=\,\vdash_{[\mathcal{R}]}$. Hence $\vdash_{\mathcal{R}}$ is a consequence relation.

Proof.

We shall prove successively the following three claims.

[TABLE]

We notice that the properties (a)–(b) of Definition 3.1.1 are obviously true for $\vdash_{\mathcal{R}}$; and we leave for the reader to check the property (c) and structurality property. (Exercise 3.4.2)

Next, suppose that $\langle\Gamma,\phi\rangle\in\mathcal{R}$. Let $\bm{\sigma}$ be an arbitrary instantiation in $\mathcal{L}$. Since $\Gamma$ is finite, we denote

[TABLE]

According to the clauses $(\text{d}^{\ast}_{1})$–$(\text{d}^{\ast}_{2})$, the list

[TABLE]

is an $\mathcal{R}$-derivation of $\bm{\sigma}(\phi)$ from $\bm{\sigma}(\Gamma)$. Hence $\bm{\sigma}(\Gamma)\vdash_{\mathcal{R}}\bm{\sigma}(\phi)$.

Finally, let $\mathcal{S}$ be an abstract logic and for any $R\in\mathcal{R}$, $R$ is sound w.r.t. $\mathcal{S}$. We show that then

[TABLE]

Suppose (3.17) is a derivation w.r.t. $\mathcal{R}$. We prove that for each formula $\alpha_{i}$ of (3.17), $X\vdash_{\mathcal{S}}\alpha_{i}$. We employ induction on the number of the formulas preceding $\alpha$ in (3.17). Indeed, we see that, if $\alpha=\alpha_{1}$, then $X\vdash_{\mathcal{S}}\alpha_{1}$, for either $\alpha\in X$ or $\alpha$ is a conclusion of a premiseless rule.

Now, suppose $\alpha$ is obtained by application of a rule $R_{\langle\Gamma,\bm{\beta}\rangle}$. That is, for some formulas $\alpha_{i_{1}},\ldots,\alpha_{i_{k}}$ preceding $\alpha$ and some instantiation $\bm{\sigma}$, $\bm{\sigma}(\Gamma)=\{\alpha_{i_{1}},\ldots,\alpha_{i_{k}}\}$ and $\bm{\sigma}(\bm{\beta})=\alpha$. Since, by induction, $X\vdash_{\mathcal{S}}\alpha_{i_{j}}$, $1\leq j\leq k$, and, by soundness of $R_{\langle\Gamma,\bm{\beta}\rangle}$ w.r.t. $\mathcal{S}$, $\bm{\sigma}(\Gamma)\vdash_{\mathcal{S}}\alpha$, we conclude that $X\vdash_{\mathcal{S}}\alpha$. ∎

Given a set $\mathcal{R}$ of modus rules, we denote by $\mathcal{S}_{\mathcal{R}}$ the abstract logic corresponding to $\vdash_{[\mathcal{R}]}$ (see the definition (3.4)) or, equivalently (due to Proposition 3.4.1), to $\vdash_{\mathcal{R}}$.

Corollary 3.4.1.1**.**

If $\mathcal{R}$ is a set of modus rules, then the abstract logic $\mathcal{S}_{\mathcal{R}}$ is structural and finitary.

Proof is left to the reader. (Exercise 3.4.1)

Corollary 3.4.1.2**.**

Let $\mathcal{S}$ be a structural abstract logic. Then $\mathcal{S}$ is finitary if, and only if, there is a set $\mathcal{R}$ of modus rules such that $\mathcal{S}=\mathcal{S}_{\mathcal{R}}$.

Proof.

The if-part follows from Corollary 3.4.1.1.

To prove the only-if part, we assume that $\mathcal{S}$ is finitary. Next we define:

[TABLE]

We aim to prove that $\mathcal{S}=\mathcal{S}_{\mathcal{R}}$.

First, assume that $X\vdash_{\mathcal{S}}\beta$, for a particular set $X\cup\{\beta\}\subseteq\textit{{Fm}}$. Since $\mathcal{S}$ is finitary, there is a set $Y\Subset X$ such that $Y\vdash_{\mathcal{S}}\beta$. Now, replacing the variables $\mathcal{V}(Y\cup\{\beta\})$ with metavariables according to arbitrary one-one correspondence, we obtain a finite set $\Gamma\cup\{\phi\}$ of metaformulas such that for any instantiation $\bm{\xi}$, $\bm{\xi}(\Gamma)\vdash_{\mathcal{S}}\bm{\xi}(\phi)$ and for a particular instantiation $\bm{\xi}_{0}$, $\bm{\xi}_{0}(\Gamma)=Y$ and $\bm{\xi}_{0}(\phi)=\beta$. This implies that $\langle\Gamma,\phi\rangle\in\mathcal{R}$. The latter in turn allows us to conclude that $Y\vdash_{\mathcal{R}}\beta$ and hence $X\vdash_{\mathcal{R}}\beta$.

Now, we suppose that $X\vdash_{\mathcal{R}}\beta$. That is, there is an $\mathcal{R}$–derivation, determined by $(\text{d}^{\ast}_{1})$–$(\text{d}^{\ast}_{2})$:

[TABLE]

It is obvious that the list $(\ast)$ is not empty. We prove (by induction) that for each formula $\gamma$ of $(\ast)$, $X\vdash_{\mathcal{S}}\gamma$.

It is true for the first formula $\gamma$ in $(\ast)$, in which case $\gamma=\alpha_{1}=\beta$, for, then, $\gamma\in X$ and hence $X\vdash_{\mathcal{S}}\gamma$.

Suppose we proved that for each $\alpha_{i}$, $X\vdash_{\mathcal{S}}\alpha_{i}$. If $\beta\in X$, we are done. If $\beta\notin X$, then $\beta$ is obtained from $\alpha_{i_{1}},\ldots,\alpha_{i_{k}}$ by a rule $\langle\Gamma,\phi\rangle\in\mathcal{R}$. By induction, this implies that $\{\alpha_{i_{1}},\ldots,\alpha_{i_{k}}\}\vdash_{\mathcal{S}}\beta$. By the transitivity property, we conclude that $X\vdash_{\mathcal{S}}\beta$. ∎

3.4.2 The class of $\mathcal{S}$-models

In this subsection we focus on the class of $\mathcal{S}$-models, when an abstract logic $\mathcal{S}$ can be determined by a set of modus rules. Given a structural abstract logic $\mathcal{S}$ in a language $\mathcal{L}$, we employ for our characterization of $\mathcal{S}$-models a special language of first order. This language depends on $\mathcal{L}$ and we denote it by $\textbf{FO}_{\mathcal{L}}$.

The denumerable set of the individual variables of $\textbf{FO}_{\mathcal{L}}$ consists of the symbols $\bm{x_{\alpha}}$, for each metavariable $\bm{\alpha}$. The functional connectives coincide with the connectives of $\mathcal{L}$. Also, there is one unary predicate symbol, $D$, two logical connectives, $\&$ (conjunction) and $\Rightarrow$ (implication), universal quantifier $\forall$, as well the parentheses, ‘(’ and ‘)’. The rules of formula formation are usual, as well as is usual the notion of an $\textbf{FO}_{\mathcal{L}}$-structure (including the notions of satisfactory and validity). If $\Theta$ is an $\textbf{FO}_{\mathcal{L}}$-formula containing only free variables, its universal closure is denoted by $\forall\ldots\forall\Theta$. Main reference here is [CK90].

It must be clear that if $\phi$ is a metaformula relevant to $\mathcal{L}$, then, replacing each metavariable $\bm{\alpha}$ in $\phi$ with the individual variable $\bm{x_{\alpha}}$, we obtain a term of $\textbf{FO}_{\mathcal{L}}$. We denote this term (obtained from $\phi$) by $\phi^{\ast}$.

Further, any modus rule $R:=\dfrac{\psi_{1},\ldots,\psi_{n}}{\phi}$ is translated to the formula

[TABLE]

and any premiseless rule $T:=\emptyset/\phi$ to the formula

[TABLE]

The formulas of types (3.17) and (3.18) belong to the class of basic Horn sentences; cf. [CK90], section 6.2.

It is clear that any matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ of type $\mathcal{L}$ can be regarded as a model for $\textbf{FO}_{\mathcal{L}}$-formulas. We denote the validity of a closed formula $\Theta$ in M by $\textsf{{M}}\Vdash\Theta$.

Let $\psi$ be a metaformula of $\textit{{Mf}}_{\mathcal{L}}$ containing only metavariables $\alpha_{1},\ldots,\alpha_{n}$. We note that there is a strong correlation between the standard valuation of the term $\psi^{\ast}$ (containing only individual variables $x_{\alpha_{1}},\ldots,x_{\alpha_{n}}$) in a first order structure M and a valuation of a formula $\bm{\xi}(\psi)$, obtained from $\psi$ by a simple instantiation $\bm{\xi}$, in a logical matrix M. For instance, let us denote the value of $\psi^{\ast}$ on a sequence $a_{1},\ldots,a_{n}$ in M (as a first order structure) by $\psi^{\ast}[a_{1},\ldots,a_{n}]$. Now let $\bm{\xi}$ be a simple instantiation with $\bm{\xi}(\alpha_{i})=p_{i}$. Then, if $v$ is a valuation in A with $v[p_{i}]=a_{i}$, then $\psi^{\ast}[a_{1},\ldots,a_{n}]=v[\bm{\xi}(\psi)]$. This can be proven by induction on the degree of $\psi$.

Grounding on the last conclusion, we obtain The first order formula $D(\psi^{\ast})$ is satisfied on the sequence $\alpha_{1},\ldots,\alpha_{n}$ in the first order structure M if, and only if, $v[\bm{\xi}(\psi)]\in D$ in the logical matrix M.

This argument leads to the following lemma.

Lemma 3.4.1**.**

Let $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be a matrix of type $\mathcal{L}$. For any modus rule $R$, $R$ is sound w.r.t. $\models_{\textbf{M}}$ if, and only if, $\textsf{{M}}\Vdash R^{\ast}$.

Proof is left to the reader. (Exercise 3.4.5)

Proposition 3.4.2**.**

Let $\mathcal{R}$ be a set of modus rules in $\mathcal{L}$. Then for any $\mathcal{L}$-matrix M, M is an $\mathcal{S}_{\mathcal{R}}$-model if, and only if, $\textsf{{M}}\Vdash R^{\ast}$, for any $R\in\mathcal{R}$.

Proof.

We fix an $\mathcal{L}$-matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$. In view of Proposition 3.4.1, we can associate with the abstract logic $\mathcal{S}_{\mathcal{R}}$ the consequence relation $\vdash_{\mathcal{R}}$.

We begin with the “only-if” part. Thus we assume that the inclusion $\vdash_{\mathcal{R}}\,\subseteq\,\models_{\textbf{M}}$ holds. This implies that any $R\in\mathcal{R}$ is sound w.r.t. $\models_{\textbf{M}}$. By Lemma 3.4.1, this in turn implies that $\textsf{{M}}\Vdash R^{\ast}$, for any $R\in\mathcal{R}$.

To prove the “if” part, we assume that the last conclusion holds. By Lemma 3.4.1, we derive that any $R\in\mathcal{R}$ is sound w.r.t. $\models_{\textbf{M}}$.

Now, suppose that $X\vdash_{\mathcal{R}}\alpha$. That is, there is an $\mathcal{R}$-derivation (3.17). By induction on the length of (3.17), one can prove that for any valuation $v$ in A, if $v[X]\subseteq D$, then $v[\alpha]\in D$. We leave this task to the reader. (Exercise 3.4.6) ∎

Corollary 3.4.2.1**.**

Let $\mathcal{R}$ be a set of modus rules in $\mathcal{L}$. Then the class of all $\mathcal{S}_{\mathcal{R}}$-models is closed under reduced products, in particular under ultraproducts.

Proof.

Let $\mathcal{M}$ be the class of all $\mathcal{S}_{\mathcal{R}}$-models. According to Proposition 3.4.2, an $\mathcal{L}$-matrix $\textsf{{M}}\in\mathcal{M}$ if, and only if, for any $R\in\mathcal{R}$, $R\in\mathcal{R}$. This means that $\mathcal{M}$ is determined by a set of Horn formulas. It is well known that every Horn sentence is preserved under reduced products, in particular under ultraproducts; cf. [CK90], proposition 6.2.2. ∎

3.4.3 Modus rules vs. non-finitary rules

Proposition 3.4.1 and Corollary 3.4.1.1 show limitation of modus rules in defining consequent relations. It should not be surprising that there are consequence relations that cannot be defined by any set of modus rules. Below we discuss an example of the consequence relation of that kind; moreover, the theorems of that abstract logic, as we will show, coincide with the theorems of a calculus, LC. (See LC completeness below.)

In the language $\mathcal{L}_{A}$, we formulate two more premiseless structural rules:

[TABLE]

A calculus LC is defined through derivations according to $(\text{d}_{1})$–$(\text{d}_{2})$ where in $(\text{d}_{2})$, however, we use only the rules ax1–ax9, ax11-ax12 and (b-$iii$) (modus ponens).

We note two properties of LC. The first is that for any set $X_{0}\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}_{A}}$,

[TABLE]

(See Exercise 3.4.3.)

The second property is known as the “deduction theorem” (for LC), which in its $\Rightarrow$-part, in essence, asserts that the hyperrule (c–$i$) is sound w.r.t. $\vdash_{\textsf{LC}}$. Namely, for any set $X\cup\{\alpha,\beta\}\subseteq\textit{{Fm}}_{\mathcal{L}_{A}}$,

[TABLE]

(See Exercise 3.4.4.)

In our consideration, we employ the single matrix relation $\models_{\textbf{LC}}$ which is grounded on the logical matrix LC; see Section 2.2.5.

We will need the following property.

For any $\mathcal{L}_{A}$-formulas $\alpha$ and $\beta$,

[TABLE]

The last equivalence is due to M. Dummett [Dum59], theorem 1.

Next, we define a consequence relation, $\vdash_{\textsf{LC}}$ (or abstract logic LC), analogously to the relation $\vdash_{2}^{\circ}$ (Section 3.3), but by using the rules ax1–ax9, ax11–ax12 and modus ponens (the rule (b-$iii$)) for the notion of LC-derivation defined by the clauses ($\text{d}_{1}^{\ast}$)–($\text{d}_{2}^{\ast}$) above.

In addition, we consider the non-modus structural rule $R^{\ast}:=R_{\langle\Gamma^{\ast},\bm{\alpha}_{0}\rangle}$ with

[TABLE]

where $\bm{\alpha}_{i}$, $0\leq i<\omega$, are pairwise distinct metavariables. Also, we define an infinite set of modus rules

[TABLE]

Then, two consequence relations, $\vdash^{\ast}$ and $\vdash^{\star}$, are defined in $\mathcal{P}(\textit{{Fm}}_{\mathcal{L}_{A}})\times\textit{{Fm}}_{\mathcal{L}_{A}}$ similarly to the notion of LC-derivation but also for $\vdash^{\ast}$ with $R^{\ast}$ as an additional inference rule and for $\vdash^{\star}$ with the rules of $\mathcal{R}$ as additional inference rules.

We aim to show that, although for any set $X_{0}\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}_{A}}$,

[TABLE]

the consequence relation $\vdash^{\ast}$ cannot be defined by any set of structural modus rules, for, as we will show, it is not finitary; see Corollary 3.4.1.1.

As concerns (3.20), it is obvious, for in any $\vdash^{\ast}$-derivation with a finite set $X_{0}$ as a set of premises, the rule $R^{\ast}$ can be applied only under such an instantiation $\bm{\xi}$, for which there is an instantiation $\bm{\zeta}$ such that $\bm{\xi}(\Gamma^{\ast})/\bm{\xi}(\bm{\alpha_{0}})=\bm{\zeta}(\Gamma)/\bm{\zeta}(\bm{\alpha})$, for some $\Gamma\Subset\Gamma^{\ast}$; and vice versa.

Finally, we demonstrate that the consequence relation $\vdash^{\ast}$ differs from $\vdash_{\textsf{LC}}$, for the latter is finitary (Corollary 3.4.1.1), while the former cannot be defined by any set of modus rules.

For contradiction, assume that $\vdash^{\ast}$ is finitary. Let $\bm{\sigma}$ be an instantiation such that $\bm{\sigma}(\bm{\alpha}_{i})=p_{i}$, $0\leq i<\omega$. We note that $\bm{\sigma}(\Gamma^{\ast})\vdash^{\ast}p_{0}$. By assumption, for some finite $X_{0}\Subset\bm{\sigma}(\Gamma^{\ast})$, $X_{0}\vdash^{\ast}p_{0}$. In virtue of (3.20), $X_{0}\vdash_{\textsf{LC}}p_{0}$. This in turn, according to (3.19) and (3.20), implies that $\vdash_{\textsf{LC}}\wedge X_{0}\rightarrow p_{0}$. By LC completeness, we obtain that $\models_{\textbf{LC}}\wedge X_{0}\rightarrow p_{0}$ and hence $X_{0}\models_{\textbf{LC}}p_{0}$. Thus, by monotonicity, we have that $\bm{\sigma}(\Gamma^{\ast})\models_{\textbf{LC}}p_{0}$. However, let $v$ be such a valuation that $v[p_{0}]$ is a pre-last element $a$ of LC w.r.t. $\leq$ and $v[p_{i}]\neq v[p_{j}]$, whenever $i<j$. Then, since $v[p_{i}\leftrightarrow p_{j}]\leq a$, we have: $v[\bm{\sigma}(\Gamma^{\ast})]\subseteq\{\mathbf{1}\}$, but $v[p_{0}]=a\neq\mathbf{1}$.

Exercises 3.4

Prove Corollary 3.4.1.1. 2. 2.

Show that if $\mathcal{R}$ is a set of structural modus rules, then the relation $\vdash_{[\mathcal{R}]}$ satisfies the property (c) and structurality property of Definition 3.1.1. 3. 3.

Prove the equivalence (3.19). 4. 4.

Prove the equivalence (3.20) (the deduction theorem for LC). 5. 5.

Prove Lemma 3.4.1. 6. 6.

Finish the proof of Proposition 3.4.2.

3.5 Extensions of abstract logics

In this section we consider interaction of abstract logics defined in different formal languages. We begin with the following two definitions.

Definition 3.5.1** (extension, conservative extension).**

Let a language $\mathcal{L}^{+}$ be an extension of a language $\mathcal{L}$. Also, let $\mathcal{S}^{+}$ and $\mathcal{S}$ be abstract logics in the languages $\mathcal{L}^{+}$ and $\mathcal{L}$, respectively. The abstract logic $\mathcal{S}^{+}$ is an extension of $($or over$)$ $\mathcal{S}$ if for any set $X$ of $\mathcal{L}$​-formulas,

[TABLE]

We call $\mathcal{S}^{+}$ a conservative extension of $($or over$)$ $\mathcal{S}$ if for any set $X$ of $\mathcal{L}$​-formulas,

[TABLE]

The following two observation are obvious.

Proposition 3.5.1**.**

Let a language $\mathcal{L}^{+}$ be an extension of a language $\mathcal{L}$. Assume that $\mathcal{S}$ is a structural logic in $\mathcal{L}$ and $\mathcal{S}^{+}$ is its structural extension in $\mathcal{L}^{+}$. Then if $\mathcal{S}$ is trivial, then so is $\mathcal{S}^{+}$.

Proof.

If $\mathcal{S}$ is trivial, then $p\in\textbf{Cn}_{\mathcal{S}}(\emptyset)$, for an arbitrary $p\in\mathcal{V}_{\mathcal{L}}$. Since $\mathcal{S}^{+}$ is an extension of $\mathcal{S}$, $p\in\textbf{Cn}_{\mathcal{S}^{+}}(\emptyset)$. And since $\mathcal{S}^{+}$ is structural, the latter implies that $\mathcal{S}^{+}$ is trivial. ∎

Proposition 3.5.2**.**

Let a language $\mathcal{L}^{+}$ be an extension of a language $\mathcal{L}$ and let $\mathcal{S}$ be an abstract logic in $\mathcal{L}$. The intersection of any nonempty set of conservative extensions of $\mathcal{S}$ in $\mathcal{L}^{+}$ is a conservative extensions of $\mathcal{S}$ in $\mathcal{L}^{+}$.

Proof is left to the reader. (Exercise 3.5.1)

A simple way to obtain a (structural) conservative extension of a given abstract logic is the following.

Indeed, assume that $\mathcal{S}$ is a structural logic in $\mathcal{L}$ and $\mathcal{L}^{+}$ is an extension of $\mathcal{L}$. According to Corollary 3.3.5.1, the atlas $\textsf{{Lin}}[\Sigma_{\mathcal{S}}]=\left\langle\mathfrak{F}_{\mathcal{L}},\Sigma_{\mathcal{S}}\right\rangle$ is adequate for $\mathcal{S}$. Let us select an arbitrary formula $\alpha\in\textit{{Fm}}$ and expand the signature of $\mathfrak{F}_{\mathcal{L}}$ to $\mathcal{L}^{+}$, thereby obtaining an expansion $\mathfrak{F}_{\mathcal{L}}[\alpha]^{+}$, as follows. For any $c\in\mathcal{C}_{\mathcal{L}^{+}}\setminus\mathcal{C}_{\mathcal{L}}$ we interpret as the element $\alpha\in|\mathfrak{F}_{\mathcal{L}}|$. Similarly, for any new connective $F\in\mathcal{F}_{\mathcal{L}^{+}}\setminus\mathcal{F}_{\mathcal{L}}$, we interpret any term $F(\beta_{1},\ldots,\beta_{n})$ by $\alpha$. Then, we define an abstract logic $\mathcal{S}^{+}$ as the one determined by the atlas $\left\langle\mathfrak{F}_{\mathcal{L}}[\alpha]^{+},\Sigma_{\mathcal{S}}\right\rangle$.

According to Proposition 3.3.3, $\mathcal{S}^{+}$ is structural. Further, $\mathcal{S}^{+}$ is a conservative extension of $\mathcal{S}$, for for any set $X\cup\{\beta\}\subseteq\textit{{Fm}}$,

[TABLE]

We leave the reader to prove (3.22); see Exercise 3.5.2.

In virtue of Proposition 3.5.1, $\mathcal{S}^{+}$ is trivial if $\mathcal{S}$ is trivial.

We summarize as follows.

Proposition 3.5.3**.**

Let $\mathcal{S}$ be an structural abstract logic in $\mathcal{L}$ and $\mathcal{L}^{+}$ be an extension of $\mathcal{L}$. Then there is a conservative structural extension $\mathcal{S}^{+}$ of $\mathcal{S}$. Moreover, if $\mathcal{S}$ is trivial, $\mathcal{S}^{+}$ is also trivial.

Corollary 3.5.3.1**.**

Let a language $\mathcal{L}^{+}$ be an extension of a language $\mathcal{L}$. Any structural abstract logic in $\mathcal{L}$ has a least structural conservative extension in $\mathcal{L}^{+}$.

Proof.

We use Proposition 3.5.3 and Proposition 3.5.2. ∎

Our next definition will play a key part in the sequel.

Definition 3.5.2** (relation $\vdash_{(\mathcal{S})^{+}}$).**

Let a language $\mathcal{L}^{+}$ be an extension of a language $\mathcal{L}$. Also, let $\mathcal{S}$ be an abstract logic in $\mathcal{L}$. We define a relation $\vdash_{(\mathcal{S})^{+}}$ in $\mathcal{P}(\textit{{Fm}}_{\mathcal{L}^{+}})\times\textit{{Fm}}_{\mathcal{L}^{+}}$ as follows:

[TABLE]

We find a justification for the last definition in the following proposition.

Proposition 3.5.4**.**

Let a language $\mathcal{L}^{+}$ be an extension of a language $\mathcal{L}$ and $\mathcal{S}$ be a structural abstract logic in $\mathcal{L}$. If the relation $\vdash_{(\mathcal{S})^{+}}$ is a consequence relation, then $(\mathcal{S})^{+}$ is the least structural conservative extension of $\mathcal{S}$ in $\mathcal{L}^{+}$. In addition, $(\mathcal{S})^{+}$ is nontrivial if, and only if, $\mathcal{S}$ is nontrivial.

Proof.

It is obvious that $(\mathcal{S})^{+}$ is a conservative extension of $\mathcal{S}$. (The structurality of $\mathcal{S}$ should be used.)

Next, we prove the structurality of $(\mathcal{S})^{+}$. For this, assume that $X\vdash_{(\mathcal{S})^{+}}\alpha$. By definition, there are a set $Y\cup\{\beta\}\subseteq\textit{{Fm}}$ and an $\mathcal{L}^{+}$-substitution $\sigma$ such that $Y\vdash_{\mathcal{S}}\beta$, $\sigma(Y)\subseteq X$ and $\sigma(\beta)=\alpha$. Let $\xi$ be any $\mathcal{L}^{+}$-substitution. We observe: $\xi\circ\sigma(Y)\subseteq\xi(X)$ and $\xi\circ\sigma(\beta)=\xi(\alpha)$. Then, by definition, $\xi(X)\vdash_{(\mathcal{S})^{+}}\xi(\alpha)$.

Now, let $\mathcal{S}^{+}$ be an arbitrary structural conservative extension of $\mathcal{S}$ in $\mathcal{L}^{+}$. Suppose that $X\vdash_{(\mathcal{S})^{+}}\alpha$. Then there is a set $Y\cup\{\beta\}\subseteq\textit{{Fm}}$ and an $\mathcal{L}^{+}$-substitution $\sigma$ such that $Y\vdash_{\mathcal{S}}\beta$, $\sigma(Y)\subseteq X$ and $\sigma(\beta)=\alpha$. By premise, $Y\vdash_{\mathcal{S}^{+}}\beta$. Since $\mathcal{S}^{+}$ is structural, we also have that $\sigma(Y)\vdash_{\mathcal{S}^{+}}\sigma(\beta)$. This implies that $X\vdash_{\mathcal{S}^{+}}\alpha$.

Finally, the last claim of the proposition follows from the conservativeness of $(\mathcal{S})^{+}$ over $\mathcal{S}$. ∎

In the next proposition, we give a sufficient condition for $(\mathcal{S})^{+}$ to be a consequence relation.

Proposition 3.5.5**.**

Let $\mathcal{L}$ be a language with $\kappa=\textit{card}(\mathcal{V}_{\mathcal{L}})\geq\aleph_{0}$ and $\mathcal{L}^{+}$ be a primitive extension of $\mathcal{L}$. Assume that $\mathcal{S}$ is a structural abstract logic in $\mathcal{L}$. Then the relation $\vdash_{(\mathcal{S})^{+}}$ is a consequence relation in $\mathcal{L}^{+}$. Moreover, the abstract logic $(\mathcal{S})^{+}$ is $\kappa$-compact; further, if $\mathcal{S}$ is finitary, then $(\mathcal{S})^{+}$ is also finitary.

Proof.

First, we have to show that $\vdash_{(\mathcal{S})^{+}}$ satisfies the properties of (a)–(c) of Definition 3.1.1. Leaving the check of the properties (a)–(b) to the reader, we turn to the property (c). (Exercise 3.5.3)

Assume that for a set $X\cup Y\cup Z\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}^{+}}$,

[TABLE]

In virtue of (P2) and Definition 3.5.2 (further in this proof, simply definition), there are sets $Y_{0}$ and $Z_{0}$ with $Y_{0}\cup Z_{0}\cup\{\beta_{0}\}\subseteq\textit{{Fm}}$ and an $\mathcal{L}^{+}$-substitution $\sigma_{0}$ such that $\sigma_{0}(Y_{0})\subseteq Y$, $\sigma_{0}(Z_{0})\subseteq Z$, $\sigma_{0}(\beta_{0})=\alpha$ and $Y_{0},Z_{0}\vdash_{\mathcal{S}}\beta_{0}$.

We denote:

[TABLE]

In virtue of (P1) and definition, for each $i\in I$, there is a set $X_{i}\cup\{\beta_{i}\}\subseteq\textit{{Fm}}$ and an $\mathcal{L}^{+}$-substitution $\sigma_{i}$ such that $\sigma_{i}(X_{i})\subseteq X$, $\sigma_{i}(\beta_{i})=\gamma_{i}$ and $X_{i}\vdash_{\mathcal{S}}\beta_{i}$.

Now the assumptions (P1)–(P2) can be refined as follows.

[TABLE]

We denote:

[TABLE]

We aim to show that $X^{\ast},Z^{\ast}\vdash_{(\mathcal{S})^{+}}\alpha$. Since $X^{\ast}\subseteq X$ and $Z^{\ast}\subseteq Z$, we will thus obtain that $X,Z\vdash_{(\mathcal{S})^{+}}\alpha$, for we have already proved that $\vdash_{(\mathcal{S})^{+}}$ is monotone.

Let us make notes about the cardinalities of the $\mathcal{L}^{+}$-variables of some formula sets. (This is where we use that the extension $\mathcal{L}^{+}$ is primitive.)

• •

$\textit{card}(\mathcal{V}(\{\gamma_{i}\}_{i\in I}))\leq\textit{card}(\mathcal{V}_{\mathcal{L}})$;

• •

$\textit{card}(\mathcal{V}(Z^{\ast}))=\textit{card}(\mathcal{V}(\sigma_{0}(Z_{0})))\leq\textit{card}(\mathcal{V}_{\mathcal{L}})$;

• •

$\textit{card}(\mathcal{V}(X^{\ast}))=\textit{card}(\mathcal{V}(\bigcup_{i\in I}\sigma_{i}(X_{i})))\leq\textit{card}(\mathcal{V}_{\mathcal{L}})$.

Thus we have: $\textit{card}(\mathcal{V}(\{\gamma_{i}\}_{i\in I}\cup X^{\ast}\cup Z^{\ast}\cup\{\alpha\}))\leq\textit{card}(\mathcal{V}_{\mathcal{L}})$. This allows us to claim that there is a one-one map

[TABLE]

For simplicity, we denote:

[TABLE]

Next we define two $\mathcal{L}^{+}$-substitutions. Let $q$ be an arbitrary fixed $\mathcal{L}$-variable. Then, we define:

[TABLE]

[TABLE]

We observe the following:

• •

$\mu\circ\sigma_{i}$, for all $i\in I$, and $\mu\circ\sigma_{0}$ are $\mathcal{L}$-substitutions;

• •

$\nu\circ\mu\circ\sigma_{i}(X_{i})=\sigma_{i}(X_{i})$ and $\nu\circ\mu(\gamma_{i})=\gamma_{i}$, for all $i\in I$, $\nu\circ\mu\circ\sigma_{0}(Z_{0})=\sigma_{0}(Z_{0})$ and $\nu\circ\mu\circ\sigma_{0}(\beta_{0})=\sigma_{0}(\beta_{0})$;

• •

thus $\nu(\bigcup_{i\in I}\mu\circ\sigma_{i}(X_{i}))=\nu(\mu(X^{\ast}))=X^{\ast}$, $\nu(\mu\circ\sigma_{0}(Z_{0}))\nu(\mu(Z^{\ast}))=Z^{\ast}$ and $\nu(\mu\circ\sigma_{0}(\beta_{0}))=\nu(\mu(\alpha))=\alpha$. And, by definition, we conclude that $X^{\ast},Z^{\ast}\vdash_{(\mathcal{S})^{+}}\alpha$.

From this, since $\mathcal{S}$ is structural, we obtain:

• •

$\mu\circ\sigma_{i}(X_{i})\vdash_{\mathcal{S}}\mu\circ\sigma_{i}(\beta_{i})$, for each $i\in I$, which implies $\mu(\bigcup_{i\in I}\sigma_{i}(X_{i}))\vdash_{\mathcal{S}}\mu(\gamma_{i})$, for each $i\in I$;

• •

$\{\mu(\gamma_{i})\}_{i\in I},\mu\circ\sigma_{0}(Z_{0})\vdash_{\mathcal{S}}\mu\circ\sigma_{0}(\beta_{0})$.

Then, from the two last assertions and the transitivity of $\mathcal{S}$, we derive: $\mu(X^{\ast}),\mu(Z^{\ast})\vdash_{\mathcal{S}}\mu(\alpha)$. ∎

Exercises 3.5

Prove Proposition 3.5.2 2. 2.

Prove the equivalence (3.22), that is for any set $X\cup\{\beta\}\subseteq\textit{{Fm}}$,

[TABLE]

(Hint: Show that for any valuation $v$ in $\mathfrak{F}_{\mathcal{L}}$, there is a valuation $v^{\ast}$ in $\mathfrak{F}_{\mathcal{L}}[\alpha]^{+}$ such that $v^{\ast}\!\!\upharpoonright\!\!\textit{{Fm}}=v$.) 3. 3.

Let $\mathcal{L}^{+}$ be a primitive extensions of a language $\mathcal{L}$ and let $\mathcal{S}$ be an abstract logic in $\mathcal{L}$. Show that the relation $\vdash_{(\mathcal{S})^{+}}$ of Definition 3.5.2 satisfies the properties (a)–(b) of Definition 3.1.1. 4. 4.

Prove that $(\mathcal{S})^{+}$ in Proposition 3.5.5 is $\kappa$-compact.

Chapter 4 Matrix Consequence

4.1 Single-matrix consequence

Two circumstances draw our attention to a single matrix consequence. The first one is Lindenbaum’s theorem (Proposition 3.3.4) which provides a universal way of definition of a weakly adequate logical matrix, namely the Lindenbaum matrix, which being defined for a given consequence relation, validates all of the theses of this consequence relation and only them. The other circumstance is related to the consequence relation $\vdash_{2}$ (Section 3.3) which turned out to be equal to the single-matrix relation $\models_{\textbf{B}_{2}}$. These circumstances lead to the the following concept.

We recall (Section 3.3) that a logical matrix M is called adequate for an abstract logic $\mathcal{S}$ if $\vdash_{\mathcal{S}}\,=\,\models_{\textbf{M}}$; that is, for any set $X$ of $\mathcal{L}$-formulas and any $\mathcal{L}$-formula $\alpha$,

[TABLE]

In connection with the notion of an adequate matrix, two questions arise. Is it true that any abstract logic has an adequate matrix? And if the answer to the first question is negative, what are the properties of an abstract logic that make it have an adequate matrix.

The first question can be answered in the negative as follows. Suppose $\mathcal{S}$ is a nontrivial abstract logic in $\mathcal{L}$ with $\textit{card}(\mathcal{V}_{\mathcal{L}})\geq\aleph_{0}$, which has a nonempty consistent set, say $X_{0}$, and such that $\bm{T}_{\mathcal{S}}\neq\emptyset$. Now, let $\vdash_{\mathcal{S}}^{\circ}$ be a relation obtained from $\vdash_{\mathcal{S}}$ according to (3.1). In virtue of Proposition 3.1.3, $\vdash_{\mathcal{S}}^{\circ}$ is a consequence relation. We claim that there is no adequate matrix for $\vdash_{\mathcal{S}}^{\circ}$. (Such a relation $\vdash_{\mathcal{S}}^{\circ}$ can be exemplified, e.g., by $\models_{\textbf{B}_{2}}^{\circ}$ where $\models_{\textbf{B}_{2}}$ is a single-matrix consequence of Section 3.3.)

Indeed, for contradiction, assume that a matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ is adequate for $\vdash_{\mathcal{S}}^{\circ}$. Since $X_{0}$ is consistent w.r.t. $\mathcal{S}$, it is also consistent w.r.t. $\vdash_{\mathcal{S}}^{\circ}$. This and the assumption that $X_{0}$ is nonempty imply that $D\neq\emptyset$. Assume that $a\in D$. By premise, there is a thesis $\alpha\in\bm{T}_{\mathcal{S}}$. Let us take a variable $p\in\mathcal{V}_{\mathcal{L}}\setminus\mathcal{V}(\alpha)$. By definition, $\emptyset\not\vdash_{\mathcal{S}}^{\circ}\alpha$ and $p\vdash_{\mathcal{S}}^{\circ}\alpha$. The former implies that there is a valuation $v$ in A such that $v[\alpha]\notin D$. Now we define a valuation:

[TABLE]

It is clear that $v^{\prime}[\alpha]=v[\alpha]$ and hence $p\not\models_{\textbf{M}}\alpha$.

Trying to find a characteristic for abstract logic to have an adequate matrix, we consider any logical matrix $\textsf{{M}}:=\langle\textsf{{A}},D\rangle$ of type $\mathcal{L}$.

Now, let $\alpha,\beta$ and $\gamma$ be $\mathcal{L}$-formulas with $(\mathcal{V}(\alpha)\cup\mathcal{V}(\beta))\cap\mathcal{V}(\gamma)=\emptyset$. Assume that for some valuation $v_{0}$, $v_{0}(\gamma)\in D$. (This assumption is equivalent to the condition that the set $\{\gamma\}$ is consistent w.r.t. the consequence relation $\models_{\textbf{M}}$.) We prove that

[TABLE]

Indeed, for contrapositive, suppose that $\alpha\not\models_{\textbf{M}}\beta$; that is, for some valuation $v$, $v(\alpha)\in D$, but $v(\beta)\notin D$.

Let us define a valuation

[TABLE]

We note that $v_{1}[\gamma]=v_{0}[\gamma]$, $v_{1}[\alpha]=v[\alpha]$ and $v_{1}[\beta]=v[\beta]$. This implies that $\gamma,\alpha\not\models_{\textbf{M}}\beta$.

The last consideration leads to the following definition.

Definition 4.1.1** (uniform abstract logic).**

An abstract logic $\mathcal{S}$ is said to be uniform if for any set $X\cup Y\cup\{\alpha\}$ of $\mathcal{L}$-formulas with $\mathcal{V}(X\cup\{\alpha\})\cap\mathcal{V}(Y)=\emptyset$ and $\textbf{Cn}_{\mathcal{S}}(Y)\neq\textit{{Fm}}_{\mathcal{L}}$, if $X,Y\vdash_{\mathcal{S}}\alpha$, then $X\vdash_{\mathcal{S}}\alpha$.

We note that the consequence relation $\models_{\textbf{B}_{2}}^{\circ}$ mentioned above is finitary but not uniform. (Exercise 4.1.1) The importance of the last definition becomes clear from Proposition 4.1.1 below. We prove this proposition by means of two lemmas.

Lemma 4.1.1**.**

If an abstract logic $\mathcal{S}$ has an adequate matrix, then $\mathcal{S}$ is uniform.

Proof.

Let a matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be adequate for $\mathcal{S}$. Suppose $X,Y\vdash_{\mathcal{S}}\alpha$, where $\mathcal{V}(X,\alpha)\cap\mathcal{V}(Y)=\emptyset$ and $\textbf{Cn}_{\mathcal{S}}(Y)\neq\textit{{Fm}}_{\mathcal{L}}$. We will show that $X\models_{\textbf{M}}\alpha$, which, in virtue of the adequacy of M for $\mathcal{S}$, will in turn imply that $X\vdash_{\mathcal{S}}\alpha$.

For contradiction, assume that for some valuation $v$ in A, $v[X]\subseteq D$ but $v[\alpha]\notin D$. Since $Y$ is consistent w.r.t. $\mathcal{S}$, there is a valuation $v^{\prime}$ such that $v^{\prime}[Y]\subseteq D$. Then, we define a valuation $v^{\prime\prime}$ as follows:

[TABLE]

It must be clear that $v^{\prime\prime}[\beta]=v[\beta]$, whenever $\beta\in X\cup\{\alpha\}$, and $v^{\prime\prime}[\beta]=v^{\prime}[\beta]$, if $\beta\in Y$. Therefore, $X,Y\not\models_{\textbf{M}}\alpha$; that is $X,Y\not\vdash_{\mathcal{S}}\alpha$. A contradiction. ∎

As preparation to the next proposition we observe the following.

Lemma 4.1.2**.**

Let $\mathcal{S}$ be a uniform structural abstract logic in a language $\mathcal{L}$ with $\textit{card}(\mathcal{V}_{\mathcal{L}})\geq\aleph_{0}$ and $\mathcal{L}^{+}$ be a primitive extension of $\mathcal{L}$. Then the abstract logic $(\mathcal{S})^{+}$ is also uniform.

Proof.

Suppose for a set $X\cup Y\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}^{+}}$, $X,Y\vdash_{(\mathcal{S})^{+}}\alpha$, providing that $\mathcal{V}(X\cup\{\alpha\})\cap\mathcal{V}(Y)=\emptyset$ and $Y$ is consistent w.r.t. $(\mathcal{S})^{+}$. Then, by definition, there is $X_{0}\cup Y_{0}\cup\{\beta\}\subseteq\textit{{Fm}}_{\mathcal{L}}$ and an $\mathcal{L}^{+}$-substitution $\sigma$ such that $\sigma(X_{0})\subseteq X$, $\sigma(Y_{0})\subseteq Y$, $\sigma(\beta)=\alpha$ and $X_{0},Y_{0}\vdash_{\mathcal{S}}\beta$. It is clear that $\mathcal{V}(X_{0}\cup\{\beta\})\cap\mathcal{V}(Y_{0})=\emptyset$. Also, $Y_{0}$ is consistent w.r.t. $\mathcal{S}$, for if it were otherwise, in virtue of conservativity of $(\mathcal{S})^{+}$ over $\mathcal{S}$, we would have $\sigma(Y_{0})\vdash_{(\mathcal{S})^{+}}\gamma$, for any arbitrary $\mathcal{L}^{+}$-formula $\gamma$. This would imply the inconsistency of $Y$ in $(\mathcal{S})^{+}$.

Since $\mathcal{S}$ is uniform, $X_{0}\vdash_{\mathcal{S}}\beta$ and hence $X_{0}\vdash_{(\mathcal{S})^{+}}\beta$, for $(\mathcal{S})^{+}$ is a conservative extension of $\mathcal{S}$. And since $(\mathcal{S})^{+}$ is structural (Proposition LABEL:P:(S)_plus), $\sigma(X_{0})\vdash_{(\mathcal{S})^{+}}\alpha$ and hence $X\vdash_{(\mathcal{S})^{+}}\alpha$. ∎

Proposition 4.1.1** (Loś-Suszko-Wójcicki theorem).**

Let $\mathcal{S}$ be a finitary structural abstract logic in a language $\mathcal{L}$ with $\textit{card}(\mathcal{V}_{\mathcal{L}})\geq\aleph_{0}$. Then $\mathcal{S}$ has an adequate matrix if, and only if, $\mathcal{S}$ is uniform.

Proof.

The “only-if” part follows from Lemma 4.1.1. So we continue with the proof of the “if” part.

We distinguish two cases: $\mathcal{S}$ is trivial and $\mathcal{S}$ is nontrivial. If the former is the case, then the matrix $\langle\textit{{Fm}}_{\mathcal{L}},\textit{{Fm}}_{\mathcal{L}}\rangle$ is adequate for $\mathcal{S}$.

Now, we assume that $\mathcal{S}$ is nontrivial; that is, the set $\Sigma_{\mathcal{S}}^{c}$ of consistent sets w.r.t. $\mathcal{S}$ is nonempty.

We introduce for each $X\in\Sigma_{\mathcal{S}}^{c}$ and each $p\in\mathcal{V}_{\mathcal{L}}$, a new sentential variable $p_{X}$ so that for any $p,q\in\mathcal{V}_{\mathcal{L}}$ and any $X,Y\in\Sigma_{\mathcal{S}}^{c}$,

[TABLE]

Accordingly, for an arbitrary $X\in\Sigma_{\mathcal{S}}^{c}$, we denote:

[TABLE]

Thus for any $X,Y\in\Sigma_{\mathcal{S}}^{c}$,

[TABLE]

A language $\mathcal{L}^{+}$ is defined as a primitive extension of $\mathcal{L}$, by adding the new sentential variables to $\mathcal{V}_{\mathcal{L}}$. Then, we introduce $(\mathcal{S})^{+}$ according to Definition 3.5.2.

Next, for each $X\in\Sigma_{\mathcal{S}}^{c}$, we define two $\mathcal{L}^{+}$-substitutions:

[TABLE]

We observe: for any $X\in\Sigma_{\mathcal{S}}^{c}$,

[TABLE]

Then, we make two observations. First, since for any $X\in\Sigma_{\mathcal{S}}^{c}$, $\mathcal{V}(\sigma_{X}(X))\subseteq\mathcal{V}_{X}$, (4.1) yields that for any $X,Y\in\Sigma_{\mathcal{S}}^{c}$,

[TABLE]

Second,

[TABLE]

Indeed, for contradiction, assume that $\sigma_{X}(X)$ is inconsistent. Let $\beta$ be any formula of $\textit{{Fm}}_{\mathcal{L}}$. By assumption, $\sigma_{X}(X)\vdash_{(\mathcal{S})^{+}}\sigma_{X}(\beta)$. Since $(\mathcal{S})^{+}$ is structural (Proposition 3.5.4), we have that $\xi_{X}(\sigma_{X}(X))\vdash_{(\mathcal{S})^{+}}\xi_{X}(\sigma_{X}(\beta))$ and hence, in virtue of (4.2), $X\vdash_{(\mathcal{S})^{+}}\beta$. Since $(\mathcal{S})^{+}$ is conservative over $\mathcal{S}$, we obtain that $X\vdash_{\mathcal{S}}\beta$. A contradiction.

Now, we define:

[TABLE]

We aim to show that M is adequate for $\mathcal{S}$; that is, for any set $Y\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$,

[TABLE]

Suppose $Y\vdash_{\mathcal{S}}\alpha$. Since $(\mathcal{S})^{+}$ is conservative over $\mathcal{S}$, this implies that $Y\vdash_{(\mathcal{S})^{+}}\alpha$. Now, let $\sigma$ be any $\mathcal{L}^{+}$-substitution. Assume that $\sigma(Y)\subseteq\textbf{Cn}_{(\mathcal{S})^{+}}(\bigcup\{\sigma_{X}(X)\leavevmode\nobreak\ |\leavevmode\nobreak\ X\in\Sigma_{\mathcal{S}}^{c}\})$. Since $(\mathcal{S})^{+}$ is structural, we have: $\sigma(\alpha)\in\textbf{Cn}_{(\mathcal{S})^{+}}(\sigma(Y))$ and hence $\sigma(\alpha)\in\textbf{Cn}_{(\mathcal{S})^{+}}(\bigcup\{\sigma_{X}(X)\leavevmode\nobreak\ |\leavevmode\nobreak\ X\in\Sigma_{\mathcal{S}}^{c}\})$.

Conversely, suppose that $Y\not\vdash_{\mathcal{S}}\alpha$. We denote:

[TABLE]

Thus $\alpha\notin X_{0}$ and hence $X_{0}\in\Sigma_{\mathcal{S}}^{c}$. The latter implies that $\sigma_{X_{0}}(X_{0})\subseteq\textbf{Cn}_{(\mathcal{S})^{+}}(\bigcup\{\sigma_{X}(X)\leavevmode\nobreak\ |\leavevmode\nobreak\ X\in\Sigma_{\mathcal{S}}^{c}\})$.

For contradiction, we assume that

[TABLE]

In virtue of finitariness of $(\mathcal{S})^{+}$ (Proposition 3.5.5), there is a finite number of sets $X_{1},\ldots,X_{n}\in\Sigma_{\mathcal{S}}^{c}$ such that

[TABLE]

Since, according to (4.4), $\sigma_{X_{n}}(X_{n})$ is consistent and

[TABLE]

in virtue of the uniformity of $(\mathcal{S})^{+}$ (Lemma 4.1.2),

[TABLE]

Repeating this argument several times, we arrive at the conclusion that $\sigma_{X_{0}}(X_{0})\vdash_{(\mathcal{S})^{+}}\sigma_{X_{0}}(\alpha)$. Then, applying the substitution $\xi_{X_{0}}$, we get $X_{0}\vdash_{(\mathcal{S})^{+}}\alpha$. Finally, the conservativity of $(\mathcal{S})^{+}$ over $\mathcal{S}$ yields $X_{0}\vdash_{\mathcal{S}}\alpha$. A contradiction. ∎

The case of nonfinitary abstract logics needs an additional investigation.

Definition 4.1.2** (couniform abstract logic).**

An abstract logic $\mathcal{S}$ in a language $\mathcal{L}$ is called couniform if for any collection $\{X_{i}\}_{i\in I}$ of formula sets with $\mathcal{V}(X_{i})\cap\mathcal{V}(X_{j})=\emptyset$, providing that $i\neq j$, and $\mathcal{V}(\bigcup_{i\in I}\{X_{i}\})\neq\mathcal{V}_{\mathcal{L}}$, there is at least one $X_{i}$ which is inconsistent, whenever the union $\bigcup_{i\in I}\{X_{i}\}$ is inconsistent.

The next lemma shows that couniformity is necessary for an abstract logic to have an adequate matrix.

Lemma 4.1.3**.**

If and abstract logic $\mathcal{S}$ has an adequate matrix, then $\mathcal{S}$ is couniform.

Proof.

Let a matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be adequate for $\mathcal{S}$. We assume that a family $\{X_{i}\}_{i\in I}$ of formula sets satisfies all the premises of couniformity. Suppose each $X_{i}$ is consistent w.r.t. $\mathcal{S}$. Then for each $i\in I$, there is a formula $\alpha_{i}$ such that $X_{i}\not\vdash_{\mathcal{S}}\alpha_{i}$. This implies that there is a valuation $v_{i}$ in A such that $v_{i}[X_{i}]\subseteq D$ but $v_{i}[\alpha_{i}]\notin D$. Let us select either one of $v_{i}[\alpha_{i}]$ and denote

[TABLE]

Then, we select any variable $p\in\mathcal{V}_{\mathcal{L}}\setminus\mathcal{V}(\bigcup_{i\in I}\{X_{i}\})$ and for each $v_{i}$, define:

[TABLE]

It must be clear that for each $i\in I$, $v_{i}^{\ast}[X_{i}]\subseteq D$. And since $\mathcal{V}(X_{i})\cap\mathcal{V}(X_{j})=\emptyset$, providing $i\neq j$, we also have that $v_{i}^{\ast}[\bigcup_{i\in I}\{X_{i}\}]\subseteq D$. Thus $\bigcup_{i\in I}\{X_{i}\}\not\vdash_{\mathcal{S}}p$, that is the set $\bigcup_{i\in I}\{X_{i}\}$ is consistent. ∎

The next lemma is rather technical and we will need it for the proof of Proposition 4.1.2 below.

Lemma 4.1.4**.**

Let $\mathcal{S}$ be a couniform structural abstract logic in a language $\mathcal{L}$ with $\textit{card}(\mathcal{V}_{\mathcal{L}})\geq\aleph_{0}$ and $\mathcal{L}^{+}$ be a primitive extension of $\mathcal{L}$. Then the abstract logic $(\mathcal{S})^{+}$ is also couniform.

Proof.

Let $\{X_{i}\}_{i\in I}$ be a nonempty family of nonempty sets of $\mathcal{L}^{+}$-formulas, about which we assume that the union $\bigcup_{i\in I}\{X_{i}\}$ is inconsistent and $\mathcal{V}(\bigcup_{i\in I}\{X_{i}\})\neq\mathcal{V}_{\mathcal{L}^{+}}$. Let us select any $p\in\mathcal{V}_{\mathcal{L}^{+}}\setminus\mathcal{V}(\bigcup_{i\in I}\{X_{i}\})$. Since $\bigcup_{i\in I}\{X_{i}\}$ is inconsistent, we have that $\bigcup_{i\in I}\{X_{i}\}\vdash_{(\mathcal{S})^{+}}p$. By definition of $(\mathcal{S})^{+}$ (Definition 3.5.2), there are a set $Y$ of $\mathcal{L}$-formulas, an $\mathcal{L}$-variable $q$ and an $\mathcal{L}$-substitution $\sigma$ such that $\sigma(Y)\subseteq\bigcup_{i\in I}\{X_{i}\}$, $\sigma(q)=p$ and $Y\vdash_{\mathcal{S}}q$.

Next we define: for each $i\in I$,

[TABLE]

Firstly, we notice that for each $i\in I$, $\sigma(Y_{i})\subseteq X_{i}$, and $\bigcup_{i\in I}\{Y_{i}\}\vdash_{\mathcal{S}}q$. (The latter is true because $\bigcup_{i\in I}\{Y_{i}\}=Y$.) Secondly, $q\in\mathcal{V}_{\mathcal{L}}\setminus\mathcal{V}(\bigcup_{i\in I}\{Y_{i}\})$. Indeed, if it were the case that $q\in\mathcal{V}(\bigcup_{i\in I}\{Y_{i}\})$, then we would have that $p\in\mathcal{V}(\bigcup_{i\in I}\{X_{i}\})$.

Thus we obtain that $\bigcup_{i\in I}\{Y_{i}\}$ is inconsistent w.r.t. $\mathcal{S}$. Since, by definition, $\mathcal{S}$ is couniform, there is $i_{0}\in I$ such that $Y_{i_{0}}$ is inconsistent w.r.t. $\mathcal{S}$. This implies that Since $(\mathcal{S})^{+}$ is a conservative extension of $\mathcal{S}$, we receive that $Y_{i_{0}}\vdash_{(\mathcal{S})^{+}}q$. And since $(\mathcal{S})^{+}$ is structural (Proposition 3.5.4), $\sigma(Y_{i_{0}})\vdash_{(\mathcal{S})^{+}}p$ and hence $X_{i_{0}}\vdash_{(\mathcal{S})^{+}}p$. We recall that $p\notin\mathcal{V}(X_{i_{0}})$. Therefore, the structurality of $(\mathcal{S})^{+}$ implies that $X_{i_{0}}$ is inconsistent. ∎

Proposition 4.1.2** (Wójcicki theorem).**

Let $\mathcal{S}$ be a structural abstract logic in a language $\mathcal{L}$ with $\textit{card}(\mathcal{V}_{\mathcal{L}})\geq\aleph_{0}$. Then $\mathcal{S}$ has an adequate matrix if, and only if, $\mathcal{S}$ is both uniform and couniform.

Proof.

The “only-if” part follows from Lemmas 4.1.1 and 4.1.3.

The proof of the “if” part repeats the steps of the “if” part of the proof of the Loś-Suszko theorem (Proposition 4.1.1) up to the assumption $(\ast)$. Then, we continue as follows.

First, we notice that, in virtue of (4.4) and of the couniformity of $(\mathcal{S})^{+}$ (Lemma 4.1.4), the set $\bigcup\{\sigma_{X}(X)\leavevmode\nobreak\ |\leavevmode\nobreak\ X\in\Sigma_{\mathcal{S}}^{c}\}$ is consistent. Thus, we have:

[TABLE]

where the set $\bigcup\{\sigma_{X}(X)\leavevmode\nobreak\ |\leavevmode\nobreak\ X\in\Sigma_{\mathcal{S}}^{c}\leavevmode\nobreak\ \text{and}\leavevmode\nobreak\ X\neq X_{0}\}$ is consistent w.r.t. $(\mathcal{S})^{+}$.

Let us denote

[TABLE]

With the help of (4.1) and (4.3), we conclude that $\mathcal{V}(\sigma_{X_{0}}(X_{0})\cup\{\sigma_{X_{0}}(\alpha)\})\cal\mathcal{V}(Y_{0})=\emptyset$. Then, using the uniformity of $(\mathcal{S})^{+}$, we derive that $\sigma_{X_{0}}(\alpha)\vdash_{(\mathcal{S})^{+}}\sigma_{X_{0}}(\alpha)$. This, in virtue of structurality of $(\mathcal{S})^{+}$ (Proposition 3.5.4), implies that $\xi_{X_{0}}(\sigma_{X_{0}}(\alpha))\vdash_{(\mathcal{S})^{+}}\xi_{X_{0}}(\sigma_{X_{0}}(\alpha))$ and hence, according to (4.2), $X_{0}\vdash_{(\mathcal{S})^{+}}\alpha$. Because of the conservativeness of $(\mathcal{S})^{+}$ over $\mathcal{S}$, the latter leads to $X_{0}\vdash_{\mathcal{S}}\alpha$. A contradiction. ∎

Exercises 4.1

Prove that the relation $\models_{\textbf{B}_{2}}^{\circ}$ obtained from $\models_{\textbf{B}_{2}}$ according to (4) is finitary but not uniform.

4.2 Finitary matrix consequence

Given a (nonempty) class $\mathcal{M}$ of $\mathcal{L}$-matrices, an abstract logic $\mathcal{S}_{\mathcal{M}}$, according to Proposition 3.3.3, is structural and, according to Corollary 3.3.5.2, is determined by the class of all $\mathcal{S}_{\mathcal{M}}$-models. The last class definitely contains $\mathcal{M}$. For the purpose of this section, it will not be an exaggeration to assume that $\mathcal{M}$ coincides with the class of all $\mathcal{S}_{\mathcal{M}}$-models. Under this assumption, the question arises: What characteristics should $\mathcal{M}$ have in order for $\mathcal{S}_{\mathcal{M}}$ to be finitary? Proposition 4.2.2 below proposes an answer to this question.

However, first we discuss the property that the matrix consequence of any finite matrix is finitary. To prove this, we use topological methods discussed in Section 1.1.

Let $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ be a finite logical matrix of type $\mathcal{L}$ and let $V_{\textsf{{A}}}:=\textsf{{A}}^{\mathcal{V}_{\mathcal{L}}}$ (the set of all valuations in algebra A). We regard $|\textsf{{A}}|$ as a finite topological space with discrete topology and $V_{\textsf{{A}}}$ as the cartesian power of the space $|\textsf{{A}}|$ relative to the product topology. According to Corollary 1.1.2.1, the space $V_{\textsf{{A}}}$ is compact.

For any formula $\alpha\in\textit{{Fm}}_{\mathcal{L}}$, we denote:

[TABLE]

We aim to show that each $V_{\textsf{{A}}}(\alpha)$ is open and closed in $V_{\textsf{{A}}}$. The idea is that, since an arbitrary formula $\alpha$ contains finitely many sentential variables and the set $|\textsf{{A}}|$ is finite, there are only finitely many restricted assignments that validate $\alpha$ and there are finitely many restricted assignments that refute it in M.

We show that each $V_{\textsf{{A}}}(\alpha)$ is an open set in the product topology. The closedness of it, that is the openness of its complement, is similar.

Given an arbitrary formula $\alpha$, we define a binary relation on $V_{\textsf{{A}}}(\alpha)$ as follows:

[TABLE]

It is clear that the relation $\equiv$ is an equivalence. For any $v\in V_{\textsf{{A}}}(\alpha)$, we denote:

[TABLE]

It is well know that $\{|v|\leavevmode\nobreak\ |\leavevmode\nobreak\ v\in V_{\textsf{{A}}}(\alpha)\}$ is a partition of $V_{\textsf{{A}}}(\alpha)$. If we show that each $|v|$ is open in the product topology, so will be $V_{\textsf{{A}}}(\alpha)$.

We observe that

[TABLE]

where

[TABLE]

According to the description (1.1) of the product topology in Section 1.1, this demonstrates that each $|v|$ is open. In a similar manner, we prove that each

[TABLE]

is also open.

Now, assume that for a set $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$, $X\models_{\textbf{M}}\alpha$. This implies (is even equivalent to) that $\bigcap_{\beta\in X}V_{\textsf{{A}}}(\beta)\subseteq V_{\textsf{{A}}}(\alpha)$. The last inclusion in turn is equivalent to the following:

[TABLE]

This means that $\{V_{\textsf{{A}}}(\alpha\}\cup\{(V_{\textsf{{A}}}\setminus V_{\textsf{{A}}}(\beta))\}_{\beta\in X}$ is an open cover of $V_{\textsf{{A}}}$. Since the space $V_{\textsf{{A}}}$ is compact, it has a finite subcover $\{V_{\textsf{{A}}}(\alpha\}\cup\{(V_{\textsf{{A}}}\setminus V_{\textsf{{A}}}(\beta))\}_{\beta\in Y}$, for some $Y\Subset X$. The latter is equivalent to $Y\models_{\textbf{M}}\alpha$.

Thus we have proved the following.

Proposition 4.2.1**.**

A single matrix consequence relative to a finite matrix is finitary.

Corollary 4.2.1.1**.**

Let $\mathcal{M}$ be a nonempty finite family of finite matrices of type $\mathcal{L}$. Then the $\mathcal{M}$-consequence is finitary.

Proof is left to the reader. (Exercise 4.1.1)

Now we turn to a more general case.

Proposition 4.2.2** (Bloom-Zygmunt criterion).**

Let $\mathcal{M}$ be the class of all models of an abstract logic $\mathcal{S}$ in $\mathcal{L}$. Then $\mathcal{S}$ is finitary if, and only if, the class $\mathcal{M}$ is closed w.r.t. ultraproducts.

Proof.

Suppose $\mathcal{S}$ is finitary. Then, according to Corollary 3.4.1.2, there is a set $\mathcal{R}$ of modus rules such that $\mathcal{S}=\mathcal{S}_{\mathcal{R}}$. Thus, $\mathcal{M}$ is the class of all $\mathcal{S}_{\mathcal{R}}$-models. Then, in virtue of Corollary 3.4.2.1, $\mathcal{M}$ is closed under ultraproducts.

Next, let the class $\mathcal{M}$ be closed w.r.t. ultraproducts. For contradiction, assume that $\mathcal{S}$ is not finitary. That is, for some set $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$, $\alpha\in\textbf{Cn}_{\mathcal{S}}(X)$ but for any $Y\Subset X$, $\alpha\notin Y$.

We denote:

[TABLE]

and for any $Y\in I$,

[TABLE]

We observe that for any $Y_{1},\ldots,Y_{n}\in I$,

[TABLE]

That is, the set $\{\langle Y\rangle\leavevmode\nobreak\ |\leavevmode\nobreak\ Y\in I\}$ has the finite intersection property. According to the Ultrafilter Theorem ([CK90], proposition 4.1.3), there is an ultrafilter $\nabla$ over $I$ such that

[TABLE]

Given an $\mathcal{L}$-formula $\beta\in X$, we note that

[TABLE]

This, in view of (4.5), implies that for arbitrary formula $\beta\in X$,

[TABLE]

Using the notation $\textsf{{Lin}}_{\,\mathcal{S}}[Y]:=\langle\mathfrak{F}_{\mathcal{L}},\textbf{Cn}_{\mathcal{S}}(Y)\rangle$ (Section 3.3.2), we define:

[TABLE]

Thus

[TABLE]

where a set $D\subseteq|(\mathfrak{F}_{\mathcal{L}})^{I}/\nabla|$ and such that for any $\theta\in|(\mathfrak{F}_{\mathcal{L}})^{I}|$,

[TABLE]

For any $\mathcal{L}$-formula $\beta$, we define:

[TABLE]

and then, for any $\beta\in\textit{{Fm}}_{\mathcal{L}}$,

[TABLE]

It must be clear that $v:\mathfrak{F}_{\mathcal{L}}\longrightarrow(\mathfrak{F}_{\mathcal{L}})^{I}/\nabla$ is a homomorphism and, hence, can be regarded as an assignment of the $\mathcal{L}$-formulas in $(\mathfrak{F}_{\mathcal{L}})^{I}/\nabla$.

We aim to show that $v[X]\subseteq D$ but $v[\alpha]\notin D$. This will imply that M is not an $\mathcal{S}$-model and hence does not belong to $\mathcal{M}$. The latter in turn will implies that $\mathcal{M}$ is not closed under ultraproducts, which is contrary to the assumption.

Indeed, it follows from (4.7) and (4.6) that for any $\beta\in X$,

[TABLE]

On the other hand,

[TABLE]

Therefore, in view of (4.7), $v[\alpha]=\overline{\alpha}/\nabla\notin D$. ∎

Exercises 4.2

Prove Corollary 4.2.1.1.

4.3 The conception of separating means

Considering an abstract logic $\mathcal{S}$ as a consequence relation $\vdash_{\mathcal{S}}$, there are two main tasks: to confirm $X\vdash_{\mathcal{S}}\alpha$ or to refute it. Given a finitary abstract logic $\mathcal{S}$, these two tasks can be regarded as one twofold problem (of extreme importance): Is there an algorithm that for any set $X\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}}$, decides whether $X\vdash_{\mathcal{S}}\alpha$ is true or false.

Trying to confirm $X\vdash_{\mathcal{S}}\alpha$, one can use rules of inference (sound w.r.t. $\mathcal{S}$) or a suitable adequate matrix or a set of matrices which determine $\mathcal{S}$. On the other hand, to refute $X\vdash_{\mathcal{S}}\alpha$, we need “means” that would separate $X$ from $\alpha$, for any $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$ or at least for any $X\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}}$. According to Corollary 3.3.5.1, the Lindenbaum atlas for $\mathcal{S}$ is a universal tool, for it works, at least in principal, for both tasks. However, it is too complicated and can be used mainly to prove very general theorems. For the refutation task, the Lindenbaum atlas is very inefficient. Nevertheless, in many cases, as we will see, it can be simplified to an extent to be useful.

A general view on the conception of separating means was formulated by A. Kuznetsov [Kuz79]. According to him, if all formulas of a set $X$ stand in a relation $R$ to an object $\mathfrak{A}$, but a formula $\alpha$ does not stand in $R$ to $\mathfrak{A}$, we say that $\mathfrak{A}$ separates $X$ from $\alpha$ w.r.t. $R$. In this case, the character of the relation $R$ must be such that from the separation of $X$ from $\alpha$ it follows that $X\vdash_{\mathcal{S}}\alpha$ does not hold.111The conception of separating means, proposed by Kuznetsov, was intended to be applied not only to the issue of derivability, but also to that of expressibility understood within the framework of a given calculus. He also emphasized that the object $\mathfrak{A}$ which was employed as a separating means in the above sense has often been of algebraic nature.

While the Lindenbaum atlas relative to an abstract logic $\mathcal{S}$ can play a role of universal separating means, but for a particular pair $X$ and $\alpha$, in case $X\vdash_{\mathcal{S}}\alpha$ does not hold, potentially any $\mathcal{S}$-matrix can be a separating means. Therefore, it would be interesting to find an algebraic connection between the Lindenbaum atlas or Lindenbaum matrix relative to $\mathcal{S}$ and any $\mathcal{S}$-matrix. This will be the topic of the next chapter.

Chapter 5 Unital Abstract Logics

5.1 Unital algebraic expansions

From the discussion in Section 4.3, the following questions arise.

(1)

Is there a regular method of simplifying the Lindenbaum atlas (Lindenbaum matrix) relative to an abstract logic $\mathcal{S}$ to obtain an adequate atlas (or matrix), or at least weakly adequate matrix that would be a more convenient separating means than $\textsf{{Lin}}[\Sigma_{\mathcal{S}}]$ or $\textsf{{Lin}}_{\mathcal{S}}$?

(2)

Is there a regular method of simplifying the Lindenbaum atlas (Lindenbaum matrix) relative to an abstract logic $\mathcal{S}$ to have a connection between these simplified forms of $\textsf{{Lin}}[\Sigma_{\mathcal{S}}]$ or $\textsf{{Lin}}_{\mathcal{S}}$ and other $\mathcal{S}$-atlases and $\mathcal{S}$-matrices, respectively?

As to the question the question $\bm{(1)}$, even any finite matrix generates abstract logic, the Lindenbaum matrix of which is always infinite, for the cardinality of any Lindenbaum matrix equals the cardinality of the set of formulas. Take, for instance, the matrix $\textsf{{B}}_{2}$ of Section 2.2.1. We showed (Section 3.3.3) that $\textsf{{B}}_{2}$ is adequate for the consequence relation $\vdash_{2}$. We denote the corresponding abstract logic by Cl. Even a rough comparison between $\textsf{{Lin}}_{\textsf{Cl}}$ and $\textsf{{B}}_{2}$ demonstrates the difference between their complexities.

One thing is remarkable about the logical matrices discussed in Sections 2.2.1–2.2.5. The logical filters of all of them consist of a single element. A logical matrix $\textsf{{M}}=\langle\textsf{{A}},D\rangle$ is called unital if $D$ is a one-element set. We denote the designated element of a unital matrix by $\mathbf{1}$ (perhaps with subscript). Thus, if $\textsf{{M}}=\langle\textsf{{A}},\{\mathbf{1}\}\rangle$, we can consider the algebra $\langle\textsf{{A}},\mathbf{1}\rangle$ as a semantics for $\mathcal{L}$-formulas. We call $\langle\textsf{{A}},\mathbf{1}\rangle$ a unital expansion of A. Very often, such an expansion is not needed. Namely, when $D=\{c\}$, where $c$ is a constant from the signature of A, we count that $\mathbf{1}=c$.

Thus, in case M is unital, instead of saying that an $\mathcal{L}$-formula $\alpha$ is valid in M, we say that $\alpha$ is valid in $\langle\textsf{{A}},\mathbf{1}\rangle$, meaning that for any valuation $v$ in A, $v[\alpha]=\mathbf{1}$. Further, given a unital expansion $\langle\textsf{{A}},\mathbf{1}\rangle$, for any set $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$, we define:

[TABLE]

The last definition allows us to adopt the definition of $\mathcal{S}$-model to algebras $\langle\textsf{{A}},\mathbf{1}\rangle$. Namely such an algebra is an (algebraic) $\mathcal{S}$-model if for any set $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$,

[TABLE]

Further, we say that an algebra $\langle\textsf{{A}},\mathbf{1}\rangle$ is **adequate **for an abstract logic $\mathcal{S}$ if for any set $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}}$,

[TABLE]

and that A is weakly adequate for $\mathcal{S}$ if for any $\alpha\in\textit{{Fm}}_{\mathcal{L}}$,

[TABLE]

Finally, the definition of $\mathcal{M}$-consequence (Section 3.3.2) can be adopted for the case when $\mathcal{M}=\{\langle\textsf{{A}}_{i},\mathbf{1}_{i}\rangle\}_{i\in I}$. Namely for such a class $\mathcal{M}$, we define:

[TABLE]

Abstract logics which can be defined as the $\mathcal{M}$-consequence of this type are called assertional; see [Fon16], definition 3.5.

It will be convenient to treat the validity of an $\mathcal{L}$-formula $\alpha$ in $\langle\textsf{{A}},\mathbf{1}\rangle$ as the validity of a first order formula in a first order model.

Namely, given a sentential language $\mathcal{L}$, we define a first order language $\textbf{FO}_{\mathcal{L}}^{\ast}$ whose individual variables are the sentential variables of $\mathcal{L}$ and the connectives of $\mathcal{F}_{\mathcal{L}}$ and the constants of $\mathcal{C}_{\mathcal{S}}$ are the functional symbols. (The constant symbols are treated as 0-ary functional symbols). In addition, $\textbf{FO}_{\mathcal{L}}^{\ast}$ has a 0-ary functional symbol $\mathbf{1}$ which is interpreted in the $\textbf{FO}_{\mathcal{L}}^{\ast}$-models by a constant $\mathbf{1}$. Also, $\textbf{FO}_{\mathcal{L}}^{\ast}$ has symbol ‘$\approx$’ which is interpreted in the $\textbf{FO}_{\mathcal{L}}^{\ast}$-models as equality, the first order logical connectives $\&$ (conjunction), $\Rightarrow$ (implication) and universal quantifier $\forall$. The parentheses ‘(’ and ‘)’ are used in the usual way.

Thus each $\mathcal{L}$-formula becomes in $\textbf{FO}_{\mathcal{L}}^{\ast}$ a term. In addition, $\textbf{FO}_{\mathcal{L}}^{\ast}$ has terms like $\alpha(p,\ldots,\mathbf{1},\ldots,q)$ obtained from $\alpha(p,\ldots,r,\ldots,q)$ by replacement of a variable $r$ with the constant $\mathbf{1}$.

The atomic formulas of $\textbf{FO}_{\mathcal{L}}^{\ast}$, called also equalities, are the expressions of the form:

[TABLE]

where $\mathfrak{r}$ and $\mathfrak{t}$ are $\textbf{FO}_{\mathcal{L}}^{\ast}$-terms.

Thus $\textbf{FO}_{\mathcal{L}}^{\ast}$ as a logical system is a first order logic with equality.

Given an $\textbf{FO}_{\mathcal{L}}^{\ast}$-formula $\phi$, its universal closure is denoted by

[TABLE]

The universal closure of an equality is often referred to as an identity. Given equalities $\phi,\phi_{1},\ldots,\phi_{n}$, the formula

[TABLE]

is called a quasiidentity.

With each expansion $\langle\textsf{{A}},\mathbf{1}\rangle$ we associate an $\textbf{FO}_{\mathcal{L}}^{\ast}$-model $\mathfrak{A}=\langle\textsf{{A}},\mathbf{1},\approx\rangle$ so that, talking about validity of identities and quasiidentities in $\mathfrak{A}$, we, abusing notation, will be writing

[TABLE]

instead of, respectively, $\mathfrak{A}\models\forall\ldots\forall\alpha(p,\mathbf{1},\ldots)\approx\beta(q,\mathbf{1},\ldots)$ and

$\mathfrak{A}\models\forall\ldots\forall((\phi_{1}\&\ldots\&\phi_{n})\Rightarrow\phi)$. Thus, it must be clear that for any $\mathcal{L}$-formula $\alpha$ and any $\textbf{FO}_{\mathcal{L}}^{\ast}$-model $\mathfrak{A}=\langle\textsf{{A}},\mathbf{1},\approx\rangle$,

[TABLE]

Let $X:=\{\alpha_{1},\ldots,\alpha_{n}\}$. We denote:

[TABLE]

Thus, in this notation, for any set $X\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}}$, we can observe that

[TABLE]

(If $X=\emptyset$, we understand the last equivalence as (5.1).)

Proposition 5.1.1**.**

Let $\mathcal{S}$ be a finitary abstract logic. Then all algebraic $\mathcal{S}$-models form a quasivariety.

Proof.

Indeed, let $\left\langle\textsf{{A}},\mathbf{1}\right\rangle$ be a unital algebraic expansion. Then, since $\mathcal{S}$ is finitary, $\left\langle\textsf{{A}},\mathbf{1}\right\rangle$ is an $\mathcal{S}$-model if, and only if, $\left\langle\textsf{{A}},\mathbf{1},\approx\right\rangle\models X\approx\mathbf{1}\Rightarrow\alpha\approx\mathbf{1}$, for any $X\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}}$ such that $X\vdash_{\mathcal{S}}\alpha$. ∎

Remark. We note that there are finitary abstract logics $\mathcal{S}$ which are not determined by their algebraic $\mathcal{S}$-models. For instance, let $\mathcal{S}^{\to}$ be the abstract logic in a language containing only one connective $\to$ and no other constants, defined by premiseless rule $\bm{\alpha}\to\bm{\alpha}$ and modus ponens. Then $\mathcal{S}^{\to}$ has no adequate finite matrix and is not determined by any nonempty set of unital matrices; see [MT48], p. 6, and [Men15], exercise 1.52, and [Fon16], example 6.78.

5.2 Unital abstract logics

Given a set $X\subseteq\textit{{Fm}}_{\mathcal{L}}$, we denote by $\theta(X)$ the congruence on $\mathfrak{F}_{\mathcal{L}}$, generated by the set $X\times X$. We will be interested in congruences $\theta(D)$, where $D$ is a theory of an abstract logic $\mathcal{S}$, in particular in congruences $\theta(\bm{T}_{\mathcal{S}})$.

The following observation will be useful in the sequel.

Proposition 5.2.1**.**

A structural abstract logic $\mathcal{S}$ is nontrivial if, and only if, it satisfies the following property: For any $p,q\in\mathcal{V}_{\mathcal{L}}$,

[TABLE]

Proof.

To prove the ‘only-if’ part, we assume that $\mathcal{S}$ is nontrivial. Then, since $\mathcal{S}$ is structural, $\bm{T}_{\mathcal{S}}$ does not contain sentential variables. Let $M$ be the congruence class w.r.t. $\theta(\bm{T}_{\mathcal{S}})$, which contains the variable $p$. Now, we define: $M_{1}:=\{p\}$ and $M_{2}:=M\setminus\{p\}$. The new partition of $\textit{{Fm}}_{\mathcal{L}}$ induces the equivalence $\theta$. It is obvious that $\theta\subset\theta(\bm{T}_{\mathcal{S}})$. We will show that $\theta$ is a congruence on $\mathfrak{F}_{\mathcal{L}}$.

Let $F$ be an arbitrary $n$-ary connective with $n\geq 1$. Assume that for formulas $\alpha_{1},\ldots,\alpha_{n},\beta_{1},\ldots,\beta_{n}$, each pair $(\alpha_{i},\beta_{i})\in\theta$. Then each pair $(\alpha_{i},\beta_{i})\in\theta(\bm{T}_{\mathcal{S}})$ and hence $(F\alpha_{1}\ldots\alpha_{n},F\beta_{1}\ldots\beta_{n})\in\theta(\bm{T}_{\mathcal{S}})$. This means that either both $F\alpha_{1}\ldots\alpha_{n}$ and $F\beta_{1}\ldots\beta_{n}$ belong to $M_{2}$ or they belong to a class of $\theta(\bm{T}_{\mathcal{S}})$ that is different from $M$ and hence is a class of $\theta$. This implies that $\{p\}$ and $\{q\}$ are two distinct congruence classes w.r.t. $\theta(\bm{T}_{\mathcal{S}})$.

Conversely, suppose the implication (5.3) holds. Then, since one of the congruence classes w.r.t. $\theta(\bm{T}_{\mathcal{S}})$ contains $\bm{T}_{\mathcal{S}}$ and there are more than two classes, $\bm{T}_{\mathcal{S}}\neq\textit{{Fm}}_{\mathcal{L}}$. ∎

5.2.1 Definition and some properties

Definition 5.2.1** (unital abstract logic).**

A structural abstract logic $\mathcal{S}$ is called unital if any $\mathcal{S}$-theory $D$ is a congruence class w.r.t. the congruence $\theta(D)$.

Since any congruence class cannot be empty, from Definition 5.2.1 and Proposition 5.2.1, we immediately obtain the following.

Proposition 5.2.2**.**

For any unital abstract logic $\mathcal{S}$, $\bm{T}_{\mathcal{S}}\neq\emptyset$; in addition, $\mathcal{S}$ is nontrivial if, and only, (5.3) holds.

As we will see below (Corollary 5.2.3.2), the unitality of an abstract logic is connected to the following concept.

Definition 5.2.2**.**

Let $X\subseteq\textit{{Fm}}_{\mathcal{L}}$ and $X\neq\emptyset$. A congruence $\theta$ on $\mathfrak{F}_{\mathcal{L}}$ is said to be compatible with $X$ if for any $(\alpha,\beta)\in\theta$,

[TABLE]

in other words, $X$ is the union of congruence classes w.r.t. $\theta$.

It is obvious that

[TABLE]

is a congruence of $\mathfrak{F}_{\mathcal{L}}$, which is compatible with any nonempty set $X\subseteq\textit{{Fm}}$.

Proposition 5.2.3**.**

Let $X\subseteq\textit{{Fm}}_{\mathcal{L}}$ and $X\neq\emptyset$. For any congruence $\theta$ on $\mathfrak{F}_{\mathcal{L}}$, $X$ is a congruence class w.r.t. $\theta$ if, and only if, the following conditions are satisfied$\,:$

[TABLE]

Proof.

Suppose $X$ is a congruence class w.r.t. $\theta$. Then (a) and (b) are obviously true.

Conversely, suppose both (a) and (b) are fulfilled. Then, according to (a), all formulas in $X$ are $\theta$-congruent to one another. In addition, in virtue of (b), each formula in $X$ cannot be $\theta$-congruent to a formula beyond $X$. ∎

The next two corollaries follow immediately from Proposition 5.2.3.

Corollary 5.2.3.1**.**

Let $\mathcal{S}$ be an abstract logic with $\bm{T}_{\mathcal{S}}\neq\emptyset$ and $D$ be an $\mathcal{S}$-theory. Then $D$ is a congruence class w.r.t. $\theta(D)$ if, and only if, $\theta(D)$ is compatible with $D$.

Corollary 5.2.3.2**.**

Let $\mathcal{S}$ be a structural abstract logic with $\bm{T}_{\mathcal{S}}\neq\emptyset$. Then the following conditions are equivalent$\,:$

[TABLE]

5.2.2 Some subclasses of unital logics

In this subsection, we introduce several classes of abstract logics, which were considered in the literature and which turned out to be included in the class of unital logics.

Definition 5.2.3** (implicative logic).**

A structural logic $\mathcal{S}$ in a language $\mathcal{L}$ is called implicative if $\mathcal{L}$ contains a binary connective $\rightarrow$ such that for any $\mathcal{S}$-theory $D$, the following conditions are satisfied$\,:$

[TABLE]

We note that if a logic $\mathcal{S}$ is implicative, then $\bm{T}_{\mathcal{S}}\neq\emptyset$.

Let $\mathcal{S}$ be (at least) an implicative logic and $D$ be an $\mathcal{S}$-theory. We define:

[TABLE]

Proposition 5.2.4**.**

Let $D$ be a theory of an implicative logic $\mathcal{S}$. Then $\theta_{D}$ is a congruence on $\mathfrak{F}_{\mathcal{L}}$ and $D$ is a congruence class w.r.t. $\theta_{D}$.

Proof.

That $\theta_{D}$ is a congruence follows straightforwardly from (a), (b) and (e) of Definition 5.2.3.

Next, we first note that, by premise, $D\neq\emptyset$. Secondly, if both $\alpha$ and $\beta$ belong to $D$, then, according to (d) of Definition 5.2.3, both $\alpha\rightarrow\beta$ and $\beta\rightarrow\alpha$ belong to $D$, that is $(\alpha,\beta)\in\theta_{D}$. And, thirdly, let $(\alpha,\beta)\in\theta_{D}$ and $\alpha\in D$. Then $\beta\in D$. In virtue of Proposition 5.2.3, this implies that $D$ is a congruence class w.r.t. $\theta_{D}$. ∎

Corollary 5.2.4.1**.**

If an abstract logic $\mathcal{S}$ is implicative, then $\mathcal{S}$ is unital.

The calculus in the language $\mathcal{L}_{A}$, which is defined by the inference rules ax1–ax10 and (b-$iii$) (modus ponens) of Section 3.3.3, is called the classical propositional logic and denoted by Cl. The calculus in $\mathcal{L}_{A}$, which is defined by the rules ax1–ax9, ax11 (Section 3.4.3) and modus ponens, is called the intuitionistic propositional logic and denoted by Int. Also, it will be convenient to consider another calculus in the language $\mathcal{L}_{A}$, P, which is defined by the inference rules ax1–ax8 and (b-$iii$) (modus ponens) of Section 3.3.3. We call P positive logic.

It must be clear that for any set $X\cup\{\alpha\}\subseteq\textit{{Fm}}_{\mathcal{L}_{A}}$

[TABLE]

Further, it can be easily shown that P, Cl and Int are implicative. (See Exercise 5.2.1.)

Another class of abstract logics, the class of Fregean logics, stems from Frege’s principle of compositionality (FPC).

An abstract logic $\mathcal{S}$ has the FPC if for for any set $X\cup\{\gamma(p,\ldots),\alpha,\beta\}\subseteq\textit{{Fm}}_{\mathcal{L}}$,

[TABLE]

This leads to the following (equivalent) definition.

Definition 5.2.4** (Fregean relation, Fregean logic).**

Given a structural logic $\mathcal{S}$ and an $\mathcal{S}$-theory $D$, the relation on $\mathfrak{F}_{\mathcal{L}}$ defined by the equivalence

[TABLE]

is called a Fregean relation relative to $D$. A structural logic is Fregean if for every $\mathcal{S}$-theory $D$, $\Lambda D$ is a congruence on $\mathfrak{F}_{\mathcal{L}}$.

We leave the reader to prove that for any structural logic $\mathcal{S}$, the properties of satisfying the FPC and being Fregean are equivalent. (See Exercise 5.3.3.)

Proposition 5.2.5**.**

If $\mathcal{S}$ is a Fregean logic with $\bm{T}_{\mathcal{S}}\neq\emptyset$, then $\mathcal{S}$ is unital.

Proof.

Let $D$ be an arbitrary $\mathcal{S}$-theory. We observe that $\theta(D)\subseteq\Lambda D$. Also, $\Lambda D$ is compatible with $D$. Applying Corollary 5.2.3.2, we obtain that $\mathcal{S}$ is unital. ∎

Exercises 5.2

Prove that the abstract logics P, Cl and Int are implicative. 2. 2.

Prove that the abstract logics P, Cl and Int are Fregean. 3. 3.

Prove that a structural logic $\mathcal{S}$ is Fregean if, and only if, it satisfies the FPC.

5.3 Lindenbaum-Tarski algebra

5.3.1 Definition and properties

The concept of unital abstract logic in turn induces the following important notion.

Definition 5.3.1** (Lindenbaum-Tarski algebra).**

Let $\mathcal{S}$ be a unital logic and $D$ be an $\mathcal{S}$-theory. The algebra $\textbf{LT}_{\mathcal{S}}[D]:=\langle\mathfrak{F}_{\mathcal{L}}/\theta(D),\mathbf{1}_{D}\rangle$, where $\mathbf{1}_{D}$ is $D$ understood as a congruence class w.r.t. $\theta(D)$, $($or very often only the first component \mathfrak{F}_{\mathcal{L}}/\theta(D)$$) is called the Lindenbaum-Tarski algebra $($of \mathcal{S}$$) relative to $D$. The algebra $\textbf{LT}_{\mathcal{S}}:=\langle\mathfrak{F}_{\mathcal{L}}/\theta(\bm{T}_{\mathcal{S}}),\mathbf{1}_{\bm{T}_{\mathcal{S}}}\rangle$ $($or the first component \mathfrak{F}_{\mathcal{L}}/\theta(\bm{T}_{\mathcal{S}})$$) is called simply the Lindenbaum-Tarski algebra of $\mathcal{S}$.

We observe that, given a unital logic $\mathcal{S}$ and any $\mathcal{S}$-theories $D$ and $D^{\prime}$, if $D^{\prime}\subseteq D$, then $\theta(D)\subseteq\theta(D^{\prime})$ and hence the algebra $\textbf{LT}_{\mathcal{S}}[D]$ is a homomorphic image of $\textbf{LT}_{\mathcal{S}}[D^{\prime}]$. Thus, for any $\mathcal{S}$-theory $D$, the algebra $\textbf{LT}_{\mathcal{S}}[D]$ is a homomorphic image of $\textbf{LT}_{\mathcal{S}}$.

Lemma 5.3.1**.**

Let $\theta$ be a congruence on $\mathfrak{F}_{\mathcal{L}}$. Then for any valuation $v$ in $\mathfrak{F}_{\mathcal{L}}/\theta$, there is an $\mathcal{L}$-substitution $\sigma$ such that for any formula $\alpha$, $v[\alpha]=\sigma(\alpha)/\theta$.

Proof.

Let $v$ be any valuation in $\mathfrak{F}_{\mathcal{L}}/\theta$; that is, $v$ is a homomorphism of $\mathfrak{F}_{\mathcal{L}}$ to $\mathfrak{F}_{\mathcal{L}}/\theta$. Suppose $v[p]=\beta_{p}/\theta$, where $p\in\mathcal{V}_{\mathcal{L}}$. Then we define a substitution as follows:

[TABLE]

for all $p\in\mathcal{V}_{\mathcal{L}}$, with any selection of $\beta_{p}$ from the class $\beta_{p}/\theta$. Thus, we have: $v[p]=\sigma(p)/\theta$, for all $p\in\mathcal{V}_{\mathcal{L}}$.

Now let us take any formula $\alpha$ and assume that $p_{1},\ldots,p_{n}$ are all variables that occur in $\alpha$. Then we have:

[TABLE]

∎

Proposition 5.3.1**.**

Let $\mathcal{S}$ be a unital logic. Each $\textbf{LT}_{\mathcal{S}}[D]$ is an $\mathcal{S}$-model.

Proof.

Suppose that $X\vdash_{\mathcal{S}}\alpha$. Let us take any $\textbf{LT}_{\mathcal{S}}[D]$ and consider a valuation $v$ in it. In virtue of Lemma 5.3.1, there is a substitution $\sigma$ such that for any formula $\beta$, $v[\beta]=\sigma(\beta)/\theta(D)$. Further, we note that, since $\mathcal{S}$ is structural, $\sigma(X)\vdash_{\mathcal{S}}\sigma(\alpha)$.

Now, suppose that for any $\gamma\in X$, $v[\gamma]=\mathbf{1}_{D}$. Then, since $\mathcal{S}$ is unital, for any $\gamma\in X$, $\sigma(\gamma)\in D$. This implies that $\sigma(\alpha)\in D$, that is $v[\alpha]=\mathbf{1}_{D}$. ∎

Corollary 5.3.1.1**.**

Let $\mathcal{S}$ be a unital logic. Then for any set $X\cup\{\alpha\}\Subset\textit{{Fm}}_{\mathcal{L}}$, and for any $\mathcal{S}$-theory $D$,

[TABLE]

Proof.

We apply successively Proposition 5.3.1 and (5.2). ∎

Proposition 5.3.2**.**

Let $\mathcal{S}$ be a unital logic and let $D\!:=\textbf{Cn}_{\mathcal{S}}(X)$. Then for any formula $\alpha$,

[TABLE]

Hence, $\textbf{LT}_{\mathcal{S}}$ is weakly adequate for $\mathcal{S}$.

Proof.

First, assume that $\models_{\textsf{{Lin}}_{\mathcal{S}}[X]}\alpha$; that is for any substitution $\sigma$, $\sigma(\alpha)\in D$. Let $v$ be a valuation in $\textbf{LT}_{\mathcal{S}}[D]$. By Lemma 5.3.1, there is a substitution $\sigma_{v}$ such that $v[\alpha]=\sigma_{v}(\alpha)/\theta(D)$. By premise, this implies that $v[\alpha]=\mathbf{1}_{D}$.

Conversely, suppose for some substitution $\sigma$, $\sigma(\alpha)\notin D$. We define a valuation in $\textbf{LT}_{\mathcal{S}}[D]$ as follows: $v[p]:=\sigma(p)/\theta(D)$, for any $p\in\mathcal{V}_{\mathcal{L}}$. Then $v[\alpha]=\sigma(\alpha)/\theta(D)\neq\mathbf{1}_{D}$. ∎

Corollary 5.3.2.1**.**

Let $D$ be an $\mathcal{S}$-theory of a unital logic $\mathcal{S}$. Then for any $\mathcal{S}$-thesis $\alpha$, the algebras $\textbf{LT}_{\mathcal{S}}[D]$ validate $\alpha$.

Proof.

Having noticed that $\textbf{LT}_{\mathcal{S}}[D]$ is a homomorphic image of $\textbf{LT}_{\mathcal{S}}$, we apply the last part of Proposition 5.3.2. ∎

We recall that $\Sigma_{\mathcal{S}}$ denotes the set of all $\mathcal{S}$-theories.

Corollary 5.3.2.2**.**

Any unital logic $\mathcal{S}$ is determined by the class $\{\textbf{LT}_{\mathcal{S}}[D]\leavevmode\nobreak\ |\leavevmode\nobreak\ D\in\Sigma_{\mathcal{S}}\}$.

Proof.

Indeed, if $X\vdash_{\mathcal{S}}\alpha$, then, in virtue of Proposition 5.3.1, $X\models_{\textbf{LT}_{\mathcal{S}}[D]}\alpha$, for each $D\in\Sigma_{\mathcal{S}}$.

On the other hand, if $X\not\vdash_{\mathcal{S}}\alpha$, then $\not\models_{\textsf{{Lin}}_{\mathcal{S}}[X]}\alpha$ and hence, according to Proposition 5.3.2, $\not\models_{\textbf{LT}_{\mathcal{S}}[D]}\alpha$, where $D=\textbf{Cn}_{\mathcal{S}}(X)$. ∎

Corollary 5.3.2.3**.**

Let $\mathcal{S}$ be a unital logic. If a set $X\subseteq\textit{{Fm}}_{\mathcal{L}}$ is closed under arbitrary substitutions, then for any formula $\alpha$,

[TABLE]

where $D=\textbf{Cn}_{\mathcal{S}}(X)$.

Proof.

We have:

[TABLE]

∎

Now we define a special valuation in $\textbf{LT}_{\mathcal{S}}[D]$:

[TABLE]

for any $p\in\mathcal{V}_{\mathcal{L}}$.

Proposition 5.3.3**.**

Let $\mathcal{S}$ be a unital logic and $D:=\textbf{Cn}_{\mathcal{S}}(X)$. Then for any formula $\alpha$, the following conditions are equivalent$\,:$

[TABLE]

In particular, the following conditions are equivalent$\,:$

[TABLE]

Proof.

The implication (a)$\Rightarrow$(b) follows from Corollary 5.3.1.1.

Assume (b). Let us take any $\beta\in X$. We have: $\bm{v}_{D}[\beta]=\beta/\theta(D)=\mathbf{1}_{D}$. Hence (c).

Now assume (c), that is $\bm{v}_{D}[\alpha]=\mathbf{1}_{D}$. This means that $\alpha/\theta(D)=\mathbf{1}_{D}$, that is $\alpha\in D$. Hence (a). ∎

We aim to show that the Lindenbaum-Tarski algebras are good as separating means (Section 4.3); or, better to say, they are useful for creating separating means. With this in mind, given a unital logic $\mathcal{S}$ in a language $\mathcal{L}$, we define the following classes of unital expansions.

• •

$\mathbb{P}_{\mathcal{S}}$ is the class of all algebraic $\mathcal{S}$-models; according to Proposition 5.1.1, $\mathbb{P}_{\mathcal{S}}$ is a quasivariety.

• •

$\mathbb{Q}_{\mathcal{S}}$ is the quasivariety generated by the set $\{\textbf{LT}_{\mathcal{S}}[D]\leavevmode\nobreak\ |\leavevmode\nobreak\ D\in\Sigma_{\mathcal{S}}\}$; according to Proposition 5.3.1, $\mathbb{Q}_{\mathcal{S}}\subseteq\mathbb{P}_{\mathcal{S}}$; also, if $\mathcal{S}$ is finitary, then, in virtue of Corollary 5.3.1.1, $\mathbb{Q}_{\mathcal{S}}$ is determined by the quasiidentities $X\approx\mathbf{1}\Rightarrow\alpha\approx\mathbf{1}$, for any $X\cup\{\alpha\}\Subset\mathfrak{F}_{\mathcal{L}}$ such that $X\vdash_{\mathcal{S}}\alpha$.

• •

$\mathbb{T}_{\mathcal{S}}$ is the class of all unital expansions $\langle\textsf{{A}},\mathbf{1}\rangle$ such that $\langle\textsf{{A}},\mathbf{1}\rangle\models\alpha\approx\mathbf{1}$, for any $\alpha\in\bm{T}_{\mathcal{S}}$; it is obvious that $\{\textbf{LT}_{\mathcal{S}}[D]\leavevmode\nobreak\ |\leavevmode\nobreak\ D\in\Sigma_{\mathcal{S}}\}\subseteq\mathbb{T}_{\mathcal{S}}$.

Summing up, we conclude this subsection as follows.

Theorem 5.3.1**.**

Let $\mathcal{S}$ be a unital logic. Then the following conditions are equivalent$\,:$

[TABLE]

Proof.

The implication (a)$\Rightarrow$(b) is due to definition of $\mathbb{P}_{\mathcal{S}}$; (b)$\Rightarrow$(c) is due to inclusion $\mathbb{Q}_{\mathcal{S}}\subseteq\mathbb{P}_{\mathcal{S}}$; (c)$\Rightarrow$(d) is due to definition of $\mathbb{Q}_{\mathcal{S}}$; and (d)$\Rightarrow$(a) is due to Corollary 5.3.2.2. ∎

Thus, we see that if $X\not\vdash_{\mathcal{S}}\alpha$, an algebra $\langle\textsf{{A}},\mathbf{1}\rangle$ separating $X$ from $\alpha$ can be found among the algebras of the class $\mathbb{Q}_{\mathcal{S}}=\mathbf{S}\mathbf{P_{r}}\{\textbf{LT}_{\mathcal{S}}[D]\}_{D\in\Sigma_{\mathcal{S}}}$; cf. [Mal73], § 11, theorem 4. As we will see in the next subsection, under a restriction on $\mathcal{S}$, separating algebras (in the above sense) can be reached as homomorphic images of $\textbf{LT}_{\mathcal{S}}$. In the proof of this below, the class $\mathbb{T}_{\mathcal{S}}$ plays a key role. The importance of the class $\mathbb{T}_{\mathcal{S}}$ also lies in the fact that if $X\not\vdash_{\mathcal{S}}\alpha$, a separating algebra $\langle\textsf{{A}},\mathbf{1}\rangle$ is likely to belong to $\mathbb{Q}_{\mathcal{S}}\cap\mathbb{T}_{\mathcal{S}}$.

5.3.2 Implicational unital logics

In view of (5.1), it is clear that the class $\mathbb{T}_{\mathcal{S}}$ is a variety. We aim to show that, under above restriction on $\mathcal{S}$, $\textbf{LT}_{\mathcal{S}}$ is a free algebra over $\mathbb{T}_{\mathcal{S}}$.

Definition 5.3.2** (implicational abstract logic).**

Let $\mathcal{S}$ be an abstract logic in a language $\mathcal{L}$. Assume that there is an $\mathcal{L}$-formula of two sentential variables, $\bm{\iota}(p,q)$, such that for any $\mathcal{L}$-formulas $\alpha$ and $\beta$, any algebra $\langle\textsf{{A}},\mathbf{1}\rangle\in\mathbb{T}_{\mathcal{S}}$ and any valuation $v$ in A,

[TABLE]

Then we call $\mathcal{S}$ implicational w.r.t. $\bm{\iota}(p,q)$.

The abstract logics P, Cl and Int are examples of implicational logics. (Exercise 5.3.1)

Below we will be considering implicational logics which are also unital. Since for such a logic $\mathcal{S}$, $\bm{T}_{\mathcal{S}}\neq\emptyset$ (Proposition 5.2.2), we select an arbitrary $\mathcal{L}$-formula $\bigstar\in\bm{T}_{\mathcal{S}}$.

In virtue of Proposition 5.3.3, for any valuation $v$ in $\textbf{LT}_{\mathcal{S}}$,

[TABLE]

(Exercise 5.3.2)

We recall the signature of any unital expansion $\langle\textsf{{A}},\mathbf{1}\rangle$ is of type $\mathcal{L}$ expanded by an additional constant symbol $\mathbf{1}$ which is interpreted by the 0-ary operation $\mathbf{1}$ in $\langle\textsf{{A}},\mathbf{1}\rangle$ (denoted is denoted by $\mathbf{1}_{\bm{T}_{\mathcal{S}}}$ in $\textbf{LT}_{\mathcal{S}}$). We denote this extended type by $\mathcal{L}^{\star}$.

Let $\mathbf{t}$ be a term of type $\mathcal{L}^{\star}$. The conversion of $\mathbf{t}$ is the $\mathcal{L}$-formula (or term of type $\mathcal{L}$), denoted by $\mathbf{t}^{\star}$, which is obtained from $\mathbf{t}$ by simultaneous replacement of all occurrences of $\mathbf{1}$, if any, in $\mathbf{t}$ by $\bigstar$.

Consequently, any valuation $v$ in an algebra A of type $\mathcal{L}$ is extended to the valuation $v^{\star}$ in $\langle\textsf{{A}},\mathbf{1}\rangle$ such that $v^{\star}(p)=v(p)$, for any $p\in\mathcal{V}_{\mathcal{L}}$, and $v^{\star}(\mathbf{1})=\mathbf{1}$, where the first occurrence of ‘$\mathbf{1}$’ is a 0-ary constant of $\mathcal{L}^{\star}$, and the second is the 0-ary operation $\mathbf{1}$ of $\langle\textsf{{A}},\mathbf{1}\rangle$. We refer to $v^{\star}$ as a $\star$-extension of $v$. We note that the valuation $v$ can be restored from $v^{\star}$ in the sense that if $w$ is any valuation in $\langle\textsf{{A}},\mathbf{1}\rangle$, there is a unique valuation $v$ in A such that $v^{\star}=w$. (Exercise 5.3.3)

Using (5.4), we observe that for any $\mathcal{L}^{\star}$-terms $\mathbf{t}$ and $\mathbf{r}$ and any valuation $v^{\star}$ in $\textbf{LT}_{\mathcal{S}}$,

[TABLE]

(Exercise 5.3.4)

For any terms $\mathbf{t}$ and $\mathbf{r}$ of type $\mathcal{L}^{\star}$, we denote:

\mathbb{T}_{\mathcal{S}}\models\mathbf{t}\approx\mathbf{r}\leavevmode\nobreak\ \stackrel{{\scriptstyle\text{df}}}{{\Longleftrightarrow}}\leavevmode\nobreak\ for any $\left\langle\textsf{{A}},\mathbf{1}\right\rangle\in\mathbb{T}_{\mathcal{S}}$, $\models_{\langle\textbf{A},\mathbf{1}\rangle}\mathbf{t}\approx\mathbf{r}$.

The equivalence (5.5) can be generalized as follows.

Lemma 5.3.2**.**

Let $\langle\textsf{{A}},\mathbf{1}\rangle\in\mathbb{T}_{\mathcal{S}}$. Then for any term $\mathbf{t}$ of type $\mathcal{L}^{\star}$ and any valuation $v^{\star}$ in $\langle\textsf{{A}},\mathbf{1}\rangle$, $v^{\star}(\mathbf{t})=v(\mathbf{t}^{\star})$.

Proof can be carried out by induction on the number of functional symbols of the language $\mathcal{L}^{\star}$. We leave it to the reader. (Exercise 5.3.5)

Proposition 5.3.4**.**

Let $\mathcal{S}$ be nontrivial unital logic which is implicational w.r.t. $\bm{\iota}(p,q)$. Then for terms $\mathbf{t}$ and $\mathbf{r}$ of type $\mathcal{L}^{\star}$,

[TABLE]

where $\bm{v}_{0}^{\star}$ is the $\star$-extension of $\bm{v}_{0}$. Hence $\textbf{LT}_{\mathcal{S}}$ is a free algebra of rank $\textit{card}(\mathcal{L})$ over the variety $\mathbb{T}_{\mathcal{S}}$ and also over the quasivariety $\mathbb{Q}_{\mathcal{S}}\cap\mathbb{T}_{\mathcal{S}}$.

Proof.

We successively obtain:

[TABLE]

According to [Mal73], § 12.2, theorem 1, this implies that $\textbf{LT}_{\mathcal{S}}$ is a free algebra over the class $\mathbb{T}_{\mathcal{S}}$. In virtue of Proposition 5.2.1, the rank of $\textbf{LT}_{\mathcal{S}}$ equals $\textit{card}(\mathcal{L})$.

Since the quasivariety $\mathbb{Q}_{\mathcal{S}}\cap\mathbb{T}_{\mathcal{S}}$ contains all algebras $\textbf{LT}_{\mathcal{S}}[D]$ and because of Corollary 5.3.2.2, $\mathcal{S}$ is determined by $\mathbb{Q}_{\mathcal{S}}\cap\mathbb{T}_{\mathcal{S}}$. It is obvious that $\textbf{LT}_{\mathcal{S}}$ is a free algebra over $\mathbb{Q}_{\mathcal{S}}\cap\mathbb{T}_{\mathcal{S}}$. ∎

5.3.3 Examples of Lindenbaum-Tarski algebras

Let $\mathcal{S}$ be a nontrivial unital logic in a language $\mathcal{L}$ with $\textit{card}(\mathcal{V}_{\mathcal{L}})=\kappa$. Then, according to (5.3), $\textit{card}(|\textbf{LT}_{\mathcal{S}}|)\geq\kappa$. In particular, $\textit{card}(|\textbf{LT}_{\textsf{Cl}}|)=\textit{card}(|\textbf{LT}_{\textsf{Int}}|)=\textit{card}(\mathcal{V}_{\mathcal{L}_{A}})$. It must be clear that $\{p/\theta(\bm{T}_{\mathcal{S}})\leavevmode\nobreak\ |\leavevmode\nobreak\ p\in\mathcal{V}_{\mathcal{L}}\}$ is the set of free generators of $\textbf{LT}_{\mathcal{S}}$, if the latter can be considered as a free algebra of $\mathbb{T}_{\mathcal{S}}$. For some questions like decision problem for the consequence relation or theoremhood of $\mathcal{S}$, it suffices to consider the formulas built of a limited set of variables. Thus, if $\mathcal{V}\subseteq\mathcal{V}_{\mathcal{L}}$ with $\textit{card}(\mathcal{V})=\kappa$ and our consideration of $\mathcal{S}$ is limited to the formulas built from $\mathcal{V}$, we denote by $\textbf{LT}_{\mathcal{S}}(\kappa)$ a subalgebra of $\textbf{LT}_{\mathcal{S}}$, generated by the set $\{p/\theta(\bm{T}_{\mathcal{S}})\leavevmode\nobreak\ |\leavevmode\nobreak\ p\in\mathcal{V}\}$. The notation is justified by the fact if $\mathcal{V}^{\prime}\subseteq\mathcal{V}_{\mathcal{L}}$ and $\textit{card}(\mathcal{V}^{\prime})=\textit{card}(\mathcal{V})$, then the subalgebras of $\textbf{LT}_{\mathcal{S}}$, generated by $\{p/\theta(\bm{T}_{\mathcal{S}})\leavevmode\nobreak\ |\leavevmode\nobreak\ p\in\mathcal{V}\}$ and, respectively, by $\{p/\theta(\bm{T}_{\mathcal{S}})\leavevmode\nobreak\ |\leavevmode\nobreak\ p\in\mathcal{V}^{\prime}\}$ are isomorphic; cf. [Grä08], §24, corollary 2. Since each such $\textbf{LT}_{\mathcal{S}}(\kappa)$ is a free algebra in $\mathbb{Q}_{\mathcal{S}}$ (or even in $\mathbb{T}_{\mathcal{S}}$), it is called the free algebra of rank $\kappa$. We note that, since $\textbf{LT}_{\mathcal{S}}$ is always has at least one 0-ary operation, $\mathbf{1}$, even it makes sense to talk about a free algebra of rank 0.

We consider the free algebras $\textbf{LT}_{\textsf{Cl}}(0)$, $\textbf{LT}_{\textsf{Int}}(0)$, $\textbf{LT}_{\textsf{Cl}}(1)$ $\textbf{LT}_{\textsf{Cl}}(2)$ and $\textbf{LT}_{\textsf{Int}}(1)$, in order. The first two algebras should be understood as subalgebras of $\textbf{LT}_{\textsf{Cl}}$ and $\textbf{LT}_{\textsf{Int}}$, generated by their unit, $\mathbf{1}$. The resulting algebras are isomorphic (see Section 1.2.1 and Section 1.2.2) and can be depicted by the diagram:

Before discussing the structure of the other just mentioned Lindenbaum-Tarski algebras, we first consider the varieties $\mathbb{T}_{\textsf{Cl}}$ and $\mathbb{T}_{\textsf{Int}}$. Namely, we aim to show that these varieties coincide with the varieties of Boolean and Heyting algebras, respectively.

Since the classes $\mathbb{T}_{\textsf{Cl}}$ and $\mathbb{T}_{\textsf{Int}}$ consist of the algebras validating the theses of Cl and Int, respectively, (defined in Section 5.2.2) we take a look at these calculi more closely.

Lemma 5.3.3**.**

In addition to modus ponens, the inference rules (a–$i$)–(a–$iii$) and (b–$i$)–(b–$ii$) of Section 3.3.3 are sound w.r.t. P and hence w.r.t. Int and Cl.

Proof.

To prove the main assertion, we have to show that for any $\mathcal{L}_{A}$-formulas $\alpha$ and $\beta$, the following hold:

[TABLE]

When it’s done, we apply (5.4). We leave this task to the reader. (Exercise 5.3.6) ∎

The next lemma is known as the deduction theorem.

Lemma 5.3.4**.**

The hyperule (c–$i$) of Section 3.3.3 is sound w.r.t. P and hence w.r.t. Int and Cl.

Proof.

First of all, we notice that for any $\mathcal{L}_{A}$-formulas $\alpha$ and $\beta$,

[TABLE]

Thus for any formula $\alpha$,

[TABLE]

Now assume that $X,\alpha\vdash_{\textsf{P}}\beta$. That is, there is a P-derivation from $X,\alpha$:

[TABLE]

Let us form a finite sequence:

[TABLE]

and denote: $\gamma_{i}:=\alpha\rightarrow\alpha_{i}$, where $1\leq i\leq n$; so that $\gamma_{n}:=\alpha\rightarrow\beta$. By induction on the number $n$ of the formulas of $(\ast\ast)$, we prove that $\vdash_{\textsf{P}}\gamma_{n}$.

If $n=1$, then either $\beta=\alpha$ or $\beta\in X$. If the former is the case, then we apply ($\ast$). If $\beta\in X$, then we successively obtain: $\vdash_{\textsf{P}}\beta\rightarrow(\alpha\rightarrow\beta)$ and $X\vdash_{\textsf{P}}\alpha\rightarrow\beta$.

Next, assume that $\beta$ is obtained from $\alpha_{i}$ and $\alpha_{j}=\alpha_{i}\rightarrow\beta$. By induction hypothesis, $\vdash_{\textsf{P}}\alpha\rightarrow\alpha_{i}$ and $\vdash_{\textsf{P}}\alpha\rightarrow(\alpha_{i}\rightarrow\beta)$. Using ax2 and (b–$iii$) twice, we receive that $\vdash_{\textsf{P}}\alpha\rightarrow\beta$.

We obtain the last part of the statement with the help of (5.4). ∎

Lemma 5.3.5**.**

The hyperrules (c–$ii$) and (c–$iii$) of Section 3.3.3 are sound w.r.t. Int and Cl. Hence the rule (a–$iv$)is sound w.r.t. Int and Cl.

Proof.

The proof of the first part is straightforward and is left to the reader. (Exercise 5.3.7)

The proof of the second part is as follows. Let $\mathcal{S}$ be either Int or Cl. Since $\alpha,\neg\alpha\vdash_{\mathcal{S}}\alpha$ and $\alpha,\neg\alpha\vdash_{\mathcal{S}}\neg\alpha$, by (c-$ii$), we conclude that $\alpha\vdash_{\mathcal{S}}\neg\neg\alpha$. ∎

Corollary 5.3.4.1**.**

The logic Cl is an extension of Int.

Proof.

We show that $\vdash_{\textsf{Cl}}\text{ax11}$, that is, for any $\mathcal{L}_{A}$-formulas $\alpha$ and $\beta$,

[TABLE]

Indeed, since $\beta,\neg\beta,\neg\alpha\vdash_{\textsf{Cl}}\beta$ and $\beta,\neg\beta,\neg\alpha\vdash_{\textsf{Cl}}\neg\beta$, by the hyperrrule (c–$ii$), we derive that $\beta,\neg\beta\vdash_{\textsf{Cl}}\neg\neg\alpha$. Also, since, in virtue of Lemma 5.3.5, $\neg\neg\alpha\vdash_{\textsf{Cl}}\alpha$, by cut, we obtain that $\beta,\neg\vdash_{\textsf{Cl}}\alpha$. Then, we apply twice the hyperrule (c–$i$). ∎

Lemma 5.3.6**.**

For any $\mathcal{L}_{A}$-formulas $\alpha$, $\beta$ and $\gamma$, the following formulas and their converses are theses of P:

[TABLE]

Proof.

We show about one of these formulas, namely (j), that it and its converse are theses of P. First, we prove that

[TABLE]

We obtain:

[TABLE]

Further, we have:

[TABLE]

We leave for the reader to complete the proof of this lemma. (Exercise 5.3.8) ∎

Lemma 5.3.7**.**

For any $\mathcal{L}_{A}$-formulas $\alpha$ and $\beta$, the following formulas and their converses are theses of Cl:

[TABLE]

Proof.

We prove that (k) and its converse are theses of Cl and leave the rest to the reader. (Exercise 5.3.9)

First, we prove that

[TABLE]

Indeed, we have:

[TABLE]

For the converse, we have:

[TABLE]

∎

Proposition 5.3.5**.**

$\mathbb{T}_{\textsf{Cl}}$* coincides with the class of all Boolean algebras.*

Proof.

Let $\textsf{{B}}=\left\langle\textsf{B};\wedge,\vee,\neg,\mathbf{1}\right\rangle$ be a Boolean algebra. Expanding this algebra with an operation

[TABLE]

according to Proposition 1.2.2, we obtain a Heyting algebra $\textsf{{H}}=\left\langle\textsf{B};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\right\rangle$. In virtue of Proposition 1.2.3, the rules ax1–ax9 are valid in H and hence in B. In view of Corollary 1.2.2.1, the rule ax10 is also valid in B. And, because of the property $(\text{h}_{2})$ (Section 1.2.2), modus ponens preserves this validity over any Cl-derivation.

Now, assume that an algebra $\textsf{{A}}=\left\langle\textsf{A};\wedge,\vee,\neg,\mathbf{1}\right\rangle\in\mathbb{T}_{\textsf{Cl}}$. That is, for any $\mathcal{L}_{A}$-formula $\alpha\in\bm{T}_{\textsf{Cl}}$, $\textsf{{A}}\models\alpha\approx\mathbf{1}$. This means that for any $\alpha\in\bm{T}_{\textsf{Cl}}$ and any $\mathcal{L}_{A}$-valuation $v$ in A, $v(\alpha)=\mathbf{1}$. Therefore, in virtue of Lemma 5.3.6 and the fact that P is implicational w.r.t $\rightarrow$, the properties $(\text{l}_{1})$–$(\text{l}_{4})$ are valid in A. Namely, we have: (a) and its converse prove the validity of ($\text{l}_{1}$–$i$); (b) and its converse prove the validity of ($\text{l}_{1}$–$ii$); (c) and its converse prove the validity of ($\text{l}_{2}$–$i$); (f) and its converse prove the validity of ($\text{l}_{2}$–$ii$); (g) and its converse prove the validity of ($\text{l}_{3}$–$i$); (h) and its converse prove the validity of ($\text{l}_{3}$–$ii$); (j) and its converse prove the validity of ($\text{l}_{4}$–$i$); (i) and its converse prove the validity of ($\text{l}_{4}$–$ii$). Thus $\langle\textsf{A};\wedge,\vee\rangle$ is a distributive lattice.

Further, if $\bigstar$ is an arbitrary Cl-thesis and $p$ is an arbitrary variable, then

[TABLE]

This implies that for any element $x\in\textsf{A}$, $x\leq\mathbf{1}$, that is the equalities $(\text{b}_{1})$ hold in $\langle\textsf{A};\wedge,\vee,\mathbf{1}\rangle$, where $\mathbf{1}$ turns to be a greatest element in the sense of $\leq$ (Section 1.2.1).

Finally, we use Lemma 5.3.7 and the fact that Cl is and implicational abstract logic w.r.t. $\rightarrow$ to conclude that A is a Boolean algebra. ∎

Corollary 5.3.5.1**.**

$\textbf{LT}_{\textsf{Cl}}$* is a free Boolean algebra of rank $\textit{card}(\mathcal{V}_{\mathcal{L}_{A}})$. Hence, $\textbf{LT}_{\textsf{Cl}}(\kappa)$, where $\kappa\leq\textit{card}(\mathcal{V}_{\mathcal{L}_{A}})$, is a free Boolean algebras of rank $\kappa$.*

According to Corollary 5.3.5.1 and Proposition 1.2.1, any $\textbf{LT}_{\textsf{Cl}}(\kappa)$ of a finite rank $\kappa$ is finite. Let us take $\kappa=1$, assuming that $\mathcal{V}=\{p\}$. For simplicity, we denote

[TABLE]

It is not difficult to show that the subalgebra of $\textbf{LT}_{\textsf{Cl}}$ generated by $[p]$ consists of the four pairwise distinct elements: $[p]$, $[\neg p]$, $[p\vee\neg p]$ and $[p\wedge\neg p]$. (Exercise 5.3.3.10)This subalgebra is $\textbf{LT}_{\textsf{Cl}}(1)$. The relation $\leq$ between $[\alpha]$ and $[\beta]$ of this algebra is defined, according to (1.1), as follows:

[TABLE]

Thus, we arrive at the following diagram:

If $\mathcal{V}=\{p,q\}$, we obtain $\textbf{LT}_{\textsf{Cl}}(2)$ as a subalgebra of $\textbf{LT}_{\textsf{Cl}}$ generated by the classes $[p]$ and $[q]$. If we identify any congruence class of this subalgebra with its representative, we can depict $\textbf{LT}_{\textsf{Cl}}(2)$ by the following diagram:

Now we turn to Heyting algebras.

Lemma 5.3.8**.**

Let $\bigstar$ be an arbitrary Int-thesis. For any $\mathcal{L}_{A}$-formulas $\alpha$, $\beta$ and $\gamma$, the following implications and their converses are Int-theses:

[TABLE]

Proof.

We prove that $\vdash_{\textsf{Int}}(\neg\bigstar\vee\alpha)\rightarrow\alpha$ and $\vdash_{\textsf{Int}}\alpha\rightarrow(\neg\bigstar\vee\alpha)$ and leave for the reader to complete this proof. (Exercise 5.3.11)

Indeed, we obtain:

[TABLE]

Further, $\alpha\rightarrow(\neg\bigstar\vee\alpha)$ is an instantiation of ax7. ∎

Proposition 5.3.6**.**

$\mathbb{T}_{\textsf{Int}}$* coincides with the class of all Heyting algebras.*

Proof.

Let $\textsf{{H}}=\langle\textsf{H};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle$ be a Heyting algebra. In virtue of Proposition 1.2.3, the rules ax1–ax9 are valid in H. In virtue of the properties (1.5), (1.6) and (1.7), we receive that ax11 is also valid in H. Noticing, that modus ponens preserves validity in any Heyting algebra, we conclude that if $\alpha\in\bm{T}_{\textsf{Int}}$, then $\textsf{{H}}\models\alpha\approx\mathbf{1}$.

Next, assume that an algebra $\textsf{{H}}=\langle\textsf{H};\wedge,\vee,\rightarrow,\neg,\mathbf{1}\rangle\in\mathbb{T}_{\textsf{Int}}$. That is, for any $\alpha\in\bm{T}_{\textsf{Int}}$ and any valuation $v$ in H, $v(\alpha)=\mathbf{1}$. We show that the properties $(\text{l}_{1})$–$(\text{l}_{4})$, $(\text{b}_{1})$, and $(\text{h}_{1})$–$(\text{h}_{6})$ are valid in H.

In virtue of Lemma 5.3.6 and the fact that P is implicational w.r.t $\rightarrow$, the properties $(\text{l}_{1})$–$(\text{l}_{4})$ are valid in H. Thus $\langle\textsf{H};\wedge,\vee\rangle$ is a distributive lattice.

Further, similarly to (5.5), we derive that

[TABLE]

for any variable $p$ and Int-thesis $\bigstar$. This implies that the equalities $(\text{b}_{1})$ are true in H.

To prove the properties $(\text{h}_{1})$–$(\text{h}_{6})$, we apply Lemma 5.3.8. ∎

Corollary 5.3.6.1**.**

$\textbf{LT}_{\textsf{Int}}$* is a free Heyting algebra of rank $\textit{card}(\mathcal{V}_{\mathcal{L}_{A}})$. Hence, $\textbf{LT}_{\textsf{Int}}(\kappa)$, where $\kappa\leq\textit{card}(\mathcal{V}_{\mathcal{L}_{A}})$, is a free Heyting algebras of rank $\kappa$.*

Below we give a description of $\textbf{LT}_{\textsf{Int}}(1)$. For this, we consider the following formulas of an arbitrary variable $p$.

First, we define:

[TABLE]

Then for any $n\geq 0$, we define:

[TABLE]

The elements of $\textbf{LT}_{\textsf{Int}}(1)$ are the congruence classes w.r.t. $\theta(\bm{T}_{\textsf{Int}})$. It will be convenient, in writing, to depict each congruence class by its representative; in other words we will treat $P_{n}$, on the one hand, as an $\mathcal{L}_{A}$-formula and, on the other, as the congruence classes it generates. In accordance with this agreement, we have:

[TABLE]

Also, we will be writing $P_{i}\leq P_{j}$ in the sense that $P_{i}\to P_{j}=\mathbf{1}$, that is $\vdash_{\textsf{Int}}P_{i}\to P_{j}$; compare with (1.6).

We conclude with the following observation, due to Iwao Nishimura [Nis62]; see also L. Rieger [Rie57].

Proposition 5.3.7**.**

Every $\mathcal{L}_{A}$-formula of one variable $p$ is equivalent in Int to one and only one formula $P_{i}$, which by themselves are not equivalent to each other and related to each other as shown in the following diagram.

Exercises 5.3

Show that the abstract logics P, Cl and Int are implicational. 2. 2.

Prove (5.4). 3. 3.

Prove that for any valuation $w$ in $\langle\textsf{{A}},\mathbf{1}\rangle$, there is a unique valuation $v$ in A such that $v^{\star}=w$. 4. 4.

Prove (5.5). 5. 5.

Prove Lemma 5.3.2. 6. 6.

Complete the proof of Lemma 5.3.3. 7. 7.

Show that the hyperrules (c–$ii$) and (c–$iii$) are sound w.r.t. Cl and Int. 8. 8.

Complete the proof of Lemma 5.3.6. 9. 9.

Complete the proof of Lemma 5.3.7. 10. 10.

Show that the elements $[p]$, $[\neg p]$, $[p\vee\neg p]$ and $[p\wedge\neg p]$ are pairwise distinct in $\textbf{LT}_{\textsf{Cl}}$. (Hint: prove that the matrix $\textsf{{B}}_{2}$ is a Cl-model.) 11. 11.

Complete the proof of Lemma 5.3.8.