Information Technology Reference
In-Depth Information
A
,
∧
,
∨
,
1
,
0
1.
is a complete distributive lattice,
2.
x
∧
y
≤
z
implies
x
≤
y
⃒
z
,
3.
x
≤
y
implies
z
⃒
x
≤
z
⃒
y
,and
4.
x
≤
y
implies
y
⃒
z
≤
x
⃒
z
.
A reasonable implication algebra is called
deductive
if
(
x
∧
y
)
⃒
z
=
x
⃒
(
y
⃒
z
)
.
is any first-order language then by NFF (the
negation-free fragment
)we
mean the closure of the atomic formulas of
L
If
L
∧
∨
→
∃
∀
under
,
,
,
,and
.The
elements of NFF will be called
negation-free formulas
.
For the axiom schemes in the axiom system for ZF (i.e., Separation and Re-
placement), we write NFF-Separation and NFF-Replacement for the subscheme
where we only allow instances of negation-free formulas in the scheme.
One of the main results in [5] is the following.
Theorem 1.
Let
be a deductive reasonable implication
algebra. Then
Extensionality
,
Pairing
,
Infinity
,
Union
and
Powerset
and the
schemes
NFF
-
Separation
and
NFF
-
Replacement
are valid in
V
(
A
)
.
A
=
A
,
∧
,
∨
,
⃒
,
1
,
0
If
A
is a deductive reasonable implication algebra and
L
A
is a logic that is
sound and complete with respect to
L
A
plays the role of the propositional
fragment of the logic of the set theoretic model
V
(
A
)
.
Below, we shall give an example PS
3
of a deductive reasonable implication
algebra which is neither a Heyting nor a Boolean algebra. Its logic is a
paracon-
sistent logic
1
which then gives rise to a model of
paraconsistent set theory
.
The three-valued matrix
PS
3
=
{
1
,
1
/
2
,
0
},∧,∨,⃒
is a deductive reasonable
implication algebra, where the truth tables for the operators are given below:
A
,then
∧
1
1
/
2
0
1
1
/
2
0
1 11 1
1
/
2
1
1
/
2
∨
1
1
/
2
0
1 110
1
/
2
110
0
⃒
1
1
1
/
2
0
1
/
2
1
/
2
1
/
2
0
1
/
2
0
000
0
1
1
/
2
0
111
Let us now introduce a unary operator
∗
in
PS
3
having the following truth table:
∗
1 0
1
/
2
1
/
2
0
1
PS
3
,
∗
We use the symbol PS
3
to refer to the augmented structure
. The des-
ignated set is
. The logic which is sound and complete with respect to
PS
3
is a paraconsistent logic [9] and we observed in [5] that
V
(PS
3
)
is a model
of paraconsistent set theory. In [2] and [3] the same truth tables have appeared
{
1
,
1
/
2
}
1
A logic is called paraconsistent if there exist formulas
˕
and
ˈ
such that
{˕, ¬˕}
ˈ
.
Semantically, the premises get the designated values but the conclusion does not.
