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

7.6 Logical Rules

Let . Negation is different from classical logic. We follow [17]

and add only the following rules:

Θ = {θ | θ ∈ Θ}

Γ Θ
Θ Γ

Γ Θ
Θ Γ

Conjunction and universal quantification are straightforward:

Θ, ϕ, ψ Γ
Θ, ϕ ∧ ψ Γ

ϕ, ψ ϕ ∧ ψ

Θ ϕ ,Γ

Θ ∀υ.ϕ, Γ

[ π/υ ]

∀υ.ϕ ϕ [ ψ/υ ]

Remember that the eigen-variable condition is built into the notation.
We also have to provide axioms for the negation and conjunction in case of
indeterminacy:

∇x ¬x = x x = y ∧∇x ∧∇y x|y

7.7 Choice Rules

We have the following choice axioms [10] corresponding to the Axiom of Choice
in axiomatic set theory:

pυ p p ˜

Notice that due to the use of we can only make a choice if ∃υ. ( pυ ). If we

used a different implication the choice might not be possible at all.

7.8 Generation Rules
We use the following abbreviations:

0 1 2

∞ ≡

0 ≡⊥ 1 ≡ 2 ≡ 3 ≡ ...

N ≡ λ x. x = ∞ T ≡ λ x.∅≡ λ x.⊥

We have the following important axioms:

x ˙ =˙ y x = y ∞ = ∞

py
The first axiom ensures the injective property and the second axiom makes the
third axiom, the induction principle, work as expected.
Hence2+2=4canbestatedin

p ∞ ∧ p 0 ∧ ( ∀x. px p x ˙ )

(seeing + as a suitable abbreviation). It
can also be proved, but many other theorems of ordinary mathematics can not
be proved, of course (it does not contain arithmetic in general).
Since

∇

ϕ ϕ we have among others 1 1, but this is just a curiosity.