A Paraconsistent Higher Order Logic - Artificial Intelligence and Symbolic Computation - page 49

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 ∇ - 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.