1 Introduction
A sentential connective
$\star $
is said to be univocal, relative to a formal system
$\mathcal {F}$
for a sentential logic containing
$\star $
iff any two connectives
$\star _1$
and
$\star _2$
which satisfy the same
$\mathcal {F}$
rules (and axioms) as
$\star $
are such that similar formulas involving
$\star _1$
and
$\star _2$
are inter-derivable in
$\mathcal {F}$
.Footnote
1
To be more precise, suppose
$\star $
is a unary connective. Then
$\star $
is univocal relative to
$\mathcal {F}$
iff for any
$\star _1$
and
$\star _2$
satisfying the same principles as
$\star $
in
$\mathcal {F}$
, we have
$\star _1 \alpha \vdash _{\mathcal {F}} \star _2 \alpha $
. And, if
$\star $
is binary, then
$\star $
is univocal relative to
$\mathcal {F}$
iff for any
$\star _1$
and
$\star _2$
satisfying the same principles as
$\star $
in
$\mathcal {F}$
, we have
$\alpha \star _1 \beta \vdash _{\mathcal {F}} \alpha \star _2 \beta $
. In order to illustrate this definition of univocity, it is helpful to begin with a simple historical example.
It is easy to see that the conditional
$\to $
is univocal, relative to Gentzen’s (intuitionistic and classical) natural deduction systems
$\mathbf {LJ}$
and
$\mathbf {LK}$
[Reference Gentzen5]. In both of these systems, if we suppose there are two conditionals (
$\to _1$
and
$\to _2$
) satisfying Gentzen’s introduction and elimination rules for
$\to $
, then we can quickly prove that
$\alpha \to _1 \beta \vdash \alpha \to _2 \beta $
, as follows:
Similar straightforward derivations may be found in order to prove that the connectives
$\land $
,
$\lor $
,
$\bot $
, and
$\neg $
are each univocal, relative to Gentzen’s system
$\mathbf {LJ}$
(proofs omitted).
Also, it is well known, as Gentzen himself observed in [Reference Gentzen5, Section 5], that
$\mathbf {LJ}$
and
$\mathbf {LK}$
have the same derivations as the Hilbert systems for intuitionistic and classical sentential logic (
$\mathbf {LHJ}$
and
$\mathbf {LHK}$
). That is
$\Gamma \vdash _{\mathbf {LJ}} \alpha $
iff
$\Gamma \vdash _{\mathbf {LHJ}} \alpha $
; and,
$\Gamma \vdash _{\mathbf {LK}} \alpha $
iff
$\Gamma \vdash _{\mathbf {LHK}} \alpha $
.
In this context, it is natural to ask whether the conditional and the other connectives are also univocal, relative to the Hilbert systems for intuitionistic and classical sentential logic (
$\mathbf {LHJ}$
and
$\mathbf {LHK}$
). This is what will be considered in what follows.
We begin by reminding the reader of the axiomatic systems
$\mathbf {LHJ}$
and
$\mathbf {LHK}$
. The system
$\mathbf {LHJ}$
consists of modus ponens, plus the following ten axiom schemata:
(
$\mathbf {LHJ}_1$
)
$\beta \to (\alpha \to \beta )$
,
(
$\mathbf {LHJ}_2$
)
$(\gamma \to (\alpha \to \beta )) \to ((\gamma \to \alpha ) \to (\gamma \to \beta ))$
,
(
$\mathbf {LHJ}_3$
)
$\alpha \to (\beta \to (\alpha \wedge \beta )$
,
(
$\mathbf {LHJ}_4$
)
$(\alpha \wedge \beta ) \to \alpha $
,
(
$\mathbf {LHJ}_5$
)
$(\alpha \wedge \beta ) \to \beta $
,
(
$\mathbf {LHJ}_6$
)
$(\alpha \to \gamma ) \to ((\beta \to \gamma ) \to ((\alpha \lor \beta ) \to \gamma ))$
,
(
$\mathbf {LHJ}_7$
)
$\alpha \to (\alpha \vee \beta )$
,
(
$\mathbf {LHJ}_8$
)
$\beta \to (\alpha \vee \beta )$
,
(
$\mathbf {LHJ}_9$
)
$(\alpha \to \beta ) \to ((\alpha \to \neg \beta ) \to \neg \alpha )$
,
(
$\mathbf {LHJ}_{10}$
)
$\neg \alpha \to (\alpha \to \beta )$
.
One nice feature of
$\mathbf {LHJ}$
is that the fragments of
$\mathbf {LHJ}$
can be picked out simply by selecting those axioms which contain the connectives in question. This is not so for the system
$\mathbf {LHK}$
, which has all ten axioms of
$\mathbf {LHJ}$
plus the following eleventh axiom:Footnote
2
(
$LEM$
)
$\alpha \vee \neg \alpha $
.
Famously, this extension of
$\mathbf {LHJ}$
is non-conservative. The implicational fragment of
$\mathbf {LHK}$
contains theorems not derivable in
$\mathbf {LHJ}$
—specifically, Peirce’s Law, that is,
(P)
$((\alpha \to \beta ) \to \alpha ) \to \alpha $
.
One can easily obtain the implicational fragment of
$\mathbf {LHK}$
by adding (P) to the implicational fragment of
$\mathbf {LHJ}$
. But, it would be preferable for our purposes to adopt a Hilbert system for classical sentential logic that allows us to easily extract all of the fragments of classical logic (just by selecting the axioms containing those connectives), as can be done with
$\mathbf {LHJ}$
. To that end, we will adopt the following alternative (equivalent) axiomatization as our classical, Hilbert system
$\mathbf {LHK}$
. It differs in two ways from
$\mathbf {LHJ}$
in the axioms containing implication and negation. Specifically, our
$\mathbf {LHK}$
replaces (
$\mathbf {LHJ}_9$
) and (
$\mathbf {LHJ}_{10}$
) with the following two axioms:
(
$\mathbf {LHK}_9$
)
$(\neg \beta \to \neg \alpha ) \to (\alpha \to \beta )$
,
(
$\mathbf {LHK}_{10}$
)
$((\alpha \to \beta ) \to \alpha ) \to \alpha $
.
Thus, our system
$\mathbf {LHK}$
consists of modus ponens, plus the ten axioms
$\mathbf {LHJ}_1$
–
$\mathbf {LHJ}_8$
, and
$\mathbf {LHK}_9$
and
$\mathbf {LHK}_{10}$
. Because our
$\mathbf {LHJ}$
and
$\mathbf {LHK}$
share these first eight axioms, we will refer to these axioms sometimes as
$\mathbf {LHJ}_1$
–
$\mathbf {LHJ}_8$
and sometimes as
$\mathbf {LHK}_1$
–
$\mathbf {LHK}_8$
, depending on what formal system(s) we are discussing in the context. Moreover, although the resulting axiomatization is now redundant (as
$\mathbf {LHK}_{10}$
follows from
$\mathbf {LHK}_1$
,
$\mathbf {LHK}_2$
, and
$\mathbf {LHK}_9$
), we can now simply speak about a fragment of
$\mathbf {LHK}$
as involving only those axioms of
$\mathbf {LHK}$
that contain the connectives appearing in the fragment in question.
In Section 2, we will discuss questions of univocity of connectives in (fragments of)
$\mathbf {LHJ}$
. In Section 3, we will discuss questions of univocity of connectives in (fragments of)
$\mathbf {LHK}$
. In Section 4, we will discuss questions of univocity of connectives in some alternative formal systems for classical sentential logic that use the Sheffer stroke.
2 Univocity in Hilbert systems for intuitionism
2.1 Non-univocity of the intuitionistic conditional
Interestingly, the conditional is not univocal, relative to the usual Hilbert systems for the implicational fragment of intuitionistic logic. More precisely, we have the following.
Theorem 1. There exist conditionals
$\to _1$
and
$\to _2$
such that (a) both conditionals satisfy the laws of the implicational fragment
$\mathbf {LHJ}^\to $
of
$\mathbf {LHJ}$
; but, (b)
$\alpha \to _1 \beta \nvdash \alpha \to _2 \beta $
.
This result was known since at least 1962 (see [Reference Smiley15, p. 430]) where a four-element counter-model is presented (see below). We recently discovered the following three-element counter-model.Footnote 3
$$ \begin{align*} \begin{array}{l|c|c|r} \to_1&1&2&3\\ \hline 1&1&2&2\\ \hline 2&1&1&1\\ \hline 3&1&1&1 \end{array} \hspace{48pt} \begin{array}{l|c|c|r} \to_2&1&2&3\\ \hline 1&1&2&3\\ \hline 2&1&1&3\\ \hline 3&1&2&1 \end{array} \end{align*} $$
So, in this model, the (sole) designated value is 1 (i.e., all and only formulas assigned the value 1 by the model are theorems of the logic defined by these 3-valued characteristic matrices). Inspection of the model reveals that (a) both conditionals satisfy modus ponens and axioms
$\mathbf {LHJ}_1$
and
$\mathbf {LHJ}_2$
; but, (b)
$2 \to _1 3 \nvdash 2 \to _2 3$
, since
$2 \to _1 3$
is assigned the designated value
$1$
, but
$2 \to _2 3$
is assigned the non-designated value
$3$
.
In fact, a stronger result was established by Smiley [Reference Smiley15]. As it turns out, the conditional is not univocal, relative to
$\mathbf {LHJ}$
as a whole. That is, even if two conditionals
$\to _1$
and
$\to _2$
satisfy all of the laws of
$\mathbf {LHJ}$
, it will still not generally be the case that
$\alpha \to _1 \beta \vdash \alpha \to _2 \beta $
.
Theorem 2. There exist two conditionals
$\to _1$
and
$\to _2$
such that (a) both conditionals satisfy all the laws of
$\mathbf {LHJ}$
; but, (b)
$\alpha \to _1 \beta \nvdash \alpha \to _2 \beta $
.
Proof In this case, four-element counter-models are required. Here is the model Smiley reports in [Reference Smiley15, p. 430].Footnote 4
$$ \begin{align*} \begin{array}{c|c|c|c|c} \to_1&1&2&3&4\\ \hline 1&1&2&3&4\\ \hline 2&1&1&1&4\\ \hline 3&1&1&1&4\\ \hline 4&1&1&1&1 \end{array} \hspace{48pt} \begin{array}{c|c|c|c|c} \to_2&1&2&3&4\\ \hline 1&1&2&3&4\\ \hline 2&1&1&3&4\\ \hline 3&1&1&1&4\\ \hline 4&1&1&1&1 \end{array} \\[18pt] \begin{array}{c|c|c|c|c} \wedge&1&2&3&4\\ \hline 1&1&2&3&4\\ \hline 2&2&2&3&4\\ \hline 3&3&3&3&4\\ \hline 4&4&4&4&4 \end{array} \hspace{48pt} \begin{array}{c|c|c|c|c} \vee&1&2&3&4\\ \hline 1&1&1&1&1\\ \hline 2&1&2&2&2\\ \hline 3&1&2&3&3\\ \hline 4&1&2&3&4 \end{array} \\[18pt] \begin{array}{c|c|c|c|c} &1&2&3&4\\ \hline \neg&4&4&4&1 \end{array}\qquad\qquad\quad \end{align*} $$
Inspection of the model reveals that (a) both conditionals satisfy modus ponens and axioms
$\mathbf {LHJ}_1$
–
$\mathbf {LHJ}_{10}$
; but, (b)
$2 \to _1 3 \nvdash 3 \to _2 3$
, since
$2 \to _1 3$
is assigned the designated value
$1$
, but
$2 \to _2 3$
is assigned the non-designated value
$3$
.
Remark Theorem 2 implies that the axiomatic presentations of all substructural logics (see [Reference Paoli12, Section 2.3] for a survey) have non-univocal conditionals.
2.2 Univocity of the other intuitionistic connectives
The other connectives are univocal, relative to
$\mathbf {LHJ}$
. For each connective, we will prove a corresponding positive theorem to establish this.
Theorem 3. If two conjunctions
$\land _1$
and
$\land _2$
each satisfy the laws of the implication-conjunction fragment
$\mathbf {LHJ}^{\to ,\wedge }$
of
$\mathbf {LHJ}$
, then
$\alpha \land _1 \beta \vdash \alpha \land _2 \beta $
.
Proof Here is a derivation of
$\alpha \land _1 \beta \vdash \alpha \land _2 \beta $
, where MP is modus ponens.
The strategy here is to eliminate
$\land _1$
and then introduce
$\land _2$
. A similar strategy will work for the other connectives as well.
Theorem 4. If two disjunctions
$\lor _1$
and
$\lor _2$
each satisfy the laws of the implication-disjunction fragment
$\mathbf {LHJ}^{\to ,\lor }$
of
$\mathbf {LHJ}$
, then
$\alpha \lor _1 \beta \vdash \alpha \lor _2 \beta $
.
Proof Here is a derivation of
$\alpha \lor _1 \beta \vdash \alpha \lor _2 \beta $
.
Here, we first introduce
$\lor _2$
and then eliminate
$\lor _1$
.
Theorem 5. If two negations
$\neg _1$
and
$\neg _2$
each satisfy the laws of the implication-negation fragment
$\mathbf {LHJ}^{\to ,\neg }$
of
$\mathbf {LHJ}$
, then
$\neg _1 \alpha \vdash \neg _2 \alpha $
.
Proof Here is a derivation of
$\neg _1 \alpha \vdash \neg _2 \alpha $
.
Here, we omit the derivation of step 3, which is a well-known theorem of the implicational fragment
$\mathbf {LHJ}^{\to }$
of
$\mathbf {LHJ}$
.
3 Univocity in Hilbert systems for classical logic
It follows from the results in Section 2.2 that the connectives
$\wedge ,\vee ,\neg $
are univocal, relative to (the relevant fragments of)
$\mathbf {LHK}$
. The only remaining questions involve the univocity of the conditional in (fragments of)
$\mathbf {LHK}$
. Here, there are two positive results and two negative results. We begin with the negative results.
Theorem 6. The conditional is non-univocal, relative to the implication-conjunction fragment
$\mathbf {LHK}^{\to ,\wedge }$
of
$\mathbf {LHK}$
.Footnote
5
Proof In this case, four-element counter-models are required. Here is one.
$$ \begin{align*} \begin{array}{c|c|c|c|c} \to_1&1&2&3&4\\ \hline 1&1&2&2&2\\ \hline 2&1&1&1&1\\ \hline 3&1&1&1&1\\ \hline 4&1&1&1&1 \end{array} \hspace{48pt} \begin{array}{c|c|c|c|c} \to_2&1&2&3&4\\ \hline 1&1&2&3&4\\ \hline 2&1&1&3&3\\ \hline 3&1&2&1&2\\ \hline 4&1&1&1&1 \end{array} \\[18pt] \begin{array}{c|c|c|c|c} \wedge&1&2&3&4\\ \hline 1&1&2&3&4\\ \hline 2&2&2&4&4\\ \hline 3&3&4&3&4\\ \hline 4&4&4&4&4 \end{array}\qquad\qquad\qquad \end{align*} $$
Inspection of the model reveals that (a) both conditionals satisfy modus ponens and axioms
$\mathbf {LHK}_1$
–
$\mathbf {LHK}_{5}$
, and
$\mathbf {LHK}_{10}$
(Peirce’s Law); but, (b)
$2 \to _1 3 \nvdash 2 \to _2 3$
, since
$2 \to _1 3$
is assigned the designated value
$1$
, but
$2 \to _2 3$
is assigned the non-designated value
$3$
.
Theorem 7. The conditional is non-univocal, relative to the implication-negation fragment
$\mathbf {LHK}^{\to ,\neg }$
of
$\mathbf {LHK}$
.
Proof In this case, six-element counter-models are required. Here, we report an eight-element counter-model.Footnote 6
$$ \begin{align*} \begin{array}{c|cccccccc} \to_1 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ \hline 1 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ 2 & 1 & 1 & 1 & 5 & 5 & 5 & 1 & 5 \\ 3 & 1 & 7 & 1 & 6 & 5 & 6 & 7 & 5 \\ 4 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 \\ 5 & 1 & 2 & 3 & 2 & 1 & 7 & 7 & 3 \\ 6 & 1 & 3 & 3 & 3 & 1 & 1 & 1 & 3 \\ 7 & 1 & 3 & 3 & 8 & 5 & 5 & 1 & 8 \\ 8 & 1 & 7 & 1 & 7 & 1 & 7 & 7 & 1 \\ \end{array} \hspace{48pt} \begin{array}{c|cccccccc} \to_2 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ \hline 1 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ 2 & 1 & 1 & 3 & 5 & 5 & 7 & 7 & 3 \\ 3 & 1 & 2 & 1 & 6 & 7 & 6 & 7 & 2 \\ 4 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 \\ 5 & 1 & 2 & 1 & 2 & 1 & 2 & 1 & 2 \\ 6 & 1 & 1 & 3 & 3 & 3 & 1 & 1 & 3 \\ 7 & 1 & 2 & 3 & 8 & 3 & 2 & 1 & 8 \\ 8 & 1 & 1 & 1 & 7 & 7 & 7 & 7 & 1 \\ \end{array} \\[18pt] \begin{array}{c|cccccccc} & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 \\ \hline \neg & 4 & 5 & 6 & 1 & 2 & 3 & 8 & 7 \\ \end{array}\qquad\qquad\qquad\qquad \end{align*} $$
Inspection of the model reveals that (a) both conditionals satisfy modus ponens and axioms
$\mathbf {LHK}_1$
,
$\mathbf {LHK}_{2}$
, and
$\mathbf {LHK}_{9}$
; but, (b)
$2 \to _1 3 \nvdash 2 \to _2 3$
, since
$2 \to _1 3$
is assigned the designated value 1, but
$2 \to _2 3$
is assigned the non-designated value 3.
Remark Theorem 7 implies that many axiomatic presentations of classical logic — dating all the way back to Frege’s Begriffsschrift [Reference Frege4] — have non-univocal conditionals.
Theorem 8. The conditional is univocal, relative to the implication-disjunction fragment
$\mathbf {LHK}^{\to ,\lor }$
of
$\mathbf {LHK}$
.
Proof Here is a derivation of
$\alpha \to _1 \beta \vdash \alpha \to _2 \beta $
.
We omit the derivations of steps 2, 3, 4, which are theorems of the implication-disjunction fragment
$\mathbf {LHK}^{\to ,\lor }$
of
$\mathbf {LHK}$
. In particular, note that steps 2 and 3 hold by Peirce’s Law. In order to derive steps 7 and 9, we have also made use of the fact that
$\alpha \to \alpha $
is a theorem of
$\mathbf {LHK}^\to $
.
Theorem 9. The conditional is univocal, relative to the implication-conjunction-negation fragment
$\mathbf {LHK}^{\to ,\land ,\neg }$
of
$\mathbf {LHK}$
.
Proof This is a corollary of Theorem 8. Because we are in the implication-conjunction-negation fragment of classical logic, we can now define a disjunction connective (which will satisfy all of the
$\mathbf {LHK}$
disjunction laws, relative to both
$\to _1$
and
$\to _2$
) in terms of negation and conjunction, as
$\alpha \lor \beta =_{df} \neg (\neg \alpha \land \neg \beta )$
. Then, we can apply the same strategy that we used above to demonstrate
$\alpha \to _1 \beta \vdash \alpha \to _2 \beta $
in our proof of Theorem 8.
4 Univocity in classical systems with Sheffer’s stroke
4.1 Univocity in Hilbert systems using Sheffer’s stroke
Nicod [Reference Nicod11] was the first to develop a formal system
$\mathbf {N}$
for classical sentential logic using (only) Sheffer’s stroke (
$\vert $
). He presented a Hilbert system, which uses the following single rule of inference:
(D) From
$\alpha \vert (\beta \vert \gamma )$
and
$\alpha $
, infer
$\gamma $
.
Various sets of axioms have been shown to be complete for classical sentential logic, in the presence of rule (D) [Reference Scharle14]. We will adopt Nicod’s original 23-symbol single axiom, that is,
(N)
$(\alpha \vert (\beta \vert \gamma ))\vert ((\epsilon \vert (\epsilon \vert \epsilon ))\vert ((\delta \vert \beta )\vert ((\alpha \vert \delta )\vert (\alpha \vert \delta ))))$
.
In other words, the system
$\mathbf {N}$
consists of the single rule D and the single axiom N. The question of univocity is a simple one in this context. And, as it happens, we have the following negative result.
Theorem 10. The Sheffer stroke is non-univocal, relative to Nicod’s Hilbert system
$\mathbf {N}$
.
Proof In this case, four-element counter-models are required. Here is one.
$$ \begin{align*} \begin{array}{c|c|c|c|c} \vert_1&1&2&3&4\\ \hline 1&2&1&4&3\\ \hline 2&1&1&1&1\\ \hline 3&4&1&4&1\\ \hline 4&3&1&1&3 \end{array} \hspace{48pt} \begin{array}{c|c|c|c|c} \vert_2&1&2&3&4\\ \hline 1&4&3&2&1\\ \hline 2&3&3&1&1\\ \hline 3&2&1&2&1\\ \hline 4&1&1&1&1 \end{array} \end{align*} $$
Inspection of the model reveals that (a) both strokes satisfy D and N; but, (b)
$1 \vert _1 2 \nvdash 1 \vert _2 2$
, since
$1 \vert _1 2$
is assigned the designated value
$1$
, but
$1 \vert _2 2$
is assigned the non-designated value
$3$
.
4.2 Univocity in Gentzen systems using Sheffer’s stroke
We know of two Gentzen systems for classical sentential logic including Sheffer’s stroke (
$\vert $
). One is due to Read [Reference Read13], and the other is due to Zach [Reference Zach16]. In both systems, the Sheffer stroke is univocal, and this is our final theorem.
Theorem 11. The Sheffer stroke is univocal, relative to both Read’s Gentzen system
$\mathbf {SC}$
, and Zach’s Gentzen system
$\mathbf {NS}$
.
Proof Here is a derivation of
$\alpha \vert _1 \beta \vdash _{\mathbf {SC}} \alpha \vert _2 \beta $
.
And, here is a derivation of
$\alpha \vert _1 \beta \vdash _{\mathbf {NS}} \alpha \vert _2 \beta $
.
Remark. It may seem surprising that the
$\bot $
-rule is not used in our derivation in Zach’s system (of
$\alpha \vert _1 \beta \vdash _{\mathbf {NS}} \alpha \vert _2 \beta $
). But, something completely analogous happens when proving the univocity of negation, relative to Gentzen’s original systems. To wit:
Acknowledgments
Rodolfo C. Ertola-Biraben is grateful to Xavier Caicedo for useful discussions. Both authors are indebted to an anonymous referee of this journal, who provided very detailed and helpful comments on an earlier version of the paper.
