Home Philosophy Advances in Proof-Theoretic Semantics
There are three major issues to observe in the definitions given above in Sect. 2:
1. We introduce functional constructions, S( f ), ∃( f ) and ∀( f ), by a defining con-
dition asking for the notion we define to be closed under a given function.
2. We introduce a conditional construction A → B by a defining condition asking
B to follow from A.
3. What we actually state in the 'definitions' are closure conditions for notions we hope to be able to define in one way or another.
The idea of function closure (in the realm of monotone inductive definitions) is that we have some things a, b,... given and also some functions f, g,.. .. We then define a notion X by saying that
• a, b,... is an X ,
• if x is an X , then f (x ), g(x ), . . . is an X .
Implicitly this means that X is defined by these clauses and nothing else. From an intensional and foundational point of view in 'generating' X the things that f, g,... act on in X are not given, besides the initial things a, b,.. ., they are introduced as we build X . Once defined, X is then the smallest collection of things including a, b,... and being closed under f, g,.. ..
Similarly the idea of a functional closure is that we have some things a, b,... and functions f, g,... given and also functionals F, G,.. .. Analogously, from an intensional and foundational point of view, the functions 'in' X that F, G,... act on, i.e., functions that X is closed under, are not given, but introduced as we build X . In both cases we take for granted certain things as primitive notions. In the first case some given objects and functions and in the second case some given objects (not necessary in all cases), some functions and functionals. In both cases what we rely on is, so to speak, inscribed in fundamental circles of reasoning. The objects we generate in building up the function closure are of course given in an abstract manner of speaking. The same thing holds for the functions we generate in building up the functional closure:
• a, b,... is an X ,
• if x is an X , then f (x ), g(x ), . . . is an X ,
• if X is closed under f , then F ( f ), G( f ),... is an X .
In non-foundational and mathematically precise definitions we assume there is given a universe of objects, a function space and some functions and functionals defined on this universe/function space.
When defining A → B is true in terms of if A is true, then B is true it is really an issue what we mean by if A is true, then B is true as a defining condition. A reasonable interpretation of this is that what we mean to say is that B follows from A on the basis of information provided by the given definition, i.e., that we can prove B to follow from A in the local logic that the given definition implicitly defines. With respect to set theory this means that the sets we introduce, or to be more precise the set definitions we introduce, open up for reasoning relative to a local set theoretic context. What this could mean will be explained below.