Database Reference
In-Depth Information
carrier
W
of
A
such that the natural mapping
W
→
W/Q
(which maps each ele-
ment
a
∈
W
into its equivalence class
[
a
]∈
W/Q
) is a homomorphism. We will
denote such an algebra as
A
/Q
(W/Q,Σ)
and will call it a
quotient algebra
of
an algebra
A
by the congruence
Q
, such that for each its
k
-ary operation
=
o
i
,wehave
o
i
(
.
Let K be a class of algebras of the same type. We say that K is a
variety
if K is
closed under homomorphic images, subalgebras and products. Each variety can be
seen as a
category
with objects being the algebras and arrows the homomorphisms
between them.
The fundamental Birkhoff's theorem in Universal algebra demonstrates that a
class of algebras forms a variety iff it is equationally definable. For example, the
class of all Heyting algebras (which are definable by the set
E
of nine equations
above), denoted by
[
a
1
]
,...,
[
a
k
]
)
=[
o
i
(a
1
,...,a
k
)
]
HA
=
(Σ
H
,E)
, is a variety. Arend Heyting produced an ax-
iomatic system of propositional logic which was claimed to generate as theorems
precisely those sentences that are valid according to the
intuitionistic
conception
of truth. Its axioms are all axioms of the Classical Propositional Logic (CPL) hav-
ing a set of propositional symbols
p,q,...
∈
PR
and the following axioms (
φ,ψ,ϕ
denote arbitrary propositional formulae):
1.
φ
φ)
;
2.
(φ
∧
ψ)
⇒
(ψ
∧
φ)
;
3.
(φ
⇒
(φ
∧
⇒
⇒
∧
⇒
∧
ψ)
((φ
ϕ)
(ψ
ϕ))
;
4.
((φ
⇒
ψ)
∧
(ψ
⇒
ϕ))
⇒
(φ
⇒
ϕ)
;
5.
ψ
ψ)
;
6.
(φ
∧
(φ
⇒
ψ))
⇒
ψ
;
7.
φ
⇒
(φ
⇒
⇒
(φ
∨
ψ)
;
8.
(φ
∨
ψ)
⇒
(ψ
∨
φ)
;
9.
((φ
⇒
ϕ)
∧
(ψ
⇒
ϕ))
⇒
((φ
∨
ψ)
⇒
ϕ)
;
10.
¬
φ
⇒
(φ
⇒
ψ)
;
11.
((φ
⇒
ψ)
∧
(φ
⇒¬
ψ))
⇒¬
φ
;
12.
φ
φ
;
except for the 12th axiom of “excluded middle”, which, according to construc-
tivist attitude (L.E.J. Brouwer) has to be replaced by “either I have constructively
demonstrated
φ
, or I have constructively demonstrated that
φ
is false”, equivalent
to modal formula
∨¬
is a “necessity” universal modal operator
in S4 modal logic (with transitive and symmetric accessibility relation between the
possible worlds in Kripke semantics, i.e., where this relation is a partial ordering
≤
φ
∨ ¬
φ
, where
¬¬
φ
⇒
φ
is not valid (different from CLP).
According to Brouwer, to say that
φ
is not true means only that I have not at this
time constructed
φ
, which is not the same as saying
φ
is false.
In fact, in Intuitionistic Logic (IL),
φ
). In the same constructivist attitude,
⇒
ψ
is equivalent to
(φ
⇒
c
ψ)
,thatis,to
(
¬
c
φ
∨
ψ)
where '
⇒
c
' is classical logical implication and '
¬
c
' is classical nega-
tion and
¬
c
φ
. Thus, in IL, the conjunction and disjunction are
that of CPL, and only the implication and negation are modal versions of classical
versions of the implication and negation, respectively.
¬
φ
is equivalent to
