Information Technology Reference
InDepth Information
7.9
Countably Infinite Indeterminacy
Let
ω
be the axiom:
(
∇x
∇
x
˙
)
∧∃y.∇y
No ambiguity is possible with respect to the use of
ω
for the set of natural
numbers, and the motivation is that the axiom
ω
introduces a countably infinite
type in
. The first part says that once indeterminate always indeterminate.
The second part of the axiom
∇
ω
says that indeterminacy exists. In other words,
we can say that
ω
yields
∇

confinement
and
∇

existence
.
∇
ω
(propositional
higher order logic with countably infinite indeterminacy) such that all theorems
of ordinary mathematics can be proved (the axioms can be shown consistent in
axiomatic set theory [16], which is the standard foundation of mathematics and
stronger than
With the axiom
ω
we extend
∇
to the indeterminacy theory
∇
ω
, cf. the second Godel incompleteness theorem).
Although the propositional higher order logic
∇
is our starting point, the
indeterminacy theory
∇
ω
is going to be our most important formal system and
we use IT =
{ϕ  ω ϕ}
as a shorthand for its theorems and
Θ
Γ
instead of
Θ, ω Γ
. In particular we previously could have used
θ
0
,θ
1
,θ
2
,θ
3
ϕ
in the
case study.
We allow a few more abbreviations:
ϕ ≡ ϕ ∧¬ϕ
ˆ
ϕ ≡ ϕ ∨¬ϕ
ˇ
We can now state the interesting property of
∇
ω
(coming from
∇
) succinctly:
ϕ
ˆ
ϕ
ˇ
7.10
Classical Logic
Let ∆ be the axiom:
x
∆
The ∆ axiom is equivalent to
∇

nonexistence
,namely
x. ∇x
, and with the
∇
∇
∆
which
axiom ∆ we extend
to the classical propositional higher order logic
was thoroughly investigated in [14, 2].
Finally we can combine the extensions
∇
ι
into the classical higher
∇
∆
and
∇
∆
,alsoknownasQ
0
basedonthetyped
order logic
calculus, and often seen
as a restriction of the transfinite type theory Q [3, 21] by removing the transfinite
types. Q
0
is implemented in several automated theorem provers with many active
users [18, 5, 9, 23]. Classical second order logic, first order logic, elementary logic
(first order logic without functions and equality) and propositional logic can be
seen as restrictions of Q
0
.
In contrast to the paraconsistent
λ
∇
∆
is not a foundation of
mathematics, but we obtain the type theory Q
0
by replacing the sort
∇
ω
the classical
ι
with the
sort
σ
and adding the relevant Peano postulates ˙
x
=0
∧
(
x
=
y
x
˙
=˙
y
)in
our notation, cf. [4, pp. 209/217] for the details.
Search WWH ::
Custom Search