# A Proof-Theoretic Interpretation

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 t*I* 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*

__ __ __r____ ____1____D ____A____ ____i ____(____i ____∈ __* I ) r* 1-

*D*t

*I Ai*

__ ____ __ __r____,____ ____A ____1____D ____B____ ____ __

*r* 1-*D A* ⇒ *B*

__ __ __r____ ____1__* D A ( A D(a)) r* 1-

*D a*

__r____,____A____i____1__

*t*

__D____C__(i I ) r,*I Ai*1-

*D C*

__ __ __r____ ____1____D ____A ____r____,____ ____B ____1 ____C____ ____ __

*r, A* ⇒ *B* 1-*D C*

__ __ __r____,____ ____A ____1____D ____C ____(____ ____A ____∈ __* D (a )) r, a* 1-

*D C*

The function closure with respect to *X* ⊂ *U* and functions *f*1 *... fn* with arities

*k*1 *... kn* over *U* , is then formally defined by the following definition

*a* **=** T *(a* ∈ *X )*

*fi (x*1 *... xki )* **=** *(x*1 *... xki ) (i* ≤ *n)*

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

Similarly the *functional closure* with respect to *X* ⊂ *U* , functions *f*1 *... fn* with

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

is given by a definition *D(X, f*1 *... fn , F,Φ)*:

*a* **=** T *(a* ∈ *X )*

*fi (x*1 *... xki )* **=** *(x*1 *... 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]).