Towards a computation system based on set theory (Q1825191)

An axiomatic theory of sets and rules is formulated, which permits the use of sets as data structures and allows rules to operate on rules, numbers, or sets. This theory combines the \(\lambda\)-calculus with traditional set theories. A natural set-theoretic model of the theory is constructed, establishing the consistency of the theory and bounding its proof-theoretic strength, and giving in a sense its denotational semantics. Another model, a natural recursion-theoretic model, is constructed, in which only recursive operations from integers to integers are represented, even though the logic can be classical. Some related philosophical considerations on the notions of set, type, and data structure are given in an appendix.