Effective Finite-Valued Approximations of General Propositional Logics

TL;DR

This paper explores how complex propositional logics can be approximated by simpler finite-valued logics, providing methods to compute minimal such logics and conditions for their effective characterization.

Contribution

It introduces a way to compute the minimal finite-valued logic for which a calculus is strongly sound and investigates conditions for representing propositional logics as intersections of finite-valued logics.

Findings

Minimal m-valued logic for strong soundness can be calculated.

Propositional logics can be characterized as intersections of finite-valued logics under certain conditions.

Finite-valued semantics offer computationally simpler alternatives for propositional logic reasoning.

Abstract

Propositional logics in general, considered as a set of sentences, can be undecidable even if they have "nice" representations, e.g., are given by a calculus. Even decidable propositional logics can be computationally complex (e.g., already intuitionistic logic is PSPACE-complete). On the other hand, finite-valued logics are computationally relatively simple - at worst NP. Moreover, finite-valued semantics are simple, and general methods for theorem proving exist. This raises the question to what extent and under what circumstances propositional logics represented in various ways can be approximated by finite-valued logics. It is shown that the minimal $m$-valued logic for which a given calculus is strongly sound can be calculated. It is also investigated under which conditions propositional logics can be characterized as the intersection of (effectively given) sequences of finite-valued logics.

Equations

$$\begin{array}[]{ll}a_{1}&A\supset A\land A\\ a_{2}&A\land B\supset B\land A\\ a_{3}&(A\supset B)\supset(A\land C\supset B\land C)\\ a_{4}&(A\supset B)\land(B\supset C)\supset(A\supset C)\\ a_{5}&B\supset(A\supset B)\\ a_{6}&A\land(A\supset B)\supset B\\ a_{7}&A\supset A\lor B\\ a_{8}&A\lor B\supset B\lor A\\ a_{9}&(A\supset C)\land(B\supset C)\supset(A\lor B\supset C)\\ a_{10}&\neg A\supset(A\supset B)\\ a_{11}&(A\supset B)\land(A\supset\neg B)\supset\neg A\\ a_{12}&A\supset(B\supset A\land B)\end{array}$$

$$B\text{lx@proof@logical@and}AA\supset B$$

$$C\text{lx@proof@logical@and}{A}_1\dots A_n$$

$$F_1,F_2,\dots ,F_s=F$$

$$A(X)\text{lx@proof@logical@and}A(\top )A(\perp )A(C)\leftrightarrow A(D)C\leftrightarrow D$$

$$X\cdot\Bigl{(}\bigl{(}(U\cdot V)\cdot W\bigr{)}\cdot Y\Bigr{)}\to ZX\cdot\Bigl{(}\bigl{(}U\cdot(V\cdot W)\bigr{)}\cdot Y\Bigr{)}\to Z\qquad\Bigl{(}X\cdot\bigl{(}(U\cdot V)\cdot W\bigr{)}\Bigr{)}\cdot Y\to Z\Bigl{(}X\cdot\bigl{(}U\cdot(V\cdot W)\bigr{)}\Bigr{)}\cdot Y\to Z$$

$$U\to V\cdot (X\wedge Y)\text{lx@proof@logical@and}U\to V\cdot XU\to V\cdot Y$$

$$X\top \supset X$$

$$\square \Pi \to \square A\square \Pi \to A$$

$$\square \Pi \to \square A\Pi \to A$$

$$\square X\supset \square YX\supset YU\wedge (\square X\wedge \square Y)\supset VU\wedge \square (X\wedge Y)\supset VU\wedge \square Y\supset VU\wedge \square \square Y\supset V$$

$$C{A}_1\dots A_n$$

$$\{{\square }^k(\top )$$

$$\{{\square }^k(\top )\mid kis\; prime\}$$

$${\tilde{\neg }}_{{\mathbf{G}}_m}(v)$$

$${\tilde{\vee }}_{{\mathbf{G}}_m}(v,w)$$

$${\tilde{\wedge }}_{{\mathbf{G}}_m}(v,w)$$

$${\tilde{\supset }}_{{\mathbf{G}}_m}(v,w)$$

$${\tilde{\square }}_{\mathbf{M}\times {\mathbf{M}}^{\prime }}(w_1,\dots ,w_n)=⟨{\tilde{\square }}_{\mathbf{M}}(w_1,\dots ,w_n),{\tilde{\square }}_{{\mathbf{M}}^{\prime }}(w_1,\dots ,w_n)⟩.$$

$$\tilde{\square }(F_1,\dots ,F_n)=\square (F_1,\dots ,F_n)$$

$$\begin{array}[]{@{}l@{}}\widetilde{\vphantom{l}\square}(v_{1},\ldots,v_{n})=\\ \quad=\begin{cases}\square(F_{1},\ldots,F_{n})&\text{if $v_{j}=F_{j}$ for $1\leq j\leq n$}\\ &\text{and $\square(F_{1},\ldots,F_{n})\in{\rm Frm}_{i,j}({\cal L})$}\\ \top&\text{otherwise}\end{cases}\end{array}$$

$$\tilde{\square }(v_1,\dots ,v_n)=\{\begin{array}{ll}{t}_i& \text{if Bi≡□(Bj1,…,Bjn)}\\ & \text{and v1=tj1, …, vn=tjn}\\ \top & \text{otherwise}\end{array}$$

$$CF\sigma$$

$$X⊲Z\text{lx@proof@logical@and}X⊲YY⊲ZYX⊲X$$

$$X\ne YY\ne XY\text{lx@proof@logical@and}X\ne TX\ne F$$

$${\tilde{\square }}_{{\mathbf{G}}_m^{\top }}(\bar{v})=\{\begin{array}{ll}\top & \text{if ⊤∈vˉ}\\ {\tilde{\square }}_{{\mathbf{G}}_m}(\bar{v})& \text{otherwise}\end{array}$$

$$X\tilde{\leftrightarrow }◯XX\tilde{\leftrightarrow }◯YX\tilde{\leftrightarrow }YYX\tilde{\leftrightarrow }X$$

$$\widetilde{◯}v$$

$$v\tilde{\tilde{\leftrightarrow }}w$$

$$\begin{array}[]{c|ccc}\supset&0&u&1\\ \hline\cr 0&1&1&1\\ u&v_{1}&1&1\\ 1&v_{0}&v_{2}&1\end{array}$$

$$\mathbf{L}=\{\begin{array}{ll}\{{\square }^k(\top )\}& \text{if k is the least solution of D(x)=0}\\ \varnothing & \text{otherwise}\end{array}$$

$${\mathbf{M}}_1$$

Full text

• Dedicated to Professor Trakhtenbrot on the occasion of his 85th birthday.

1 Introduction

The question of what to do when faced with a new logical calculus is an old problem of mathematical logic. Often, at least at first, no semantics are available. For example, intuitionistic propositional logic was constructed by Heyting only as a calculus; semantics for it were proposed much later. Linear logic was in a similar situation in the early 1990s. The lack of semantical methods makes it difficult to answer questions such as: Are statements of a certain form (un)derivable? Are the axioms independent? Is the calculus consistent? For logics closed under substitution, many-valued methods have often proved valuable since they were first used for proving underivabilities by Bernays [5] in 1926 (and later by others, e.g., McKinsey and Wajsberg; see also [17, § 25]). The method is very simple. Suppose you find a many-valued logic in which the axioms of a given calculus are tautologies, the rules are sound, but the formula in question is not a tautology: then the formula cannot be derivable.

Example 1

Intuitionistic propositional logic is axiomatized by the following calculus IPC:

Axioms:

[TABLE] 2. 2.

Rules (in usual notation):

[TABLE]

Now consider the two-valued logic with classical truth tables, except that $\lnot$ maps both truth values to “true”. Then every axiom except $a_{10}$ is a tautology and modus ponens preserves truth. Hence $a_{10}$ is independent of the other axioms.

To use this method to answer underivability question in general it is necessary to find many-valued matrices for which the given calculus is sound. It is also necessary, of course, that the matrix has as few tautologies as possible in order to be useful. We are interested in how far this method can be automatized.

Such “optimal” approximations of a given calculus may also have applications in computer science. In the field of artificial intelligence many new (propositional) logics have been introduced. They are usually better suited to model the problems dealt with in AI than traditional (classical, intuitionistic, or modal) logics, but many have two significant drawbacks: First, they are either given solely semantically or solely by a calculus. For practical purposes, a proof theory is necessary; otherwise computer representation of and automated search for proofs/truths in these logics is not feasible. Although satisfiability in many-valued propositional logics is (as in classical logic) NP-complete [16], this is still (probably) much better than many other important logics.

On the other hand, it is evident from the work of Carnielli [6] and Hähnle [12] on tableaux, and Rousseau, Takahashi, and Baaz et al. [2] on sequents, that finite-valued logics are, from the perspective of proof and model theory, very close to classical logic. Therefore, many-valued logic is a very suitable candidate if one looks for approximations, in some sense, of given complex logics.

What is needed are methods for obtaining finite-valued approximations of the propositional logics at hand. It turns out, however, that a shift of emphasis is in order here. While it is the logic we are actually interested in, we always are given only a representation of the logic. Hence, we have to concentrate on approximations of the representation, and not of the logic per se.

What is a representation of a logic? The first type of representation that comes to mind is a calculus. Hilbert-type calculi are the simplest conceptually and the oldest historically. We will investigate the relationship between such calculi on the one hand and many-valued logics or effectively enumerated sequences of many-valued logics on the other hand. The latter notion has received considerable attention in the literature in the form of the following two problems: Given a calculus C,

find a minimal (finite) matrix for which C is sound (relevant for non-derivability and independence proofs), and 2. 2.

find a sequence of finite-valued logics, preferably effectively enumerable, whose intersection equals the theorems of C, and its converse, given a sequence of finite-valued logics, find a calculus for its intersection (exemplified by Jaśkowski’s sequence for intuitionistic propositional calculus, and by Dummett’s extension axiomatizing the intersection of the sequence of Gödel logics, respectively).

For (1), of course, the best case would be a finite-valued logic M whose tautologies coincide with the theorems of C. C then provides an axiomatization of M. This of course is not always possible, at least for finite-valued logics. Lindenbaum [15, Satz 3] has shown that any logic (in our sense, a set of formulas closed under substitution) can be characterized by an infinite-valued logic. For a discussion of related questions see also Rescher [17, § 24].

In the following we study these questions in a general setting. Consider a propositional Hilbert-type calculus C. It is (weakly) sound for a given $m$-valued logic if all its theorems are tautologies. Unfortunately, it turns out that it is undecidable if a calculus is sound for a given $m$-valued logic. However, for natural stronger soundness conditions this question is decidable; a finite-valued logic for which C satisfies such soundness conditions is called a cover for C. The optimal (i.e., minimal under set inclusion of the tautologies) $m$-valued cover for C can be computed. The next question is, can we find an approximating sequence of $m$-valued logics in the sense of (2)? It is shown that this is impossible for undecidable calculi C, and possible for all decidable logics closed under substitution. This leads us to the investigation of the many-valued closure ${\rm MC}({\bf C})$ of C, i.e., the set of formulas which are true in all covers of C. In other words, if some formula can be shown to be underivable in C by a Bernays-style many-valued argument, it is not in the many-valued closure. Using this concept we can classify calculi according to their many-valued behaviour, or according to how good they can be dealt with by many-valued methods. In the best case ${\rm MC}({\bf C})$ equals the theorems of C (This can be the case only if C is decidable). We give a sufficient condition for this being the case. Otherwise ${\rm MC}({\bf C})$ is a proper superset of the theorems of C.

Axiomatizations C and ${\bf C}^{\prime}$ of the same logic may have different many-valued closures ${\rm MC}({\bf C})$ and ${\rm MC}({\bf C}^{\prime})$ while being model-theoretically indistinguishable. Hence, the many-valued closure can be used to distinguish between C and ${\bf C}^{\prime}$ with regard to their proof-theoretic properties.

Finally, we investigate some of these questions for other representations of logics, namely for decision procedures and (effectively enumerated) finite Kripke models. In these cases approximating sequences of many-valued logics whose intersection equals the given logics can always be given.

Some of our results were previously reported in [4], of which this paper is a substantially revised and expanded version.

2 Propositional Logics

Definition 2.1

A propositional language $\cal L$ consists of the following:

propositional variables: $X_{1}$, $X_{2}$, $X_{3}$, … 2. 2.

propositional connectives of arity $n_{j}$: $\square_{1}^{n_{1}}$, $\square_{2}^{n_{2}}$, …, $\square_{r}^{n_{r}}$. If $n_{j}=0$, then $\square_{j}$ is called a propositional constant. 3. 3.

Auxiliary symbols: $($, $)$, and , (comma).

Formulas and subformulas are defined as usual. We denote the set of formulas over a language $\cal L$ by ${\rm Frm}({\cal L})$. By $\mathord{\rm Var}(A)$ we mean the set of propositional variables occurring in $A$. A substitution $\sigma$ is a mapping of variables to formulas, and if $F$ is a formula, $F\sigma$ is the result of simultaneously replacing each variable $X$ in $F$ by $\sigma(X)$.

Definition 2.2

The depth $\mathrm{dp}(A)$ of a formula $A$ is defined as follows: $\mathrm{dp}(A)=0$ if $A$ is a variable or a 0-place connective (constant). If $A=\square(A_{1},\ldots,A_{n})$, then let $\mathrm{dp}(A)=\max\{\mathrm{dp}(A_{1}),\ldots,\mathrm{dp}(A_{n})\}+1$.

Definition 2.3

A propositional Hilbert-type calculus C in the language ${\cal L}$ is given by

a finite set $A({\bf C})\subseteq{\rm Frm}({\cal L})$ of axioms. 2. 2.

a finite set $R({\bf C})$ of rules of the form

[TABLE]

where $C$, $A_{1}$, …, $A_{n}\in{\rm Frm}({\cal L})$

A formula $F$ is a theorem of L if there is a derivation of $F$ in C, i.e., a finite sequence

[TABLE]

of formulas s.t. for each $F_{i}$ there is a substitution $\sigma$ so that either

$F_{i}=A\sigma$ where $A$ is an axiom in $A({\bf C})$, or 2. 2.

there are $F_{k_{1}}$, …, $F_{k_{n}}$ with $k_{j}<i$ and a rule $r\in R({\bf C})$ with premises $A_{1}$, …, $A_{n}$ and conclusion $C$, s.t. $F_{k_{j}}=A_{j}\sigma$ and $F_{i}=C\sigma$

If $F$ is a theorem of C we write ${\bf C}\vdash F$. The set of theorems of C is denoted by ${\rm Thm}({\bf C})$.

Remark 1

The above notion of a propositional rule is the one usually used in axiomatizations of propositional logic. It is, however, by no means the only possible notion. For instance, Schütte’s rules

[TABLE]

where $X$ is a propositional variable, and $A$, $C$, and $D$ are formulas, does not fit under the above definition. And not only do they not fit this definition, the proof-theoretic behaviour of such rules is indeed significantly different from other “ordinary” rules. For instance, the rule on the left allows the derivation of all tautologies with $n$ variables in number of steps linear in $n$; with a Hilbert-type calculus falling under the definition, this is not possible [3].

Remark 2

Many logics are more naturally axiomatized using sequent calculi, in which structure (sequences of formulas, sequent arrows) are used in addition to formulas. Many sequent calculi can easily be encoded in Hilbert-type calculi in an extended language, or even straightforwardly translated into Hilbert calculi in the same language, using constructions sketched below:

Sequences of formulas can be coded using a binary operator $\cdot$. The sequent arrow can simply be coded as a binary operator $\to$. For empty sequences, a constant $\Lambda$ is used. We have the following rules, to assure associativity of $\cdot$:

[TABLE]

as well as the respective rules without $X$, without $Y$, without both $X$ and $Y$, with the rules upside-down, and also for the right side of the sequent (20 rules total). 2. 2.

The usual sequent rules can be coded using the above constructions, e.g., the $\land$-Right rule of LJ would become:

[TABLE] 3. 3.

If the language of the logic in question contains constants and connectives which “behave like” the $\Lambda$ and $\cdot$ on the left or right of a sequent, and a conditional which behaves like the sequent arrow, then no additional connectives are necessary. For instance, instead of $\cdot$, $\Lambda$ on the left, use $\land$, $\top$; on the right, use $\lor$, $\bot$, and use $\supset$ instead of $\to$. Addition of the rule

[TABLE]

would then result in a calculus which proves exactly the formulas $F$ for which the sequent ${}\to F$ is provable in the original sequent calculus. 4. 4.

Some sequent rules require restrictions on the form of the side formulas in a rule, e.g., the $\square$-right rule in modal logics:

[TABLE]

It is not immediately possible to accommodate such a rule in the translation. However, in some cases it can be replaced with another rule which can. E.g., in S4, it can be replaced by

[TABLE]

which can in turn be accommodated using rules such as

[TABLE]

(in the version with standard connectives serving as $\cdot$ and sequent arrow).

Definition 2.4

A propositional Hilbert-type calculus is called strictly analytic iff for every rule

[TABLE]

it holds that $\mathord{\rm Var}(A_{i})\subseteq\mathord{\rm Var}(C)$ and $\mathrm{dp}(A_{i}\sigma)\leq\mathrm{dp}(C\sigma)$ for every substitution $\sigma$.

This notion of strict analyticity is orthogonal to the one employed in the context of sequent calculi, where “analytic” is usually taken to mean that the rules have the subformula property (the formulas in the premises are subformulas of those in the conclusion). A strictly analytic calculus in our sense need not satisfy this. On the other hand, Hilbert calculi resulting from sequent calculi using the coding above need not be strictly analytic in our sense, even if the sequent calculus has the subformula property. For instance, the contraction rule does not satisfy the condition on the depth of substitution instances of the premises and conclusion. The standard notion of analyticity does not entail decidability, since for instance cut-free propositional linear logic LL is analytic but LL is undecidable [14]. Our notion of strict analyticity does entail decidability, since the depth of the conclusion of a rule in a proof is always greater or equal to the depth of the premises, and so the number of formulas that can appear in a proof of a given formula is finite.

Definition 2.5

A propositional logic L in the language $\cal L$ is a subset of ${\rm Frm}({\cal L})$ closed under substitution.

Every propositional calculus C defines a propositional logic, namely ${\rm Thm}({\bf C})$, since ${\rm Thm}({\bf C})$ is closed under substitution. Not every propositional logic, however, is axiomatizable, let alone finitely axiomatizable by a Hilbert calculus. For instance, the logic

[TABLE]

is not axiomatizable, whereas the logic

[TABLE]

is certainly axiomatizable (it is even decidable), but not by a Hilbert calculus using only $\square$ and $\top$. (It is easily seen that any Hilbert calculus for $\square$ and $\top$ has either only a finite number of theorems or yields arithmetic progressions of $\square$’s.)

Definition 2.6

A *propositional finite-valued logic *M is given by a finite set of truth values $V({\bf M})$, the set of designated truth values $V^{+}({\bf M})\subseteq V({\bf M})$, and a set of truth functions $\widetilde{\vphantom{l}\square}_{j}\colon V({\bf M})^{n_{j}}\to V({\bf M})$ for all connectives $\square_{j}\in{\cal L}$ with arity $n_{j}$.

Definition 2.7

A valuation $v$ is a mapping from the set of propositional variables into $V({\bf M})$. A valuation $v$ can be extended in the standard way to a function from formulas to truth values. $v$ satisfies a formula $F$, in symbols: $v\models_{\bf M}F$, if $v(F)\in V^{+}({\bf M})$. In that case, $v$ is called a model of $F$, otherwise a countermodel. A formula $F$ is a tautology of M iff it is satisfied by every valuation. Then we write ${\bf M}\models F$. We denote the set of tautologies of M by ${\rm Taut}({\bf M})$.

Example 2

The sequence of $m$-valued Gödel logics ${\bf G}_{m}$ is given by $V({{\bf G}_{m}})=\{0,1,\ldots,m-1\}$, the designated values $V^{+}({{\bf G}_{m}})=\{0\}$, and the following truth functions:

[TABLE]

In the remaining sections, we will concentrate on the relations between propositional logics L represented in some way (e.g., by a calculus), and finite-valued logics M. The objective is to find many-valued logics M, or effectively enumerated sequences thereof, which, in a sense, approximate the the logic L.

The following well-known product construction is useful for characterizing the “intersection” of many-valued logics.

Definition 2.8

Let ${\bf M}$ and ${\bf M}^{\prime}$ be $m$ and $m^{\prime}$-valued logics, respectively. Then ${\bf M}\times{\bf M}^{\prime}$ is the $mm^{\prime}$-valued logic where $V({\bf M}\times{\bf M}^{\prime})=V({\bf M})\times V({\bf M}^{\prime})$, $V^{+}({\bf M}\times{\bf M}^{\prime})=V^{+}({\bf M})\times V^{+}({\bf M}^{\prime})$, and truth functions are defined component-wise. I.e., if $\square$ is an $n$-ary connective, then

[TABLE]

For convenience, we define the following: Let $v$ and $v^{\prime}$ be valuations of M and ${\bf M}^{\prime}$, respectively. $v\times v^{\prime}$ is the valuation of ${\bf M}\times{\bf M}^{\prime}$ defined by: $(v\times v^{\prime})(X)=\langle v(X),v^{\prime}(X)\rangle$. If $v^{\times}$ is a valuation of ${\bf M}\times{\bf M}^{\prime}$, then the valuations $\pi_{1}v^{\times}$ and $\pi_{2}v^{\times}$ of ${\bf M}$ and ${\bf M}^{\prime}$, respectively, are defined by $\pi_{1}v^{\times}(X)=v$ and $\pi_{2}v^{\times}(X)=v^{\prime}$ iff $v^{\times}(X)=\langle v,v^{\prime}\rangle$.

Lemma 1

${\rm Taut}({\bf M}\times{\bf M}^{\prime})={\rm Taut}({\bf M})\cap{\rm Taut}({\bf M}^{\prime})$**

Proof

Let $A$ be a tautology of ${\bf M}\times{\bf M}^{\prime}$ and $v$ and $v^{\prime}$ be valuations of ${\bf M}$ and ${\bf M}^{\prime}$, respectively. Since $v\times v^{\prime}\models_{{\bf M}\times{\bf M}^{\prime}}A$, we have $v\models_{\bf M}A$ and $v^{\prime}\models_{{\bf M}^{\prime}}A$ by the definition of $\times$. Conversely, let $A$ be a tautology of both M and ${\bf M}^{\prime}$, and let $v^{\times}$ be a valuation of ${\bf M}\times{\bf M}^{\prime}$. Since $\pi_{1}v^{\times}\models_{\bf M}A$ and $\pi_{2}v^{\times}\models_{{\bf M}^{\prime}}A$, it follows that $v^{\times}\models_{{\bf M}\times{\bf M}^{\prime}}A$. ∎

The definition and lemma are easily generalized to the case of finite products $\prod_{i}{\bf M}_{i}$ by induction.

The construction of Lindenbaum [15, Satz 3] shows that every propositional logic can be characterized as the set of tautologies of an infinite-valued logic. ${\bf M}({\bf L})$ is defined as follows: the set of truth values $V({\bf M}({\bf L}))={\rm Frm}({\cal L})$, and the set of designated values $V^{+}({\bf M}({\bf L}))={\bf L}$. The truth functions are given by

[TABLE]

Since we are interested in finite-valued logics, the following constructions will be useful.

Definition 2.9

Let ${\rm Frm}_{i,j}({\cal L})$ be the set of formulas of depth $\leq i$ containing only the variables $X_{1}$, …, $X_{j}$. The finite-valued logic ${\bf M}_{i,j}({\bf L})$ is defined as follows: The set of truth values of ${\bf M}_{i,j}({\bf L})$ is $V={\rm Frm}_{i,j}({\cal L})\cup\{\top\}$; the designated values $V^{+}=({\rm Frm}_{i,j}({\cal L})\cap{\bf L})\cup\{\top\}$. The truth tables for ${\bf M}_{i,j}({\bf L})$ are given by:

[TABLE]

Proposition 1

Let $v$ be a valuation in ${\bf M}_{i,j}({\bf L})$. If $v(X)\notin{\rm Frm}_{i,j}({\cal L})$ for some $X\in\mathord{\rm Var}(A)$, then $v(A)=\top$. Otherwise, $v$ can also be seen as a substitution $\sigma_{v}$ assigning the formula $v(X)\in{\rm Frm}_{i,j}({\cal L})$ to the variable $X$. Then $v(A)=A$ if $\mathrm{dp}(A\sigma_{v})\leq i$ and $=\top$ otherwise.

If $A\in{\rm Frm}_{i,j}({\cal L})$, then $A\in{\rm Taut}({\bf M}_{i,j}({\bf L}))$ iff $A\in{\bf L}$; otherwise $A\in{\rm Taut}({\bf M}_{i,j}({\bf L}))$. In particular, ${\bf L}\subseteq{\rm Taut}({\bf M}_{i,j}({\bf L}))$.

Proof

By induction on the depth of $A$. ∎

When looking for a logic with as small a number of truth values as possible which falsifies a given formula we can use the following construction.

Proposition 2

Let M be any many-valued logic, and $A_{1}$, …, $A_{n}$ be formulas not valid in M. Then there is a finite-valued logic ${\bf M}^{\prime}=\Phi({\bf M},A_{1},\ldots,A_{n})$ s.t.

$A_{1}$, …, $A_{n}$ are not valid in ${\bf M}^{\prime}$, 2. 2.

${\rm Taut}({\bf M})\subseteq{\rm Taut}({\bf M}^{\prime})$, and 3. 3.

$\left|V({\bf M}^{\prime})\right|\leq\xi(A_{1},\ldots,A_{n})$, where $\xi(A_{1},\ldots,A_{n})=\prod_{i=1}^{n}\xi(A_{i})$ and $\xi(A_{i})$ is the number of subformulas of $A_{i}\ +1$.

Proof

We first prove the proposition for $n=1$. Let $v$ be the valuation in M making $A_{1}$ false, and let $B_{1}$, …, $B_{r}$ ($\xi(A_{1})=r+1$) be all subformulas of $A_{1}$. Every $B_{i}$ has a truth value $t_{i}$ in $v$. Let ${\bf M}^{\prime}$ be as follows: $V({\bf M}^{\prime})=\{t_{1},\ldots,t_{r},\top\}$, $V^{+}({\bf M}^{\prime})=V^{+}({\bf M})\cap V({\bf M}^{\prime})\cup\{\top\}$. If $\square\in{\cal L}$, define $\widetilde{\vphantom{l}\square}$ by

[TABLE]

(1) Since $t_{r}$ was undesignated in ${\bf M}$, it is also undesignated in ${\bf M}^{\prime}$. But $v$ is also a truth value assignment in ${\bf M}^{\prime}$, hence ${\bf M}^{\prime}\not\models A_{1}$.

(2) Let $C$ be a tautology of M, and let $w$ be a valuation in ${\bf M}^{\prime}$. If no subformula of $C$ evaluates to $\top$ under $w$, then $w$ is also a valuation in M, and $C$ takes the same truth value in ${\bf M}^{\prime}$ as in M w.r.t. $w$, which is designated also in ${\bf M}^{\prime}$. Otherwise, $C$ evaluates to $\top$, which is designated in ${\bf M}^{\prime}$. So $C$ is a tautology in ${\bf M}^{\prime}$.

(3) Obvious.

For $n>1$, the proposition follows by taking $\Phi({\bf M},A_{1},\ldots,A_{n})=\prod_{i=1}^{n}\Phi({\bf M},A_{i})$ ∎

3 Many-Valued Covers for Propositional Calculi

A very natural way of representing logics is via calculi. In the context of our study, one important question is under what conditions it is possible to find, given a calculus C, a finite-valued logic M which approximates as well as possible the set of theorems ${\rm Thm}({\bf C})$. In the optimal case, of course, we would like to have ${\rm Taut}({\bf M})={\rm Thm}({\bf C})$. This is, however,not always possible. In fact, it is in general not even possible to decide, given a calculus C and a finite-valued logic M, if M is sound for C. In some circumstances, however, general results can be obtained. We begin with some definitions.

Definition 3.1

A calculus C is weakly sound for an $m$-valued logic M provided ${\rm Thm}({\bf C})\subseteq{\rm Taut}({\bf M})$.

Definition 3.2

A calculus C is t-sound for an $m$-valued logic M if

1. ($*$)

All axioms $A\in A({\bf C})$ are tautologies of M, and for every rule $r\in R({\bf C})$ and substitution $\sigma$: if for every premise $A$ of $r$, $A\sigma$ is a tautology, then the corresponding instance $C\sigma$ of the conclusion of $r$ is a tautology as well.

Definition 3.3

A calculus C is strongly sound for an $m$-valued logic M if

1. (*$$*)

All axioms $A\in A({\bf C})$ are tautologies of M, and for every rule $r\in R({\bf C})$: if a valuation satisfies the premises of $r$, it also satisfies the conclusion.

M is then called a cover for C.

We would like to stress the distinction between these three notions of soundness. soundness. The notion of weak soundness is the familiar property of a calculus to produce only valid formulas (in this case: tautologies of M) as theorems. This “plain” soundness is what we actually would like to investigate in terms of approximations. More precisely, when looking for a finite-valued logic that approximates a given calculus, we are content if we find a logic for which C is weakly sound. This is unfortunately not possible in general.

Proposition 3

It is undecidable if a calculus C is weakly sound for a given $m$-valued logic M.

Proof

Let C be an undecidable propositional calculus, let $F$ be a formula, and let $C$ and, for each $X_{i}\in\mathord{\rm Var}(F)$, $C_{i}$ be new propositional constants ([math]-ary connective) not occurring in C. Let $\sigma\colon X_{i}\mapsto C_{i}$ be a substitution. Clearly, ${\bf C}\vdash F$ iff ${\bf C}\vdash F\sigma$. Now let ${\bf C}^{\prime}$ be C with the additional rule

[TABLE]

and let ${\bf M}$ be an $m$-valued logic which assigns a non-designated value to $C$ and otherwise interprets every connective as a constant function with a designated value. Then every formula except a variable of the original language is a tautology, and $C$ is not. M is then weakly sound for C over the original language, but weakly sound for ${\bf C}^{\prime}$ iff $C$ is not derivable. Moreover, ${\bf C}^{\prime}\vdash C$ iff ${\bf C}^{\prime}\vdash F\sigma$, i.e., iff ${\bf C}\vdash F$. If it were decidable whether M is weakly sound for ${\bf C}^{\prime}$ it would then also be decidable if ${\bf C}\vdash F$, contrary to the assumption that C is undecidable. ∎

On the other hand, it is obviously decidable if C is strongly sound for a given matrix M.

Proposition 4

It is decidable if a given propositional calculus is strongly sound for a given $m$-valued logic.

Proof

(*$$*) can be tested by the usual truth-table method. ∎

It is also decidable if C is t-sound for a matrix M, although this is less obvious:

Proposition 5

It is decidable if a given propositional calculus is t-sound for a given $m$-valued logic M.

Proof

Let $r$ be a rule with premises $A_{1}$, …, $A_{n}$ and conclusion $C$ containing the variables $X_{1}$, …, $X_{k}$, and $\sigma$ a substitution. If $A_{1}\sigma$, …, $A_{n}\sigma$ are tautologies, but $C$ is not, then ($*$) is violated and $r$ is not weakly sound. Given $\sigma$, this is clearly decidable. We have to show that there are only a finite number of substitutions $\sigma$ which we have to test.

Let $Y_{1}$, …, $Y_{l}$ be the variables occurring in $X_{1}\sigma$, …, $X_{k}\sigma$. We show first that it suffices to consider $\sigma$ with $l=m$. For if $v$ is a valuation in which $C\sigma$ is false, then at most $m$ of $Y_{1}$, …, $Y_{l}$ have different truth values. Let $\tau$ be a substitution so that $\tau(Y_{i})=Y_{j}$ where $j$ is the least index such that $v(Y_{j})=v(Y_{i})$. Then (1) $v(C\sigma\tau)=v(C\sigma)$ and hence $C\sigma\tau$ is not a tautology; (2) $A_{i}\sigma\tau$ is still a tautology; (3) there are at most $m$ distinct variables occurring in $A_{1}\sigma\tau$, …, $A_{n}\sigma\tau$, $C\sigma\tau$.

Now every $B_{i}=X_{i}\sigma$ defines an $m$-valued function of $m$ arguments. There are $m^{m^{m}}$ such functions. Whether $A_{i}\sigma$ is a tautology only depends on the function defined by $B_{i}$, but it is not prima facie clear which functions can be expressed in M. Nevertheless, we can give a bound on the depth of formulas $B_{i}$ that have to be considered. Suppose $\sigma$ is a substitution of the required form with $B_{i}=X_{i}\sigma$ of minimal depth and suppose that the depth of $B_{i}$ is greater than $m^{\prime}=m^{m^{m}}$. Now consider a sequence of formulas $C_{1}$, …, $C_{m^{\prime}+1}$ with $C_{1}=B_{i}$ and each $C_{j}$ a subformula of $C_{j-1}$. Each $C_{j}$ also expresses an $m$-valued function of $m$ arguments. Since there are only $m^{\prime}$ different such functions, there are $j<j^{\prime}$ so that $C_{j}$ and $C_{j^{\prime}}$ define the same function. The formula obtained from $B_{i}$ by replacing $C_{j}$ by $C_{j^{\prime}}$ expresses the same function. Since this can be done for every sequence of $C_{j}$’s of length $>m^{\prime}$ we eventually obtain a formula which expresses the same function as $B_{i}$ but of depth $\leq m^{\prime}$, contrary to the assumption that it was of minimal depth. ∎

Now, if C is strongly sound for M, it is also t-sound; and if it is t-sound, it is also weakly sound. The converses, however, are false:

Example 3

Let $\cal L$ be the language consisting of a unary connective $\square$ and a binary connective $\vartriangleleft$, and let C be the calculus consisting of the sole axiom $X\vartriangleleft\square X$ and the rules

[TABLE]

It is easy to see that the only derivable formulas in C using only rule $r_{1}$ are substitution instances of $\square^{\ell}X\vartriangleleft\square^{k}X$ with $\ell<k$. In particular, no substitution instance of the premise of $r_{2}$, $X\vartriangleleft X$, is derivable. It follows that rule $r_{2}$ can never be applied. We now show that if C is strongly sound for an $m$-valued matrix M, ${\rm Taut}({\bf M})={\rm Frm}({\cal L})$, i.e., M is trivial. Suppose M is given by the set of truth values $V=\{1,\ldots,m\}$. Since $X\vartriangleleft\square X$ must be a tautology, $\widetilde{\vartriangleleft}(i,\widetilde{\square}(i))\in V^{+}$ for $i=1$, …, $m$. Since C is strongly sound for rule $r_{1}$, and by induction, $\widetilde{\vartriangleleft}(i,\widetilde{\square}^{k}(i))\in V^{+}$ for all $k$. Since $V$ is finite, there are $i$ and $k$ such that $i=\widetilde{\square}^{k}(i)$. Then $\widetilde{\vartriangleleft}(i,i)\in V^{+}$. Since C is strongly sound for $r_{2}$, we have $V=V^{+}$. However, C is weakly sound for non-trivial matrices, e.g., ${\bf M}^{\prime}$ with $V^{\prime}=\{1,\ldots,k\}$, $V^{+}=\{k\}$, $\widetilde{\square}(i)=i+1$ for $i<k$ and $=k$ otherwise, and $\widetilde{\vartriangleleft}(i,j)=k$ if $i<j$ or $j=k$ and $=1$ otherwise. C is, however, also not t-sound for this matrix.

Example 4

Consider the calculus with propositional constants $T$, $F$, and binary connective $\neq$, the axiom $T\neq F$ and the rules

[TABLE]

and the matrix with $V=\{0,1,2\}$, $V^{+}=\{2\}$, $\widetilde{T}=2$, $\widetilde{F}=0$, and $\widetilde{\neq}(i,j)=2$ if $i\neq j$ and $=0$ otherwise. Clearly, the only derivable formulas are $T\neq F$ and $F\neq T$, which are also tautologies. The calculus is not strongly sound, since for $v(X)=1$, $v(Y)=0$ the premises of $r_{2}$ are designated, but the conclusion is not. It is, however, t-sound: only a substitution $\sigma$ with $v(X\sigma)=1$ for all valuations $v$ would turn both premises of $r_{2}$ into tautologies, and there can be no such formulas. Hence, we have an example of a calculus t-sound but not strongly sound for a matrix.

Example 5

The IPC is strongly sound for the $m$-valued Gödel logics ${\bf G}_{m}$. For instance, take axiom $a_{5}$: $B\supset(A\supset B)$. This is a tautology in ${\bf G}_{m}$, for assume we assign some truth values $a$ and $b$ to $A$ and $B$, respectively. We have two cases: If $a\leq b$, then $(A\supset B)$ takes the value $m-1$. Whatever $b$ is, it certainly is $\leq m-1$, hence $B\supset A\supset B$ takes the designated value $m-1$. Otherwise, $A\supset B$ takes the value $b$, and again (since $b\leq b$), $B\supset A\supset B$ takes the value $m-1$.

Modus ponens passes the test: Assume $A$ and $A\supset B$ both take the value $m-1$. This means that $a\leq b$. But $a=m-1$, hence $b=m-1$.

Now consider the following extension ${\bf G}_{m}^{\top}$ of ${\bf G}_{m}$: $V({\bf G}_{m}^{\top})=V({{\bf G}_{m}})\cup\{\top\}$, $V^{+}({\bf G}_{m}^{\top})=\{m-1,\top\}$, and the truth functions are given by:

[TABLE]

for $\square\in\{\neg,\supset,\land,\lor\}$. IPC is not strongly sound for ${\bf G}_{m}^{\top}$, since a valuation with $v(X)=\top$, $v(Y)=0$ would satisfy the premises of rule MP, $X$ and $X\supset Y$, but not the conclusion $Y$. However, a calculus in which the conclusion of each rule contains all variables occurring in the premises, is strongly sound (such as a calculus obtained from LJ using the construction outlined in Remark 2).

Example 6

Consider the following calculus K:

[TABLE]

It is easy to see that the corresponding logic consists of all instances of $X\mathop{\tilde{\leftrightarrow}}{\scriptstyle\bigcirc}^{k}X$ where $k\geq 1$. This calculus is only strongly sound for the $m$-valued logic having all formulas as its tautologies. But if we leave out $r_{2}$, we can give a sequence of many-valued logics ${\bf M}_{i}$, for each of which K is strongly sound: Take for $V({\bf M}_{n})=\{0,\ldots,n-1\}$, $V^{+}({\bf M}_{n})=\{0\}$, with the following truth functions:

[TABLE]

Obviously, ${\bf M}_{n}$ is a cover for K. On the other hand, ${\rm Taut}({\bf M}_{n})\neq{\rm Frm}({\cal L})$, e.g., any formula of the form ${\scriptstyle\bigcirc}(A)$ takes a (non-designated) value $>0$ (for $n>1$). In fact, every formula of the form ${\scriptstyle\bigcirc}^{k}X\mathop{\tilde{\leftrightarrow}}X$ is falsified in some ${\bf M}_{n}$.

4 Optimal Covers

By Proposition 4 it is decidable if a given $m$-valued logic M is a cover of C. Since we can enumerate all $m$-valued logics, we can also find all covers of C. Moreover, comparing two many-valued logics as to their sets of tautologies is decidable, as the next theorem will show. Using this result, we see that we can always generate optimal covers for C.

Definition 4.1

For two many-valued logics ${\bf M}_{1}$ and ${\bf M}_{2}$, we write ${\bf M}_{1}\mathrel{\unlhd}{\bf M}_{2}$ iff ${\rm Taut}({\bf M}_{1})\subseteq{\rm Taut}({\bf M}_{2})$.

${\bf M}_{1}$ is better than ${\bf M}_{2}$, ${\bf M}_{1}\mathrel{\lhd}{\bf M}_{2}$, iff ${\bf M}_{1}\mathrel{\unlhd}{\bf M}_{2}$ and ${\rm Taut}({\bf M}_{1})\neq{\rm Taut}({\bf M}_{2})$.

Theorem 4.2

Let two logics ${\bf M}_{1}$ and ${\bf M}_{2}$, $m_{1}$-valued and $m_{2}$-valued respectively, be given. It is decidable whether ${\bf M}_{1}\mathrel{\lhd}{\bf M}_{2}$.

Proof

It suffices to show the decidability of the following property: There is a formula $A$, s.t. (*) ${\bf M}_{2}\models A$ but ${\bf M}_{1}\not\models A$. If this is the case, write ${\bf M}_{1}\mathrel{\lhd}^{*}{\bf M}_{2}$. ${\bf M}_{1}\mathrel{\lhd}{\bf M}_{2}$ iff ${\bf M}_{1}\mathrel{\lhd}^{*}{\bf M}_{2}$ and not ${\bf M}_{2}\mathrel{\lhd}^{*}{\bf M}_{1}$.

We show this by giving an upper bound on the depth of a minimal formula $A$ satisfying the above property. Since the set of formulas of ${\cal L}$ is enumerable, bounded search will produce such a formula iff it exists. Note that the property (*) is decidable by enumerating all assignments. In the following, let $m=\max(m_{1},m_{2})$.

Let $A$ be a formula that satisfies (), i.e., there is a valuation $v$ s.t. $v\not\models_{{\bf M}_{1}}A$. W.l.o.g. we can assume that $A$ contains at most $m$ different variables: if it contained more, some of them must be evaluated to the same truth value in the counterexample $v$ for ${\bf M}_{1}\not\models A$. Unifying these variables leaves () intact.

Let $B=\{B_{1},B_{2},\ldots\}$ be the set of all subformulas of $A$. Every formula $B_{j}$ defines an $m$-valued truth function $f(B_{j})$ of $m$ variables where the values of the variables which actually occur in $B_{j}$ determine the value of $f(B_{j})$ via the matrix of ${\bf M}_{2}$. On the other hand, every $B_{j}$ evaluates to a single truth value $t(B_{j})$ in the countermodel $v$.

Consider the formula $A^{\prime}$ constructed from $A$ as follows: Let $B_{i}$ be a subformula of $A$ and $B_{j}$ be a proper subformula of $B_{i}$ (and hence, a proper subformula of $A$). If $f(B_{i})=f(B_{j})$ and $t(B_{i})=t(B_{j})$, replace $B_{i}$ in $A$ with $B_{j}$. $A^{\prime}$ is shorter than $A$, and it still satisfies (). By iterating this construction until no two subformulas have the desired property we obtain a formula $A^{*}$. This procedure terminates, since $A^{\prime}$ is shorter than $A$; it preserves (), since $A^{\prime}$ remains a tautology under ${\bf M}_{2}$ (we replace subformulas behaving in exactly the same way under all valuations) and the countermodel $v$ is also a countermodel for $A^{\prime}$.

The depth of $A^{*}$ is bounded above by $m^{m^{m}+1}-1$. This is seen as follows: If the depth of $A^{*}$ is $d$, then there is a sequence $A^{*}=B_{0}^{\prime},B_{1}^{\prime},\ldots,B_{d}^{\prime}$ of subformulas of $A^{*}$ where $B_{k}^{\prime}$ is an immediate subformula of $B_{k-1}^{\prime}$. Every such $B_{k}^{\prime}$ defines a truth function $f(B_{k}^{\prime})$ of $m$ variables in ${\bf M}_{2}$ and a truth valued $t(B_{k}^{\prime})$ in ${\bf M}_{1}$ via $v$. There are $m^{m^{m}}$ $m$-ary truth functions of $m$ truth values. The number of distinct truth function-truth value pairs then is $m^{m^{m}+1}$. If $d\geq m^{m^{m}+1}$, then two of the $B_{k}^{\prime}$, say $B_{i}^{\prime}$ and $B_{j}^{\prime}$ where $B_{j}^{\prime}$ is a subformula of $B_{i}^{\prime}$ define the same truth function and the same truth value. But then $B_{i}^{\prime}$ could be replaced by $B_{j}^{\prime}$, contradicting the way $A^{*}$ is defined. ∎

Corollary 1

It is decidable if two many-valued logics define the same set of tautologies. The relation $\mathrel{\unlhd}$ is decidable.

Proof

${\rm Taut}({\bf M}_{1})={\rm Taut}({\bf M}_{2})$ iff neither ${\bf M}_{1}\mathrel{\lhd}^{*}{\bf M}_{2}$ nor ${\bf M}_{2}\mathrel{\lhd}^{*}{\bf M}_{1}$. ∎

Let $\simeq$ be the equivalence relation on $m$-valued logics defined by: ${\bf M}_{1}\simeq{\bf M}_{2}$ iff ${\rm Taut}(M_{1})={\rm Taut}(M_{2})$, and let ${\rm MVL}_{m}$ be the set of all $m$-valued logics over ${\cal L}$with truth value set $\{1,\ldots,m\}$. By ${\cal M}_{m}$ we denote the set of all sets ${\rm Taut}({\bf M})$ of tautologies of $m$-valued logics ${\bf M}$. The partial order $\langle{\cal M}_{m},\subseteq\rangle$ is isomorphic to $\langle{\rm MVL}_{m}/\simeq,\mathrel{\unlhd}/\simeq\rangle$.

Proposition 6

The optimal (i.e., minimal under $\mathrel{\lhd}$) $m$-valued covers of C are computable.

Proof

Consider the set $C_{m}({\bf C})$ of $m$-valued covers of C. Since $C_{m}({\bf C})$ is finite and partially ordered by $\mathrel{\unlhd}$, $C_{m}({\bf C})$ contains minimal elements. The relation $\mathrel{\unlhd}$ is decidable, hence the minimal covers can be computed. ∎

Example 7

By Example 5, IPC is strongly sound for ${\bf G}_{3}$. The best 3-valued approximation of IPC is the 3-valued Gödel logic. In fact, it is the only 3-valued approximation of any sound calculus C (containing modus ponens) for IPL which has less tautologies than classical logic CL. This can be seen as follows: Consider the fragment containing $\bot$ and $\supset$ ($\neg B$ is usually defined as $B\supset\bot$). Let M be some 3-valued strongly sound approximation of C. By Gödel’s double-negation translation, $B$ is a classical tautology iff $\neg\neg B$ is true intuitionistically. Hence, whenever ${\bf M}\models\neg\neg X\supset X$, then ${\rm Taut}({\bf M})\supseteq{\bf CL}$. Let [math] denote the value of $\bot$ in M, and let $1\in V^{+}({\bf M})$. We distinguish cases:

$0\in V^{+}({\bf M})$: Then ${\rm Taut}({\bf M})={\rm Frm}({\cal L})$, since $\bot\supset X$ is true intuitionistically, and by modus ponens: $\bot,\bot\supset X/X$. 2. 2.

$0\notin V^{+}({\bf M})$: Let $u$ be the third truth value.

1. (a)

$u\in V^{+}({\bf M})$: Consider $A\equiv((X\supset\bot)\supset\bot)\supset X$. If $v(X)$ is $u$ or $1$, then, since everything implies something true, $A$ is true (Note that we have $Y,Y\supset(X\supset Y)\vdash X\supset Y$). If $v(X)=0$, then (since $0\supset 0$ is true, but $u\supset 0$ and $1\supset 0$ are both false), $A$ is true as well. So ${\rm Taut}({\bf M})\supseteq{\bf CL}$. 2. (b)

$u\notin V^{+}({\bf M})$, i.e., $V^{+}({\bf M})=\{1\}$: Consider the truth table for implication. Since $B\supset B$, $\bot\supset B$, and something true is implied by everything, the upper right triangle is $1$. We have the following table:

[TABLE]

Clearly, $v_{0}$ cannot be $1$. If $v_{0}=u$, we have, by $((X\supset X)\supset\bot)\supset Y$, that $v_{1}=1$. In this case, ${\bf M}\models A$ and hence ${\rm Taut}({\bf M})\supseteq{\bf CL}$. So assume $v_{0}=0$.

1. i.

$v_{1}=1$: ${\bf M}\models A$ (Note that only the case of $((u\supset 0)\supset 0)\supset u$ has to be checked). 2. ii.

$v_{1}=u$: ${\bf M}\models A$. 3. iii.

$v_{1}=0$: With $v_{2}=0$, M would be incorrect ($u\supset(1\supset u)$ is false). If $v_{2}=1$, again ${\bf M}\models A$. The case of $v_{2}=u$ is the Gödel logic, where $A$ is not a tautology.

Note that it is in general impossible to effectively construct a $\mathrel{\unlhd}$-minimal $m$-valued logic M with ${\bf L}\subseteq{\rm Taut}({\bf M})$ if L is given independently of a calculus, because, e.g., it is undecidable whether L is empty or not: e.g., take

[TABLE]

where $D(x)=0$ is the Diophantine representation of some undecidable set.

5 Effective Sequential Approximations

In the previous section we have shown that it is always possible to obtain the best $m$-valued covers of a given calculus, but there is no way to tell how good these covers are. In this section, we investigate the relation between sequences of many-valued logics and the set of theorems of a calculus C. Such sequences are called sequential approximations of C if they verify all theorems and refute all non-theorems of C, and effective sequential approximations if they are effectively enumerable. This is also a question about the limitations of Bernays’s method. On the negative side, an immediate result says that calculi for undecidable logics do not have effective sequential approximations. If, however, a propositional logic is decidable, it also has an effective sequential approximation (independent of a calculus). Moreover, any calculus has a uniquely defined many-valued closure, whether it is decidable or not. This is the set of all sentences which cannot be proved underivable using a Bernays-style many-valued argument. If a calculus has an effective sequential approximation, then the set of its theorems equals its many-valued closure. If it does not, then its closure is a proper superset. Different calculi for one and the same logic may have different many-valued closures according to their degree of analyticity.

Definition 5.1

Let L be a propositional logic and let ${\bf A}=\langle{\bf M}_{1},{\bf M}_{2},{\bf M}_{3},\ldots,\rangle$ be a sequence of many-valued logics s.t. (1) ${\bf M}_{i}\mathrel{\unlhd}{\bf M}_{j}$ iff $i\geq j$.

A is called a sequential approximation of L iff ${\bf L}=\bigcap_{j\in\omega}{\rm Taut}({\bf M}_{j})$. If in addition A is effectively enumerated, then A is an effective sequential approximation.

If L is given by the calculus C, and each $M_{j}$ is a cover of C, then A is a strong (effective) sequential approximation of C (if A is effectively enumerated).

We say C is effectively approximable, if there is such a strong effective sequential approximation of C.

Condition (1) above is technically not necessary. Approximating sequences of logics in the literature (see next example), however, satisfy this condition. Furthermore, with the emphasis on “approximation,” it seems more natural that the sequence gets successively “better.”

Example 8

Consider the sequence ${\bf G}=\langle{\bf G}_{i}\rangle_{i\geq 2}$ of Gödel logics and intuitionistic propositional logic IPC. ${\rm Taut}({\bf G}_{i})\supset{\rm Thm}({\bf IPC})$, since ${\bf G}_{i}$ is a cover for IPC. Furthermore, ${\bf G}_{i+1}\mathrel{\lhd}{\bf G}_{i}$. This has been pointed out by [10], for a detailed proof see [11, Theorem 10.1.2]. It is, however, not a sequential approximation of IPC: The formula $(A\supset B)\lor(B\supset A)$, while not a theorem of IPL, is a tautology of all ${\bf G}_{i}$. In fact, $\bigcap_{j\geq 2}{\rm Taut}({\bf G}_{i})$ is the set of tautologies of the infinite-valued Gödel logic ${\bf G}_{\aleph}$, which is axiomatized by the rules of IPC plus the above formula. This has been shown in [8] (see also [11, Section 10.1]). Hence, G is a strong effective sequential approximation of ${\bf G}_{\aleph}={\bf IPC}+(A\supset B)\lor(B\supset A)$.

Jaśkowski [13] gave an effective strong sequential approximation of IPC. That IPC is approximable is also a consequence of Theorem 5.6, with the proof adapted to Kripke semantics for intuitionistic propositional logic, since IPL has the finite model property [9, Ch. 4, Theorem 4(a)].

The natural question to ask is: Which logics have (effective) sequential approximations; which calculi are approximable?

First of all, any propositional logic has a sequential approximation, although it need not have an effective approximation.

Proposition 7

Every propositional logic L has a sequential approximation.

Proof

A sequential approximation of L a is given by ${\bf M}_{i}={\bf M}_{i,i}({\bf L})$ (see Definition 2.9). Any formula $F\notin{\bf L}$ is in $V({\bf M}_{k})$ for $k=\max\{\mathrm{dp}(F),j\}$ where $j$ is the maximum index of variables occurring in $F$. By Proposition 1, $F$ is falsified in ${\bf M}_{k}$. Also, ${\rm Taut}({\bf M}_{i})\supseteq{\bf L}$, and ${\bf M}_{i}\mathrel{\unlhd}{\bf M}_{i+1}$. ∎

Corollary 2

If L is decidable, it has an effective sequential approximation.

Proof

Using a decision procedure for L, we can effectively enumerate the ${\bf M}_{i,i}({\bf L})$. ∎

Proposition 8

If L has an effectively sequential approximation, then ${\rm Frm}({\cal L})\setminus{\bf L}$ is effectively enumerable.

Proof

Suppose there is an effectively enumerated sequence ${\bf A}=\langle{\bf M}_{1},{\bf M}_{2},\ldots\rangle$ s.t. $\bigcap_{j\geq 2}{\rm Taut}({\bf M}_{j})={\bf L}$. If $F\notin{\bf L}$ then there would be an index $i$ s.t. $F$ is false in ${\bf M}_{i}$. But this would yield a semi-decision procedure for non-members of L: Try for each $j$ whether $F$ is false in ${\bf M}_{j}$. If $F\notin{\bf L}$, this will be established at $j=i$. ∎

Corollary 3

If C is undecidable, then it is not effectively approximable.

Proof

${\rm Thm}({\bf C})$ is effectively enumerable. If C were approximable, it would have an effective sequential approximation, and this contradicts the assumption that the non-theorems of C are not effectively enumerable. ∎

Example 9

This shows that a result similar to that for IPC cannot be obtained for full propositional linear logic.

If C is not effectively approximable (e.g., if it is undecidable), then the intersection of all covers for C is a proper superset of ${\rm Thm}({\bf C})$. This intersection has interesting properties.

Definition 5.2

The many-valued closure ${\rm MC}({\bf C})$ of a calculus C is the set of formulas which are true in every many-valued cover for C.

Proposition 9

${\rm MC}({\bf C})$* is unique and has an effective sequential approximation.*

Proof

${\rm MC}({\bf C})$ is unique, since it obviously equals $\bigcap_{{\bf M}\in S}{\rm Taut}({\bf M})$ where $S$ is the set of all covers for C. It is also effectively approximable, an approximating sequence is given by

[TABLE]

where ${\bf M}_{i}^{\prime}$ is an effective enumeration of $S$. ∎

Since ${\rm MC}({\bf C})$ is defined via the many-valued logics for which ${\bf C}$ is strongly sound, it need not be the case that ${\rm MC}({\bf C})={\rm Thm}({\bf C})$ even if ${\bf C}$ is decidable. (An example is given below.) On the other hand, it also need not be trivial (i.e., equal to ${\rm Frm}({\cal L})$) even for undecidable C. For instance, take the Hilbert-style calculus for linear logic given in [1, 19], and the 2-valued logic which interprets the linear connectives classically and the exponentials as the identity. All axioms are then tautologies and the rules (modus ponens, adjunction) are strongly sound, but the matrix is clearly non-trivial.

Corollary 4

If C is strictly analytic, then ${\rm MC}({\bf C})={\rm Thm}({\bf C})$.

Proof

We have to show that for every $F\notin{\rm Thm}({\bf C})$ there is a finite-valued logic ${\bf M}$ which is strongly sound for ${\bf C}$ and where $F\notin{\rm Taut}({\bf M})$. Let $X_{1}$, …, $X_{j}$ be all the variables occurring in $F$ and the axioms and rules of C. Then set ${\bf M}={\bf M}_{\mathrm{dp}(F),j}({\rm Thm}({\bf C}))$.

By Proposition 1, $F\notin{\rm Taut}({\bf M})$ and all axioms of C are in ${\rm Taut}({\bf M})$. Now consider a valuation $v$ in M and suppose $v(A_{i})\in V^{+}$ for all premises $A_{i}$ of a rule of C. We have two cases: if $v(X)=\top$ for some variable $X$ appearing in a premise $A_{i}$, then, since C is strictly analytic, $X$ also appears in the conclusion $C$ and hence $v(C)=\top$. Otherwise, let $\sigma_{v}$ be the substitution corresponding to $v$. If $v(A_{i})=\top$ for some $i$, this means that $\mathrm{dp}(A_{i}\sigma)>\mathrm{dp}(F)$. By strict analyticity, $\mathrm{dp}(C\sigma)\geq\mathrm{dp}(A_{i}\sigma)>\mathrm{dp}(F)$ and hence $v(C)=\top$. Otherwise, $v(A_{i})=A_{i}\sigma$ for all premises $A_{i}$. Since $v(A_{i})$ is designated, $A_{i}\sigma\in{\rm Thm}({\bf C})$, hence $C\sigma\in{\rm Thm}({\bf C})$. Then either $v(C)=C\sigma$ or $v(C)=\top$, and both are in $V^{+}$. ∎

Example 10

The last corollary can be used to uniformly obtain semantics for strictly analytic Hilbert calculi. Strict analyticity of the calculus is a necessary condition, as Example 3 shows. The calculus given there is decidable, though not strictly analytic, and has only trivial covers. Its set of theorems nevertheless has an effective sequential approximation, i.e., it is the intersection of an infinite sequence of finite-valued matrices which are weakly sound for C. For this it is sufficient to give, for each formula $A$ s.t. ${\bf C}\nvdash A$, a matrix M weakly sound for C with $A\notin{\rm Taut}({\bf M})$. Let the depth of $A$ be $k$, and let

[TABLE]

Then set $V=V_{k}$, $V^{+}=\{B\vartriangleleft C\mid B\vartriangleleft C\in V,C\equiv\square^{l}B\}\cup\{\dagger\}$. The truth functions are defined as follows:

[TABLE]

The axiom $X\vartriangleleft\square X$ is a tautology. For if $v(X)=\dagger$, then $v(\square X)=\dagger$ and hence $v(X\vartriangleleft\square X)=\dagger\in V^{+}$. If $v(X)\in V_{k}$ but $\notin V_{k-1}$, then $v(\square X)=\dagger$ and $v(X\vartriangleleft\square X)=\dagger$. Otherwise $v(\square X)=\square B$ for $B=v(A)$ and $v(X\vartriangleleft\square X)=\dagger$ (if $\square B\in V_{k}$) or $=B\vartriangleleft\square B\in V^{+}$.

If $v(X)=\dagger$, then $v(X\vartriangleleft Z)=\dagger$. Otherwise $v(X\vartriangleleft Z)\in V^{+}$ only if $v(X)=B$ and $v(Y)=\square^{l}B$ and $B\notin V_{k}$. Then, in order for $v(Y\vartriangleleft Z)$ to be $\in V^{+}$, either $v(Y\vartriangleleft Z)=\dagger$, in which case $v(Z)\in V_{k}$ but $\notin V_{k-1}$, and hence $v(Y\vartriangleleft Z)=\dagger$, or $v(Y\vartriangleleft Z)=\square^{l}B\vartriangleleft\square^{l^{\prime}}B$ with $l<l^{\prime}$, in which case $v(Y\vartriangleleft Z)=B\vartriangleleft\square^{l^{\prime}}B$.

However, $A\notin Taut({\bf M})$. For it is easy to see by induction that in the valuation with $v(X)=X$ for all variables $X\in\mathord{\rm Var}(A)$, $v(B)=B$ as long as $B\in V_{k}$ and so $v(A)$ can only be designated if $A\equiv B\vartriangleleft\square B$ for some $B$, but all such formulas are derivable in C.

However, there are substitution instances of $X\vartriangleleft X$, viz., for any $\sigma$ with $X\sigma$ of depth $>k$, for which $(X\vartriangleleft X)\sigma$ is a tautology. Even though C is weakly sound for M, it is not t-sound.

So far we have concentrated on approximations of logics given via calculi. However, propositional logics are also often defined via their semantics. The most important example of such logics are modal logics, where logics can be characterized using families of Kripke structures. If these Kripke structures satisfy certain properties, they also yield sequential approximations of the corresponding logics. Unsurprisingly, for this it is necessary that the modal logics have the finite model property, i.e., they can be characterized by a family of finite Kripke structures. The sequential approximations obtained by our method are only effective, however, if the Kripke structures are effectively enumerable.

Definition 5.3

A modal logic L has as its language ${\cal L}$ the usual propositional connectives plus two unary modal operators: $\square$ (necessary) and $\Diamond$ (possible). A Kripke model for $\cal L$ is a triple $\langle W,R,P\rangle$, where

$W$ is any set: the set of worlds, 2. 2.

$R\subseteq W^{2}$ is a binary relation on $W$: the accessibility relation, 3. 3.

$P$ is a mapping from the propositional variables to subsets of $W$.

A modal logic L is characterized by a class of Kripke models for L.

This is called the standard semantics for modal logics (see [7, Ch. 3]). The semantics of formulas in standard models is defined as follows:

Definition 5.4

Let L be a modal logic, ${\cal K}_{\bf L}$ be its characterizing class of Kripke models. Let $K=\langle W,R,P\rangle\in{\cal K}_{\bf L}$ be a Kripke model and $A$ be a modal formula.

If $\alpha\in W$ is a possible world, then we say $A$ is true in $\alpha$, $\alpha\models_{\bf L}A$, iff the following holds:

$A$ is a variable: $\alpha\in P(X)$ 2. 2.

$A\equiv\neg B$: not $\alpha\models_{\bf L}B$ 3. 3.

$A\equiv B\land C$: $\alpha\models_{\bf L}B$ and $\alpha\models_{\bf L}C$ 4. 4.

$A\equiv B\lor C$: $\alpha\models_{\bf L}B$ or $\alpha\models_{\bf L}C$ 5. 5.

$A\equiv\square B$: for all $\beta\in W$ s.t. $\alpha\mathrel{R}\beta$ it holds that $\beta\models_{\bf L}B$ 6. 6.

$A\equiv\Diamond B$: there is a $\beta\in W$ s.t. $\alpha\mathrel{R}\beta$ and $\beta\models_{\bf L}B$

We say $A$ is true in $K$, $K\models_{\bf L}A$, iff for all $\alpha\in W$ we have $\alpha\models_{\bf L}A$. $A$ is *valid in *L, ${\bf L}\models A$, iff $A$ is true in every Kripke model $K\in{\cal K}_{\bf L}$. By ${\rm Taut}({\bf L})$ we denote the set of all formulas valid in L.

Many of the modal logics in the literature have the finite model property (fmp): for every $A$ s.t. ${\bf L}\not\models A$, there is a finite Kripke model $K=\langle W,R,P\rangle\in{\cal K}$ (i.e., $W$ is finite), s.t. $K\not\models_{\bf L}A$ (where L is characterized by ${\cal K}$). We would like to exploit the fmp to construct sequential approximations. This can be done as follows:

Definition 5.5

Let $K=\langle W,R,P\rangle$ be a finite Kripke model. We define the many-valued logic ${\bf M}_{K}$ as follows:

$V({\bf M}_{K})=\{0,1\}^{W}$, the set of 0-1-sequences with indices from $W$. 2. 2.

$V^{+}({\bf M}_{K})=\{1\}^{W}$, the singleton of the sequence constantly equal to 1. 3. 3.

$\widetilde{\neg}_{{\bf M}_{K}}$, $\widetilde{\lor}_{{\bf M}_{K}}$, $\widetilde{\land}_{{\bf M}_{K}}$, $\widetilde{\supset}_{{\bf M}_{K}}$ are defined componentwise from the classical truth functions 4. 4.

$\widetilde{\vphantom{l}\square}_{{\bf M}_{K}}$ is defined as follows:

[TABLE] 5. 5.

$\widetilde{\vphantom{l}\Diamond}_{{\bf M}_{K}}$ is defined as follows:

[TABLE]

Furthermore, $v_{K}$ is the valuation defined by $v_{K}(X)_{\alpha}=1$ iff $\alpha\in P(X)$ and $=0$ otherwise.

Lemma 2

Let ${\bf L}$ and $K$ be as in Definition 5.5. Then the following hold:

Every valid formula of L is a tautology of ${\bf M}_{K}$. 2. 2.

If $K\not\models_{\bf L}A$ then $v_{K}\not\models_{{\bf M}_{K}}A$.

Proof

Let $B$ be a modal formula, and $K^{\prime}=\langle W,R,P^{\prime}\rangle$. We prove by induction that $v_{K^{\prime}}(B)_{\alpha}=1$ iff $\alpha\models_{\bf L}B$:

$B$ is a variable: $P^{\prime}(B)=W$ iff $v_{K}(B)_{\alpha}=1$ for all $\alpha\in W$ by definition of $v_{K}$.

$B\equiv\neg C$: By the definition of $\widetilde{\neg}_{{\bf M}_{K}}$, $v_{K}(B)_{\alpha}=1$ iff $v_{K}(C)_{\alpha}=0$. By induction hypothesis, this is the case iff $\alpha\not\models_{\bf L}C$. This in turn is equivalent to $\alpha\models_{\cal K}B$. Similarly if $B$ is of the form $C\land D$, $C\lor D$, and $C\supset D$.

$B\equiv\square C$: $v_{K}(B)_{\alpha}=1$ iff for all $\beta$ with $\alpha\mathrel{R}\beta$ we have $v_{K}(C)_{\beta}=1$. By induction hypothesis this is equivalent to $\beta\models_{\bf L}C$. But by the definition of $\square$ this obtains iff $\alpha\models_{\bf L}B$. Similarly for $\Diamond$.

(1) Every valuation $v$ of ${\bf M}_{K}$ defines a function $P_{v}$ via $P_{v}(X)=\{\alpha\mid v(X)_{\alpha}=1\}$. Obviously, $v=v_{P_{v}}$. If ${\bf L}\models B$, then $\langle W,R,P_{v}\rangle\models_{\bf L}B$. By the preceding argument then $v(B)_{\alpha}=1$ for all $\alpha\in W$. Hence, $B$ takes the designated value under every valuation.

(2) Suppose $A$ is not true in $K$. This is the case only if there is a world $\alpha$ at which it is not true. Consequently, $v_{K}(A)_{\alpha}=0$ and $A$ takes a non-designated truth value under $v_{K}$. ∎

The above method can be used to construct many-valued logics from Kripke structures for not only modal logics, but also for intuitionistic logic. Kripke semantics for IPL are defined analogously, with the exception that $\alpha\models A\supset B$ iff $\beta\models A\supset B$ for all $\beta\in W$ s.t. $\alpha\mathrel{R}\beta$. IPL is then characterized by the class of all finite trees [9, Ch. 4, Thm. 4(a)]. Note, however, that for intuitionistic Kripke semantics the form of the assignments $P$ is restricted: If $w_{1}\in P(X)$ and $w_{1}\mathrel{R}w_{2}$ then also $w_{2}\in P(X)$ [9, Ch. 4, Def. 8]. Hence, the set of truth values has to be restricted in a similar way. Usually, satisfaction for intuitionistic Kripke semantics is defined by satisfaction in the initial world. This means that every sequence where the first entry equals 1 should be designated. By the above restriction, the only such sequence is the constant 1-sequence.

Example 11

The Kripke tree with three worlds

[TABLE]

yields a five-valued logic ${\bf T}_{3}$, with $V({\bf T_{3}})=\{000,001,010,011,111\}$, $V^{+}({\bf T_{3}})=\{111\}$, the truth table for implication

[TABLE]

$\bot$ is the constant $000$, $\neg A$ is defined by $A\supset\bot$, and $\lor$ and $\land$ are given by the componentwise classical operations.

The Kripke chain with four worlds corresponds directly to the five-valued Gödel logic ${\bf G}_{5}$. It is well know that $(X\supset Y)\lor(Y\supset X)$ is a tautology in all ${\bf G}_{m}$. Since ${\bf T}_{3}$ falsifies this formula (take $001$ for $X$ and $010$ for $Y$), we know that ${\bf G}_{5}$ is not the best five-valued approximation of IPL.

Furthermore, let

[TABLE]

$O_{5}$ assures that the truth values assumed by $X_{1}$, …, $X_{5}$ are linearly ordered by implication. Since neither $010\supset 001$ nor $001\supset 010$ is true, we see that there are only four truth values which can be assigned to $X_{1}$, …, $X_{5}$ making $O_{5}$ true. Consequently, $O_{5}\supset F_{5}$ is valid in ${\bf T}_{3}$. On the other hand, $F_{5}$ is false in ${\bf G}_{5}$.

Theorem 5.6

Let L be a modal logic characterized by a set of finite Kripke models ${\cal K}=\{K_{1},K_{2},\ldots\}$. A sequential approximation of L is given by $\langle{\bf M}_{1},{\bf M}_{2},\ldots\rangle$ where ${\bf M}_{1}={\bf M}_{K_{1}}$, and ${\bf M}_{i+1}={\bf M}_{i}\times{\bf M}_{K_{i+1}}$. This approximation is effective if ${\cal K}$ is effectively enumerable.

Proof

(1) ${\rm Taut}({\bf M}_{i})\supseteq{\rm Taut}({\bf L})$: By induction on $i$: For $i=1$ this is Lemma 2 (1). For $i>1$ the statement follows from Lemma 1, since ${\rm Taut}({\bf M}_{i-1})\supseteq{\rm Taut}({\bf L})$ by induction hypothesis, and ${\rm Taut}({\bf M}_{K_{i}})\supseteq{\rm Taut}({\bf L})$ again by Lemma 2 (1).

(2) ${\bf M}_{i}\mathrel{\unlhd}{\bf M}_{i+1}$ from $A\cap B\subseteq A$ and Lemma 1.

(3) ${\rm Taut}({\bf L})=\bigcap_{i\geq 1}{\rm Taut}({\bf M}_{i})$. The $\subseteq$-direction follows immediately from (1). Furthermore, by Lemma 2 (2), no non-tautology of L can be a member of all ${\rm Taut}({\bf M}_{i})$, whence $\supseteq$ holds. ∎

Remark 3

Finitely axiomatizable modal logics with the fmp always have an effective sequential approximation, since it is then decidable if a given finite Kripke structure satisfies the axioms. Urquhart [20] has shown that this is not true if the assumption is weakened to recursive axiomatizability, by giving an example of an undecidable recursively axiomatizable modal logic with the fmp. Since this logic cannot have an effective sequential approximation, its characterizing family of finite Kripke models is not effectively enumerable. The preceding theorem thus also shows that the many-valued closure of a calculus for a modal logic with the fmp equals the logic itself, provided that the calculus contains modus ponens and necessitation as the only rules. (All standard axiomatizations are of this form.)

6 Conclusion

Our brief discussion unfortunate must leave many interesting questions open, and suggests further questions which might be topics for future research. The main open problem is of course whether the approach used here can be extended to the case of first-order logic. There are two distinct questions: The first is how to check if a given finite-valued matrix is a cover for a first-order calculus. Is this decidable? One might expect that it is at least for “standard” formulations of first-order rules, e.g., where the rules involving quantifiers are monadic in the sense that they only involve one variable per rule. The second question is whether the relationship $\mathrel{\lhd}^{*}$ is decidable for $n$-valued first order logics. Another problem, especially in view of possible applications in computer science, is the complexity of the computation of optimal covers. One would expect that it is tractable at least for some reasonable classes of calculi which are syntactically characterizable.

We have shown that for strictly analytic calculi, the many-valued closure coincides with the set of theorems, i.e., that they are effectively approximable by their finite-valued covers. Is it possible to extend this result to a wider class of calculi, in particular, what can be said about calculi in which modus ponens is the only rule of inference (so-called Frege systems)? For calculi which are not effectively approximable, it would still be interesting to characterize the many-valued closure. For instance, we have seen that the many-valued closure of linear logic is not equal to linear logic (since linear logic is undecidable) but also not trivial (since all classical non-tautologies are falsified in a 2-valued cover). What is the many-valued closure of linear logic? For those (classes of) logics for which we have shown that sequential approximations are possible, our methods of proof also do not yield optimal solutions. For instance, for modal logics with the finite model property we have shown that all non-valid formulas can be falsified in the many-value logic obtained by coding the corresponding Kripke countermodel. But there may be logics with fewer truth-values which also falsify these formulas. A related question is to what extent our results on approximability still hold if we restrict attention to many-valued logics in which only one truth-value is designated. The standard examples of sequences of finite-valued logics approximating, e.g., Łukasiewicz or intuitionistic logic are of this form, but it need not be the case that every approximable logic can be approximated by logics with only one designated value.