JUXTAPOSITION: A NEW WAY TO COMBINE LOGICS
31
the consequence relation ‘ just in case ‘ is strongly unital sound with respect
to B and B contains at least one representative from every isomorphism class of
unital structures for ‘ that has a set of semantic values with cardinality at most
that of the language of ‘.
Proposition 6.34. Suppose ‘
12
is the juxtaposition of ‘
1
and ‘
2
and B
12
is
the juxtaposition of B
1
and B
2
. Suppose at least one of ‘
1
and ‘
2
has theorems.
Then:
1. If B
1
is full for ‘
1
and B
2
is full for ‘
2
, then ‘
12
is strongly determined
with respect to B
12
;
2. If ‘
1
and ‘
2
are each left-extensional, B
1
is unital full for ‘
1
, and B
2
is
unital full for ‘
2
, then ‘
12
is strongly determined with respect to B
12
, a
class of juxtaposed unital structures.
Proof. Since ‘
1
is strongly sound with respect to B
1
and ‘
2
is strongly sound
with respect to B
2
,by Theorem 5.5, ‘
12
is strongly sound with respect to B
12
.
Suppose B
1
is full for ‘
1
and B
2
is full for ‘
2
. By Proposition 6.29, ‘
12
is
strongly determined with respect to B
12
. Using fullness, it is routine to show
that each element of B
12
is isomorphic to an element of B
1
B
2
=B
12
. Therefore,
12
is strongly complete with respect to respect to B
12
.
Suppose B
1
is unital full for ‘
1
and B
2
is unital full for ‘
2
. Since ‘
1
and ‘
2
are each left-extensional, by Proposition 6.29, ‘
12
is strongly determined with
respect to B
12
,a class of juxtaposed unital structures. Using fullness, it is again
routine to show that each element of B
12
is isomorphic to an element of B
12
.
So ‘
12
is strongly complete with respect to respect to B
12
. Since B
12
is the
juxtaposition of two classes of unital structures, it is a class of juxtaposed unital
structures.
6.7. Equivalential Logics. There is an important special case worth dis-
cussing. It concerns logics that contain a set of formulas that behave like a
generalized biconditional.
Let q and r be distinct elements of P . Suppose   Sent(C; fq; rg). For sim-
plicity, if  2 , we write (; ) to stand for the result of uniformly substituting
each occurrence of q in  with  and each occurrence of r in  with . We write
(; ) to stand for the set f(; ) j  2 g. We write ‘ (; ) to abbreviate
the claim that for every  2 , ‘ (; ). We write   ‘ (; ) to abbreviate
the claim that for every  2 ,   ‘ (; ).
We say that  is an equivalence set over C
for ‘ just in case  satises the
following conditions for every ; ;  2 Sent(C; P):
Re exivity. ‘ (; );
Symmetry. (; ) ‘ (; );
Transitivity. (; ) [ (;  ) ‘ (;  );
Modus Ponens. fg [ (; ) ‘ ;
Congruence over C
. For every c
2 C
n
, 
1
;: :: ;
n
; 2 Sent(C; P),
and k 2 f1; : :: ;ng, (k; ) ‘ (c c 1 :: : k :: : n; c c 1 : : :  : : : n).
There is an additional condition worth stating:
Substitution over C
. For every  2 Sent(C; P) and p that strictly C
-
occurs in , f[=p]g [ (; ) ‘ [=p].
Pdf to multi page tiff - control software system:C# PDF Convert to Tiff SDK: Convert PDF to tiff images in C#.net, ASP.NET MVC, Ajax, WinForms, WPF
Online C# Tutorial for How to Convert PDF File to Tiff Image File
www.rasteredge.com
Pdf to multi page tiff - control software system:VB.NET PDF Convert to Tiff SDK: Convert PDF to tiff images in vb.net, ASP.NET MVC, Ajax, WinForms, WPF
Free VB.NET Guide to Render and Convert PDF Document to TIFF
www.rasteredge.com
32
JOSHUA B. SCHECHTER
Proposition 6.35. Suppose  satises Re exivity and Congruence over
C
. Then  satises Substitution over C
just in case  satises Modus Po-
nens.
Proof. Suppose  satises Modus Ponens. Suppose  2 Sent(C; P) and p
strictly C
-occurs in . Using Re exivity and Congruence over C
,by induction
on the complexity of , (; ) ‘ ([=p]; [=p]). By Modus Ponens and Cut,
f[=p]g [ (;) ‘ [=p].
Now suppose  satises Substitution over C C . So fp[=p]g[(; ) ‘ p[=p].
That is, fg [ (; ) ‘ .
We say that  is a regular equivalence set over C
for ‘ just in case  is an
equivalence set over C
for ‘ that satises the following additional condition:
Regularity. f; g ‘ (; ).
We say that  is an equivalence set for ‘ just in case  is an equivalence set
over C for ‘. We say that  is a regular equivalence set for ‘ just in case 
is a regular equivalence set over C for ‘. In many familiar logics { including
classical and intuitionist logic { the sets fq $ rg and fq ! r;r ! qg are regular
equivalence sets.
We say that ‘ is equivalential over C
if there is an equivalence set over C
for
‘. Wesay that ‘ is regularly equivalential over C
if there is a regular equivalence
set over C
for ‘. We say that ‘ is equivalential (simpliciter) just in case ‘ is
equivalential over C. We say that ‘ is regularly equivalential (simpliciter) just
in case ‘ is regularly equivalential over C.
45
It is straightforward to show that if ‘ is regularly equivalential over C C , then
‘is C C -left-extensional (and is therefore left-extensional over Sent(C C ; P)).
Proposition 6.36. If ‘ is regularly equivalential over C C , then ‘ is C C -
left-extensional.
Proof. Suppose  is a regular equivalence set over C  for ‘. Suppose
2 Sent(C; P) and p strictly C C -occurs in . By Proposition 6.35, f[=p]g [
(; ) ‘ [=p]. By Regularity, f; g ‘ (;). By Cut, f; ; [=p]g ‘
[=p]. Therefore, ‘ is C
-left-extensional.
Equivalence sets over C
provide simple ways to construct equivalence re-
lations suitable for C
, ‘, and  . Suppose   Sent(C;P ) is an equivalence
set over C
for ‘. Suppose    Sent(C; P). We dene a binary relation on
Sent(C; P) as follows:
h; i 2 
just in case   ‘ (; ):
We write    (mod 
)to stand for the claim that h; i 2 
.
Lemma 6.37. Suppose  is an equivalence set over C
for ‘. Then for
every    Sent(C; P), 
is an equivalence relation on Sent(C; P ) suitable for
C
,‘, and  .
45Thenotion of an equivalentiallogic(simpliciter)isoriginallyduetoPrucnal &Wronski
(1974). See Czelakowski (1981) for discussion.
control software system:C# TIFF: C# Code for Multi-page TIFF Processing Using RasterEdge .
com aims at developing professional multi-page Tiff processing SDK adding & deleting Tiff file page, merging and commonly used file formats, like PDF, Bmp, Jpeg
www.rasteredge.com
control software system:VB.NET Image: Multi-page TIFF Editor SDK; Process TIFF in VB.NET
VB.NET Imaging - Multi-page TIFF Processing in VB. VB.NET TIFF Editor SDK to Process Multi-page TIFF Document Image. Visual C#. VB.NET.
www.rasteredge.com
JUXTAPOSITION: A NEW WAY TO COMBINE LOGICS
33
Proof. Suppose    Sent(C; P). By Re exivity, Symmetry, Transitivity,
Weakening, and Cut, 
is an equivalence relation on Sent(C; P ).
Congruence over C
: Suppose c
2C
n
; 
1
;: : : ; 
n
; 2 Sent(C; P ); and
k 2 f1; : : : ng. Suppose k   (mod   ). So   ‘ (k; ). Since  sat-
ises Congruence over C C , (k; ) ‘ (c c 1 : : :k : : : n; c c 1 : ::  : : :n).
By Cut,   ‘ (c c 1 : : : k : : : n; c c 1 : : :  : : : n). Hence, c c 1 : : : k : : : n 
c
1
:: :  : : : 
n
(mod 
).
Compatibility with   and ‘: Suppose    (mod 
). So   ‘ (; ).
Suppose   ‘ . By Modus Ponens, fg [(;) ‘ . By Cut,   ‘ . Similarly,
if   ‘ , then   ‘ . So   ‘  just in case   ‘ .
Lemma 6.38. Suppose  is an equivalence set over C
for ‘. Then 
is a regular equivalence set over C
for ‘ just in case for every non-empty
 Sent(C; P) consistent with ‘, 
is unital suitable for C
,‘, and  .
Proof. Suppose  is a regular equivalence set over C  for ‘. Suppose   
Sent(C; P). Suppose   ‘  and   ‘ . By Regularity, f; g ‘ (; ). By
Cut,   ‘ (; ). So    (mod 
). Therefore, 
is unital suitable for C
,
‘, and  .
Now suppose for every non-empty    Sent(C; P) consistent with ‘, 
is
unital suitable for C
, ‘, and  . Suppose ;  2 Sent(C; P ). If f; g is
inconsistent with respect to ‘, f; g ‘ (; ). Suppose, then, that f; g is
consistent with respect to ‘. So f;g is unital suitable for C C , ‘, and f; g.
By Identity and Weakening, f; g ‘  and f; g ‘ . By strong compatibility
with ‘ and f; g,    (mod 
f;g
). So, again, f; g ‘ (; ). Therefore,
is a regular equivalence set over C
for ‘.
Suppose 
1
is an equivalence set over C
1
for ‘
12
and 
2
is an equivalence
set over C
2
for ‘
12
.Let B
h
1
;
2
i
12
be the Lindenbaum-Tarski class of juxtaposed
structures for C
1
,C
2
, and ‘
12
built using the 
i
relations. Any consequence
relation that is equivalential over some signature has theorems. Combining this
fact with Lemmas 6.37 and 6.38 and Theorem 6.7, we arrive at the following
result:
Proposition 6.39. Suppose 
1
is an equivalence set over C
1
for ‘
12
and
2
is an equivalence set over C
2
for ‘
12
. Then:
1. ‘
12
is strongly complete with respect to B
h
1
;
2
i
12
;
2. If ‘
12
is the juxtaposition of ‘
1
and ‘
2
, then ‘
12
is strongly sound with
respect to B
h
1
;
2
i
12
;
3. If ‘
12
is consistent, then there is a coherent non-trivial model based on
B
h
1
;
2
i
12
;
4. B
h
1
;
2
i
12
is a class of juxtaposed unital structures just in case 
1
is a regular
equivalence set over C
1
for ‘
12
and 
2
is a regular equivalence set over C
2
for ‘
12
.
There is a particularly well-behaved kind of equivalence set over C
. We say
that  is an internal equivalence set over C
for ‘ just in case  is an equivalence
set over C
for ‘ and   Sent(C
;fq; rg). We say that  is an regular internal
equivalence set if, in addition,  satises the Regularity condition. We say that
control software system:.NET Multipage TIFF SDK| Process Multipage TIFF Files
on Windows Forms applications, upload to SharePoint and save to PDF documents View, edit, insert, delete and mark up pages in multi-page TIFF files; Annotate and
www.rasteredge.com
control software system:C# TIFF: How to Delete Page(s) from Multi-page TIFF File Using
VB.NET How-to, VB.NET PDF, VB.NET Word, VB.NET Excel, VB.NET RasterEdge.com offers an advanced multi-page Tiff editing utility, XDoc.Tiff for .NET, which allows
www.rasteredge.com
34
JOSHUA B. SCHECHTER
‘is internally equivalential over C
if there is an internal equivalence set over
C
for ‘. We say that ‘ is regularly internally equivalential over C
if there is
aregular internal equivalence set over C
for ‘. Notice that ‘ is equivalential
(simpliciter) just in case ‘ is internally equivalential over C. ‘ is regularly
equivalential (simpliciter) just in case ‘ is regularly internally equivalential over
C.
We rst put forward two alternative ways to characterize internal equivalence
sets over C
.
Proposition 6.40. Suppose   Sent(C
;fq; rg).  is an internal equiv-
alence set over C
for ‘ just in case  satises Re exivity, Modus Ponens, and
Congruence over C
.
Proof. Suppose  satises Re exivity, Modus Ponens, and Congruence over
C
. Suppose  2 .
Symmetry: Since  is an internal equivalence set over C
for ‘, p strictly C
-
occurs in (p;). So by Proposition 6.35, f(p; )[=p]g[(; ) ‘ (p; )[=p].
That is, f(; )g [ (; ) ‘ (; ). By Re exivity, ‘ (; ). By Cut,
(; ) ‘ (; ).
Transitivity: Since  is an internal equivalence set over C
for ‘, p strictly
C
-occurs in (; p). By Proposition 6.35, f(; p)[=p]g[(;  ) ‘ (; p)[ =p].
That is, (; ) [(;  ) ‘ (;  )).
Proposition 6.41. Suppose   Sent(C C ; fq; rg).  is an internal equiva-
lence set over C  for ‘ just in case  satises Re exivity and Substitution over
C
.
Proof. Suppose  is an internal equivalence set over C
for ‘.  satises
Re exivity. By Proposition 6.35,  satises Substitution over C
.
Now suppose  satises Re exivity and Substitution over C
. Suppose c
2
C
n
;
1
;: : : ; 
n
; 2 Sent(C; P); p is an element of P that does not occur in
1
;: : : ; 
n
; and k 2 f1; :: : ; ng. Suppose  2 . Since  2 Sent(C
;fq; rg),
pstrictly C
-occurs in (c
1
:: : 
k
:: : 
n
;c
1
:: : p : : : 
n
). By Substitution
over C C , Re exivity, and Cut, (k; ) ‘ (c c 1 : : :k : : : n; c c 1 : ::  : : :n).
So  satises Congruence over C C . By Proposition 6.35,  satises Modus
Ponens. By Proposition 6.40,  satises Symmetry and Transitivity. Therefore,
is an internal equivalence set over C
for ‘.
We next show that any two internal equivalence sets over C
for ‘ are inter-
derivable:
Proposition 6.42. Suppose  and 
0
are both internal equivalence sets
over C
for ‘. Then (;) ‘ 
0
(; ).
Proof. Suppose 
0
2
0
.Since 
0
is an internal equivalence set over C
for ‘,
pstrictly C
-occurs in 
0
(; p). By Proposition 6.35, f
0
(; p)[=p]g [(; ) ‘
0(; p)[=p]. That is, f0(; )g [(; ) ‘ 0(; ). By Re exivity, ‘ 0(; ).
By Cut, (; ) ‘ 0(; ).
It follows from this result that if  and 
0
are both internal equivalence sets
over C
for ‘, then 
= 
. (It also follows that if  is regular, so is 
0
.
control software system:VB.NET TIFF: VB.NET Sample Code to Process & Manage TIFF Page
TIFF pages into a new multi-page TIFF document file VB.NET programming, this TIFF page processing control add & profession imaging controls, PDF document, image
www.rasteredge.com
control software system:Process Multipage TIFF Images in Web Image Viewer| Online
images into one; Swap two pages' position in multi-page TIFF images; Convert multi-page TIFF image into scannable PDF; Convert TIFF to
www.rasteredge.com
JUXTAPOSITION: A NEW WAY TO COMBINE LOGICS
35
Indeed, it is straightforward to show that if ‘ is internally equivalential and
regularly equivalential, then every internal equivalence relation is regular.)
Suppose ‘ is internally equivalential over C
. Let 
C
stand for the unique
equivalence relation dened on Sent(C; P ) generated by any of the internal equiv-
alence sets over C  for ‘. We can show that 
C
=
C
=
C
is the most
coarse-grained equivalence relation on Sent(C; P) suitable for C
,‘, and  .
Lemma 6.43.
1. If  is an equivalence set over C
for ‘, then  is an equivalence set over
C
for any consequence relation that extends ‘;
2. If  is a regular equivalence set over C
for ‘, then  is a regular equiva-
lence set over C
for any consequence relation that extends ‘.
Proof. Suppose C is a sub-signature of C+ and P is a subset of P+. Suppose
+
is a consequence relation for Sent(C
+
;P
+
)that extends ‘. Suppose p, q, and
rare distinct elements of P . Suppose ; ;   2 Sent(C
+
;P
+
).
Re exivity: ‘ (p; p). So ‘
+
(p;p). By Uniform Substitution, ‘
+
(; ).
Symmetry: (p; q) ‘ (q; p). So (p; q) ‘
+
(q; p). By Uniform Substitution,
(; ) ‘
+
(; ).
Transitivity: (p; q) [ (q; r) ‘ (p; r). So (p; q) [ (q; r) ‘
+
(p; r). By
Uniform Substitution, (; ) [ (;  ) ‘
+
(;  ).
Modus Ponens: fpg [ (p; q) ‘ q. So fpg [ (p; q) ‘
+
q. By Uniform Substi-
tution, fg [ (; ) ‘
+
.
Congruence over C
: Let c
2 C
n
. Let p
1
;: : : p
n
;q be distinct elements
of P. Let 
1
;: : : ; 
n
; 2 Sent(C
+
;P
+
) and k 2 f1;: : : ; ng. (p
k
;q) ‘
(c
p
1
:: : p
k
:: : p
n
, c
p
1
:: : q: : : p
n
).
So (p
k
;q) ‘
+
(c
p
1
::: p
k
:: :p
n
;
c
p
1
:: : q : : :p
n
). By Uniform Substitution, (
k
;) ‘
+
(c
1
:: : 
k
:: : 
n
;
c
1
:: :  : : : 
n
).
Regularity: By Regularity, fp; qg ‘ (p; q). So fp; qg ‘+ (p; q). By Uniform
Substitution, f; g ‘ (; ).
Proposition 6.44. Suppose ‘ is internally equivalential over C
. Suppose
 Sent(C; P). Then 
C
=
C
=
C
is the most coarse-grained equiva-
lence relation over Sent(C;P ) suitable for C
,‘, and  .
Proof. Suppose  is an internal equivalence set over C
for ‘.
We rst show that    (mod 
C
)just in case    (mod 
C
).
Suppose    (mod 
C
). By Proposition 6.11,    (mod 
C
).
Now suppose    (mod 
C
). Suppose  2 . Let p be an element of P
that does not occur in . Since  is an internal equivalence set over C
for ‘, p
strictly C
-occurs in (;p). So   ‘ (; p)[=p] just in case   ‘ (; p)[=p].
That is,   ‘ (; ) just in case   ‘ (; ). By Re exivity and Weakening,
‘ (; ). So   ‘ (; ). Therefore,    (mod 
C
).
We next show that    (mod 
C
)just in case    (mod 
C
).
Suppose    (mod 
C
). So   ‘ (; ). Suppose  2 Sent(C C ; P [ P)
and p occurs in . By Lemma 6.43,  is an equivalence set over C
for ‘
. By
Proposition 6.35, f[=p]g[(; ) ‘
[=p]. Since ‘
extends ‘,   ‘
(; ).
By Cut,   [ f[=p]g ‘
[=p]. Moreover, by Symmetry,   ‘
(;). So by
analogous reasoning,   [ f[=p]g ‘
[=p]. Therefore,    (mod 
C
).
control software system:Online Convert PDF file to Tiff. Best free online PDF Tif
C# developers can render and convert PDF document to TIFF image file with no loss in original file quality. Both single page and multi-page Tiff image files
www.rasteredge.com
control software system:C# PDF File & Page Process Library SDK for C#.net, ASP.NET, MVC
VB.NET Word, VB.NET Excel, VB.NET PowerPoint, VB.NET Tiff, VB.NET Easily manipulate multi-page PDF document file with page inserting, deleting and re-ordering
www.rasteredge.com
36
JOSHUA B. SCHECHTER
Now suppose    (mod 
C
). Suppose  2  and p 2 P
. Since  is
an internal equivalence set over C
for ‘,   [ (p; ) ‘
(p;). By Uniform
Substitution,   [ (;) ‘
(; ). By Lemma 6.17,   [ (; ) ‘ (; ). By
Re exivity, ‘ (; ). By Cut,   ‘ (;). Therefore,    (mod 
C
).
By Proposition 6.11, 
C
is the most coarse-grained equivalence relation on
Sent(C; P) suitable for C
,‘, and  .
Suppose ‘
12
is internally equivalential over C
1
and over C
2
. Let B
12
be the
Lindenbaum-Tarski class of juxtaposed structures for C
1
, C
2
, and ‘
12
, built
using the 
C
i
relations.
Proposition 6.45. Suppose ‘
12
is internally equivalential over C
1
and over
C
2
. Then:
1. B
12
=B
12
=B
12
;
2. B
12
is a class of juxtaposed unital structures just in case ‘
12
is regularly in-
ternally equivalential over C
1
and over C
2
just in case ‘
12
is left-extensional
over Sent(C
1
;P
1
)and over Sent(C
2
;P
2
).
Proof. Claim 1 follows from Proposition 6.44 Claim 2 follows from Proposi-
tion 6.44 and Lemmas 6.14 and 6.21.
Since B
12
=B
12
= B
12
, it is natural to think of this class as the canonical
Lindenbaum-Tarski class of juxtaposed structures for C
1
,C
2
,and ‘
12
.
Suppose each of ‘
1
and ‘
2
is equivalential. When is ‘
12
hC
1
;C
2
i-strongly
determined or hC
1
;C
2
i-strongly unital determined? Our results provide a fairly
comprehensive answer to this question.
Proposition 6.46. Suppose ‘
12
is a juxtaposed consequence relation over
1
and ‘
2
. Suppose each of ‘
1
and ‘
2
is equivalential. Then:
1. ‘
12
is strongly complete with respect to B
12
;
2. If ‘
12
is the juxtaposition of ‘
1
and ‘
2
, then ‘
12
is strongly sound with
respect to B
12
;
3. If ‘
12
is consistent, then there is a coherent non-trivial model based on B
12
;
4. If each of ‘
1
and ‘
2
is regularly equivalential then B
12
is a class of juxta-
posed unital structures.
Proof. By Lemma 6.43, if ‘
i
is equivalential, then ‘
12
is internally equiv-
alential over C
i
. By Proposition 6.42, B
12
is well-dened. Claims 1{4 then follow
by Proposition 6.39.
Proposition 6.47. Suppose C
1
and C
2
are disjoint. Suppose ‘
12
is a jux-
taposed consequence relation over ‘
1
and ‘
2
. Suppose each of ‘
1
and ‘
2
is
consistent and equivalential. Then:
1. ‘
12
is strongly complete with respect to B
12
;
2. If ‘
12
is the juxtaposition of ‘
1
and ‘
2
, then ‘
12
is strongly sound with
respect to B
12
;
3. There is a coherent non-trivial model based on B
12
;
4. B
12
is a class of juxtaposed unital structures just in case each of ‘
1
and ‘
2
is regularly equivalential.
control software system:C# PDF Page Rotate Library: rotate PDF page permanently in C#.net
Using this C# .NET PDF rotate page control SDK, you can easily select any page from a multi-page PDF document file, rotate selected PDF page to special
www.rasteredge.com
JUXTAPOSITION: A NEW WAY TO COMBINE LOGICS
37
Proof. If ‘
1
and ‘
2
are consistent, then by Theorem 5.10, ‘
12
is consistent.
Claims 1{3 then follow from Proposition 6.46. Claim 4 follows from Proposition
6.39 and Theorem 5.11.
x7. Classical and Intuitionist Logics. In this section, we make use of our
general results about juxtaposition to investigate cases of particular interest {
juxtapositions of classical and intuitionist logics.
Let P
1
=P
2
=P
12
be the countably innite set fp
1
;p
2
;:: : g. For i = 1 and 2,
let the signature C
i
contain the following sets of connectives:
 C
1
i
=f:
i
g.
 C
2
i
=f^
i
;_
i
;!
i
;$
i
g.
C
12
thus contains two copies of each of the standard propositional connectives.
We say that a consequence relation, ‘
12
,for Sent(C
12
;P
12
) collapses just in
case for every ; 
0
2Sent(C
12
;P
12
)exactly alike except perhaps for some or all
of their subscripts, fg ‘
12
0
.
46
Let ‘
c
1
be the classical consequence relation for Sent(C
1
;P
1
). Let ‘
i
1
be the
intuitionist consequence relation for Sent(C
1
;P
1
). Let ‘
c
2
and ‘
i
2
be dened
similarly.
Let ‘
cc
be the juxtaposition of ‘
c
1
and ‘
c
2
. We call this the \bi-classical"
consequence relation for Sent(C
12
;P
12
). Let ‘
ii
be the juxtaposition of ‘
i
1
and
i
2
. We call this the \bi-intuitionist" consequence relation for Sent(C
12
;P
12
).
Finally, let ‘
ic
be the juxtaposition of ‘
i
1
and ‘
c
2
. We call this the \intuitionist-
classical" consequence relation for Sent(C
12
;P
12
).
7.1. Applying the Results. Let us rst consider the case of bi-classical
logic, the juxtaposition of two classical consequence relations. Applying the
results above, we can derive several properties of ‘
cc
.
Given any non-trivial Boolean algebra, hB; i, there is a corresponding unital
structure hB; f1g; i where B is the same set of semantic values, 1 is the greatest
element of the Boolean algebra, and for every a;b 2 B:
(:)(a) =  a;
(^)(a; b) = a u b;
(_)(a; b) = a t b;
(!)(a; b) =  a t b;
($)(a; b) = ( a t b) u( b ta):
Here,  , u, and t are the complement, inmum, and supremum relations on the
Boolean algebra, respectively.
Let us call such structures \Boolean structures". Given a Boolean structure,
the partial order of the corresponding Boolean algebra can be recovered: a  b
just in case (!)(a; b) = 1.
46Intheliteratureonbring, the term
\collapse" is typically used for the property called
\weak collapse" in section 7.4 below.
38
JOSHUA B. SCHECHTER
The classical consequence relation is strongly determined with respect to the
class of Boolean structures.
47
It is consistent, has theorems, and is left-extensional.
By Theorem 5.10, ‘
cc
is consistent. By Theorem 5.11, ‘
cc
is strongly conserva-
tive over ‘c
1
and ‘c
2
.It can be axiomatized using two copies of any Hilbert-style
axiomatization for classical logic. (It can also be axiomatized using two copies
of any natural deduction-style axiomatization for classical logic restricted so
that the rules for one stock of connectives cannot be applied within any sub-
derivation used in the application of a meta-rule governing a connective from
the other stock.) By Corollary 6.32, ‘
cc
is hC
1
;C
2
i-strongly unital determined.
We can extract additional information about ‘
cc
using Proposition 6.34. The
class of all Boolean structures is unital full for the classical consequence relation.
We say that a juxtaposed unital structure hB
1
;B
2
iis a bi-Boolean structure just
in case both B
1
and B
2
are Boolean structures. By Proposition 6.34, ‘
cc
is
strongly determined with respect to the class of all bi-Boolean structures.
The case of the bi-intuitionist consequence relation, ‘
ii
is analogous. Given
any non-trivial Heyting algebra, hB; i, there is a corresponding unital structure
hB; f1g; i where B is the same set of semantic values, 1 is the greatest element
of the Heyting algebra, and for every a;b 2 B:
(:)(a) = a ) 0;
(^)(a; b) = a ub;
(_)(a; b) = a tb;
(!)(a;b) = a ) b;
($)(a;b) = (a ) b) u(b ) a):
Here, u, t, and ), are the inmum, supremum, and implication relations on
the Heyting algebra, and 0 is its least element.
Let us call such structures \Heyting structures". Given a Heyting structure,
the partial order of the corresponding Heyting algebra can be recovered: a  b
just in case (!)(a; b) = 1.
The intuitionist consequence relation is strongly determined with respect to
the class of Heyting structures.48 It is consistent, has theorems, and is left-
extensional. By Theorem 5.10, ‘ii is consistent. By Theorem 5.11, ‘ii is strongly
conservative over ‘
i
1
and ‘
i
2
. It can be axiomatized using two copies of any
Hilbert-style axiomatization for intuitionist logic. (It can also be axiomatized
using two copies of any natural deduction-style axiomatization for intuitionist
logic restricted so that the rules for one stock of connectives cannot be applied
within any sub-derivation used in the application of a meta-rule governing a
connective from the other stock.) By Corollary 6.32, ‘
ii
is hC
1
;C
2
i-strongly
unital determined.
47
The classical consequence relation is also strongly determined with respect to the class of
structures dened as above except that the set of designated values is allowed to be any proper
lter on the Boolean algebra.
48
The intuitionist consequence relation is also strongly determined with respect to the class
of structures dened as above except that the set of designated values is allowed to be any
proper lter on the Heyting algebra.
JUXTAPOSITION: A NEW WAY TO COMBINE LOGICS
39
The class of all Heyting structures is unital full for the intuitionist consequence
relation. We say that a juxtaposed unital structure hB
1
;B
2
iis a bi-Heyting struc-
ture just in case both B
1
and B
2
are Heyting structures. By Proposition 6.34,
ii is strongly determined with respect to the class of all bi-Heyting structures.
Finally, consider the intuitionist-classical consequence relation, ‘ic. By The-
orem 5.10, ‘ic is consistent. By Theorem 5.11, ‘ic is strongly conservative over
i
1
and ‘
c
2
. It can be axiomatized by combining a Hilbert-style axiomatization
for classical logic and a Hilbert-style axiomatization for intuitionist logic. (It can
also be axiomatized using a copy of any natural deduction-style axiomatization
for intuitionist logic and a copy of any natural deduction-style axiomatization
for classical logic, each restricted so that the rules for one stock of connectives
cannot be applied within any sub-derivation used in the application of a meta-
rule governing a connective from the other stock.) By Corollary 6.32, ‘
ic
is
hC
1
;C
2
i-strongly unital determined.
We say that a juxtaposed unital structure hB
1
;B
2
iis a Heyting-Boolean struc-
ture just in case B
1
is a Heyting structure and B
2
is a Boolean structure. Again
using Proposition 6.34, ‘
ic
is strongly determined with respect to the class of all
Heyting-Boolean structures.
7.2. Non-Collapse Results. These results already have implications for the
collapse of classical and intuitionist logics. Consider the case of ‘
ic
. We have
shown that this consequence relation is strongly conservative over ‘
i
1
and ‘
c
2
.
This suces to show that ‘
ic
does not collapse.
49
Since p _ :p is a theorem of
classical logic but not a theorem of intuitionist logic, 0
ic
p_
1
:
1
pand ‘
ic
p_
2
:
2
p.
Similarly, Peirce’s law, ((p ! q) ! p) ! p, can be used to show that !
1
and !
2
are not intersubstitutable. Double Negation Elimination can be used to show
that :
1
and :
2
are not intersubstitutable, either.
The interest of these results should not be underemphasized. Juxtaposition
is a natural way to combine classical and intuitionist logic. ‘
ic
has all of the
entailments of intuitionist logic (for the 1-connectives) and all of the entailments
of classical logic (for the 2-connectives). Indeed, it is a strong conservative
extension of both intuitionist and classical logic. It obeys the usual structural
rules, and is substitution invariant. Yet, the classical and intuitionist connectives
are not intersubstitutable. There is no collapse.
Notice that the non-collapse result also applies to ‘
ii
.This is a strictly weaker
relation than ‘
ic
. Thus, if corresponding connectives are not intersubstitutable
in ‘
ic
,they are not intersubstitutable in ‘
ii
,either.
What about bi-classical logic? Does this logic avoid collapse? The answer is
yes, but proving this takes a bit more work. In particular, to show that ‘
cc
does
not collapse, we make use of Lemma 5.1 to build a coherent bi-Boolean model.
ABoolean model can be specied by specifying a Boolean algebra and a valu-
ation. Boolean algebras can be visually represented using Hasse diagrams. Such
adiagram contains nodes { each representing a distinct element of the carrier
set of the algebra { and line segments connecting pairs of nodes. Given two
elements of the carrier set, a and b, a  b just in case there is a path from a to
49
This can also be proved using the technique of cryptobring. See Caleiro & Ramos (2007).
40
JOSHUA B. SCHECHTER
bmonotonically increasing in height. For example, here are the Hasse diagrams
for two Boolean algebras:
1
2
1
1
0
1
1
2
e
f
0
2
Let B
1
be the Boolean structure corresponding to the rst of these Boolean
algebras. Let B
2
be the Boolean structure corresponding to the second Boolean
algebra. Let V
1
(p
1
) = V
1
(p
2
) = V
1
(p
3
) = 0
1
. Let V
2
(p
1
) = V
2
(p
2
) = e and
V
2
(p
3
) = f. Let V
i
(p) = 1
i
for every other p 2 P
12
. Let M
1
= hB
1
;V
1
i and
M
2
= hB
2
;V
2
i. M
1
and M
2
designate the very same sentence symbols. By
Lemma 5.1, there is a coherent juxtaposition of M
1
and M
2
. We can single
out a specic coherent juxtaposition of these models by specifying which non-
designated elements to use in the construction relied upon in the proof of that
lemma. (Since B
1
and B
2
are unital, there is no choice about which designated
elements to use in the construction.) In particular, let a
1
= 0
1
and a
2
= 0
2
.
Let M
12
be the coherent bi-Boolean model that results from this choice in the
construction.
Using this juxtaposed model, we can prove the non-collapse result. Indeed,
we can prove the stronger result that no two corresponding connectives in C
12
are intersubstitutable according to ‘cc:
Proposition 7.1. In ‘
cc
, no pair of corresponding connectives are inter-
substitutable. In particular:
 f:
1
pg 0
cc
:
2
p;
 fp _
1
qg 0
cc
p_
2
q;
 fp !
1
qg 0
cc
p!
2
q;
 fp $
1
qg 0
cc
p$
2
q;
 f:
2
(p ^
1
q)g 0
cc
:
2
(p ^
2
q).
Therefore, ‘
cc
does not collapse.
Proof. Since ‘cc is strongly sound with respect to the class of bi-Boolean
structures, all we have to do is to nd a coherent bi-Boolean countermodel to
each putative entailment claim. We make use of the model M
12
,
In M
12
,k:
1
p
1
k
1
=1
1
and k:
2
p
1
k
2
=f. So f:
1
p
1
g0
cc
:
2
p
1
. kp
1
_
2
p
3
k
2
=1
2
and kp
1
_
1
p
3
k
1
=0
1
. So fp
1
_
2
p
3
g0
cc
p
1
_
1
p
3
. By symmetry, fp
1
_
1
p
3
g0
cc
p1 _
2
p3. kp1 !
1
p3k
1
=1
1
and kp1 !
2
p3k
2
=f. So fp1 !
1
p3g 0cc p1 !
2
p3.
kp
1
$
1
p
3
k
1
=1
1
. kp
1
$
2
p
3
k
2
=0
2
. So fp
1
$
1
p
3
g0
cc
p
1
$
2
p
3
.
The trickiest case is the nal one, since it involves an embedded connective.
This is what requires us to specify a particular coherent juxtaposition of M
1
and
M
2
.In M
12
,k:
2
(p1 ^
1
p2)k
2
2
kp1 ^
1
p2k
2
2
0
2
=1
2
. k:
2
(p1 ^
2
p2)k
2
=
f. So f:
2
(p1 ^
1
p3)g 0cc :
2
(p1 ^
2
p3).
Since ‘
ii
and ‘
ic
are weaker than ‘
cc
, the result applies to these logics, as
well.
Documents you may be interested
Documents you may be interested