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

7.1 Syntax
We define the following sets of types and terms - the latter for each type

τ and

in the case of the λ abstraction we additionally require that τ is of the form αβ .

T = o |TT |S L τ = L γτ L γ | λ V α . L β |C τ |V τ

Here S is the set of sorts (empty in the propositional case, where the only basic

type is o for formulas), C τ and V τ are the sets of term constants and variables

of type τ (the set of variables must be countably infinite), and α, β, γ, τ ∈T .

We often write τ 1 ...τ m γ instead of the type τ 1 ( ... ( τ m γ )) and ϕψ 1 ...ψ n

instead of the term (( ϕψ 1 ) ... ) ψ n . Note that the relational types are τ 1 ...τ n o

(also called predicates).
If we add a sort of individuals

ι ∇

to the propositional higher order logic

∇ ι (further sorts can be added, but for our

we obtain the higher order logic

purposes they are not needed).

7.2 Semantics
As usual Y X is the set of functions from X to Y .

U αβ ⊆ U U α A universe U is an indexed set of type universes U τ = ∅ such that .

β

The universe is full if is replaced by =.

A basic interpretation

⊆

: C τ → U τ I on a universe U is a function I such

that Iκ τ ∈ U τ for κ τ ∈C τ . Analogously, an assignment A on a universe U is a

: V τ → U τ function A such that Aυ τ ∈ U τ for υ τ ∈V τ .

Amodel M ≡U, I consists of a basic interpretation I on a universe U such

]] M,A : L τ →

that for all assignments A on the universe U the interpretation [[ ·

U τ

ϕ τ ]] M,A ∈ U τ

has [[ for all terms ϕ τ ∈L τ , where (we use the λ -calculus in

the meta-language as well):

[[ κ ]] = Iκ

[[ υ ]] = Aυ

]] A [ υ→u ]

[[ λ υ α .ϕ β ]] =

λ u.

[[ ϕ

]]
For clarity we omit some types and parameters.
What we call just a model is also known as a general model, and a full model
is then a standard model. An arbitrary basic interpretation on a universe is
sometimes considered a very general model.

[[ ϕ γτ ψ γ ]] = [[ ϕ ]] [[ ψ

7.3 Primitives
We use five primitive combinators of the following types (

τ ∈T ):

D ooo Joint denial - Sheffer's stroke

Q ττo Equality

A ( τo ) o Universal quantification

C ( τo ) τ Global choice

V oo Indeterminacy generation