Even if we note that there are no definitions having the closure properties stated in Sect. 2 above, there is still the possibility to read these definitions from a more strict intensional point of view. We then look at the closure conditions as clauses in two partial inductive definitions ([6, 7, 13]). The idea is basically to look at if .. ., then

... and is closed under in terms of the notion of logical consequence that defines the

local logic of the definitions in question, i.e., that if A, then B is read as B follows from A by the given definition.

As a mathematical object a (partial inductive) definition D consists of a collection of equations

a=A

for a ∈ U for some given universe of discourse and where A is a defining condition built up from elements in U , T and ⊥ using constructions tI and ⇒. Let D(a) be the collection of conditions defining a in D if there are any and {⊥} otherwise. The local logic of D, 1-D , is then given by the following elementary (monotone) inductive

definition

r, a 1-D a

r 1-D T r, ⊥ 1-D C

r1D Ai (i ∈ I) r 1-D tI Ai

r,A 1D B

r 1-D A ⇒ B

r1D A ( A D(a)) r 1-D a r,Ai 1D C (i I ) r, tI Ai 1-D C

r1D A r,B 1 C

r, A ⇒ B 1-D C

r,A 1D C (A ∈ D(a)) r, a 1-D C

The function closure with respect to X ⊂ U and functions f1 ... fn with arities

k1 ... kn over U , is then formally defined by the following definition

a= T (a ∈ X )

fi (x1 ... xki )=(x1 ... xki ) (i ≤ n)

De f (D(X, f1 ... fn )) is then the smallest set containing X and being closed under the functions f1 ... fn .

Similarly the functional closure with respect to X ⊂ U , functions f1 ... fn with

arities k1 ... kn over U , a functional F : [U → U ] → U and a set Φ ⊂ [U → U ],

is given by a definition D(X, f1 ... fn , F,Φ):

a= T (a ∈ X )

fi (x1 ... xki )=(x1 ... xki ) (i ≤ n)

F ( f )= t (x ⇒ f (x )) ( f ∈ Φ)

Now we might rewrite the definitions SΦ and T SΦ in the following way:

⎧ T= T

⎪ F= T

⎪ /

⎪

A → B=

⎪

⎪ ( A, B)

/

⎪ A ∈ B=

⎪

SΦ ⎨ A = B=

⎪ S( f )

⎪

⎪

⎪

⎪ ( A, B)

/( A, B)

/(x ⇒ f (x ))

SΦ

⎪ ∃( f )= /(x ⇒ f (x ))

⎪ SΦ

⎪ /

⎪⎩

⎧ T= T

⎪ ∀( f )=(x ⇒ f (x ))

SΦ

⎪ A → B=A ⇒ B

⎪

⎪ A ∈ S( f )=f ( A)

⎪

⎪⎨

T SΦ

⎪

⎪

⎪

⎪

⎪ A = B= /((x ∈ A ⇒ x ∈ B), (x ∈ B ⇒ x ∈ A))

SΦ

∃( f )=f (x ) (SΦ)

/

∀( f )=

⎩ ( f (x ))

SΦ

Reading them as foundational definitions we have to accept certain notions as primitive notions; the conditions T and F , the function →, the functionals S, ∃ and

∀, the notion of a function and indexing families over the sets we define. In principle

what amounts to understanding the functional closure as a primitive foundational

notion. The resulting formal systems, defining the local logics of the definitions, are consequently formal systems in an informal sense. They define what a proof is as a foundational notion, providing a proof-theoretic foundation of set theory, that is, using proof-theoretical notions in an abstract and open manner (cf. the notion of a general proof theory in [10–12]).

Found a mistake? Please highlight the word and press Shift + Enter