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

We have the following abbreviations (we omit the types):

ϕ|ψ ≡ D ϕψ ϕ = ψ ≡ Q ϕψ ϕ ≡ Q ϕ ˘

ϕ ≡ C ϕ ευ.ϕ ≡ C λ υ.ϕ ∂ ϕ ≡ V ϕ
Only a few of these abbreviations need explanation. The (global) choice operator
ε

∀υ.ϕ ≡ A λ υ.ϕ ˜

); if no such
value exists then an arbitrary value is chosen (of the right type). The choice is
global in the sense that all choices are the same for equivalent

chooses some value υ for which ϕ is satisfied ( υ can be free in ϕ

ϕ 's, hence for

instance we have ( εx.⊥ )=( εx.⊥ ).

The notation ˘ ϕ turns ϕ into a singleton set with itself as the sole member

˘

and ˜ ϕ is its inverse, since ϕ = ϕ , which is called the selection property, cf. the

selection operator is of course also defined for non-singleton

sets, namely as the (global) choice operator just described. We say a little more
about these matters when we come to the choice rules.
We can even eliminate the

ı in Q 0 [4]. But ˜ ϕ

λ -notation if we use two additional primitive

combinators, the so-called S and K combinators of suitable types. For example,

the identity function λ x.x is available as the abbreviation I ≡ SKK , cf. [7].

7.4 Structural Rules

In the sequent Θ Γ we understand Θ as a conjunction of a set of formulas

and as a disjunction of a set of formulas, and we have the usual rules for a

monotonic sequent calculus:

Γ

Θ, ϕ ΓΘ ϕ, Γ Cut Θ Γ

Θ, ϕ Γ

Θ Γ
Θ ϕ, Γ

Θ Γ

Notice that ϕ ϕ follows from these rules and the rules for equality below.

7.5 Fundamental Rules

We use the abbreviation:

=

ϕ ψ ≡ ( λ pq. ∀x. px = qx ) ϕψ

We have the usual conversion and extensionality axioms of the λ -calculus:

=

( λ υ.ϕ ) ψ = ϕ [ ψ/υ ] ϕ ψ ϕ = ψ

Here ϕ [ ψ/υ ] means the substitution of ψ for the variable υ in ϕ (the notation

presupposes that ). For later use we note that if the

notation for an arbitrary so-called eigen-variable

ψ is substitutable for υ in ϕ

π ψ

is used in place of then it

ϕ ψ

must not occur free in other formulas in the given axiom/rule. Also [ ]means

ϕ ψ/υ υ

[ with respect to the given axioms/rule.

We have the usual reflexivity and substitution axioms for equality:

] for an arbitrary variable

ϕ ϕ ϕ ψ, θ ϕ θ ψ

= = [ ] [ ]