Information Technology Reference
In-Depth 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
Θ Γ
Θ, ω Γ
. 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
-
non-existence
,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