Sets

From an extensional perspective viewing sets as collections of given sets, the notion of an elementary set connects to hierarchies of what we somehow can visualize, i.e., low levels of the cumulative hierarchy. From an intensional point of view, where the act of abstraction with respect to a given defining property/function is in focus, a natural notion of an elementary set must build on characteristics of the definition. The Levy hierarchy [8] of course shows strong connections between both perspectives for ZF , but the situation here is a bit different as we look at set definitions in much

more open set theories. It is for instance clear that a set such as S(λ(x = x )) is a

very elementary set with respect to its defining function.

Let us say that a set

• S( f ) is a Φ-set if SΦ is closed under f , i.e., that f (x ) follows from x in SΦ for

all sets x in SΦ,

• S( f ) is elementary if it is a Φ-set for all Φ.

Both S(λ(x = x )) and S(λ(x ∈/ x )) are elementary sets. A simple example of a non-elementary set is S(λ(x = S(λ(y = a)))).

Foundational Issues

It is clear that consistency is not an explicit issue in the present context. Falsity (i.e., F ) is by definition something that is not defined and can thus never be proved in a set theory SΦ. But consistency of course relates to issues of cut elimination for sequent calculi, which relates to upward absoluteness. So assume we have a set theory S where all basic defining conditions are absolute, or at least upward absolute. From the point of view of set theoretic reasoning the sets definable in these theories are somehow 'nice' sets.

Stating that there are functions Φ with certain properties is what here corresponds

to axioms of set theory, and proving or believing that the theory SΦ is absolute in some sense corresponds to defining a model for the axioms. But while the true cumulative hierarchy V is the universe in which these models live, a general set theory SΩ with no restrictions on functions is the context in which these definitional theories SΦ live. The big difference is that V is an extensional context, i.e., the true world of pure sets, whereas SΩ is an intensional context based on a very general notion of set definitions not presupposing a rationale of welldefinedness. What set theories SΦ reflect is not inner models, but the locality of proof logics.

The idea of reduction is somehow inherent in the notion of foundations, i.e., that we build on elementary foundations. Although we evidently just walk around in ontological circles, this idea of reduction is not meaningless. A very clear and conceptually elementary model provides a reduction in the sense that we see clearly why given axioms make sense. The argument that the idea of a reduction is an illusion since the construction of the model involves all the power of the axioms themselves does not make for a strong case. It is the suggestive simplicity and clearness of the picture the model paints that is important, i.e., that we really can see the construction. Simplicity with respect to definitional principles builds another type of foundations; the local logic of given definitions. The foundational construction here is the functional closure interpreted as a partial inductive definition. What is important is then that we can 'see' the proofs that build the sets and the set theoretical arguments in a very elementary sense. A typical example making the difference clear is the power set P( A) = S( P A) where P Ax is ∀z(z ∈ x → z ∈ A). To envision P( A) as a collection of given objects involves very abstract acts of visualising for large sets A.

Can we see the set, can we trust the axiom? It is of course clear that S( P A) as a set theoretical definition opens up for logical complexity in reasoning, but in this case it is a matter of visualising proofs with respect to a given definition. Can we see the proofs, can we trust the definition?

The definition itself is in some sense elementary, the proofs defining reasoning in theories SΦ are also elementary in some sense. Thus there is a reduction in foundations in some sense. But in actual set theoretical practice we need to trust certain closure conditions on the definitions allowing for nice forms of reasoning for what we believe to be nice theories SΦ. The major challenge here is to develop set theory within the framework of theories SΦ and explore the meaning of classical set theoretical issues in this context.

Since SΩ is closed, in the sense that each definable function f is reflected in a

set S( f ), we have the following

Theorem V (modulo large cardinals beyond ℵ0) has a definable reflection in SΩ.

References

1. Aczel, P.: Frege structures and the notions of proposition, truth and set. In: J. Barwise, H.J. Keisler, K. Kunen (eds.) The Kleene Symposium. North-Holland (1980)

2. Cantor, G.: Contributions to the Founding of the Theory of Transfinite Numbers. Dover Publications (1955)

3. Ekman, J.: Normal proofs in set theory. Ph.D. thesis, Department of Computing Science, Chalmers University of Technology (1994)

4. Fraenkel, A.A., Bar-Hillel, Y., Levy, A.: Foundations of Set Theory. North-Holland, Amsterdam (1973)

5. Hallnäs, L.: On normalization of proofs in set theory. Ph.D. Thesis, Dissertationes Mathematicae CCLXI, Warszawa (1988)

6. Hallnäs, L.: Partial inductive definitions. Theor. Comput. Sci. 87, 115–142 (1991)

7. Hallnäs, L., Schroeder-Heister, P.: A proof-theoretic characterization of logic programming II: programs as definitions. J. Log. Comput. 1(5), 635–660 (1991)

8. Levy, A.: A hierarchy of formulas in set theory. In: Memoirs of the American Mathematical Society, vol. 57. American Mathematical Society, Providence (1965)

9. Prawitz, D.: Natural Deduction. A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm (1965)

10. Prawitz, D.: Ideas and results in proof theory. In: Fenstad, J.E. (ed.) Proceedings of the Second Scandinavian Logic Symposium. North-Holland (1971)

11. Prawitz, D.: Towards a general proof theory. In: Suppes, P. (ed.) Logic. Methodology and the Philosophy of Science IV. North-Holland, Amsterdam (1973)

12. Prawitz, D.: On the idea of a general proof theory. Synthese 27, 63–77 (1974)

13. Schroeder-Heister, P.: Rules of definitional reflection. In: Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science. Los Alamitos, Montreal (1993)

14. Schroeder-Heister, P.: Paradoxes and structural rules. In: Novaes, C.D., Hjortland, O.T. (eds.) Insolubles and Consequences: Essays in honour of Stephen Read. College Publications, London (2012)