 Home Philosophy Advances in Proof-Theoretic Semantics

# 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 aU 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

r 1D A i (i I ) r 1-D tI Ai

r, A 1D B

r 1-D AB

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

r 1D A r, B 1 C

r, AB 1-D C

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

The function closure with respect to XU and functions f1 ... fn with arities

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

a = T (aX )

fi (x1 ... xki ) = (x1 ... xki ) (in)

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 XU , functions f1 ... fn with

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

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

a = T (aX )

fi (x1 ... xki ) = (x1 ... xki ) (in)

F ( f ) = t (xf (x )) ( fΦ)

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

T = T

F = T

⎪ /

AB =

( A, B)

/

AB =

A = B =

S( f )

( A, B)

/( A, B)

/(xf (x ))

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

⎪ /

⎪⎩

T = T

⎪ ∀( f ) = (xf (x ))

AB = AB

AS( f ) = f ( A)

⎪⎨

T SΦ

A = B = /((xAxB), (xBxA))

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

/

( f ) =

( f (x ))

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]).

 Related topics