[FOM] "What is a 'set', anyway?" A simple, useful, precise, and constructive answer.

[Daniel Méhkeri]

CZF is a well-known, useful formal system of set theory which can formalise an awful lot of constructive mathematics. It is classically, but not constructively, equivalent to the standard ZF. I had asked about it on FOM a year or so ago. It seems CZF is normally justified in terms of constructive type theory. This really begs the question of what, in the name of the good lord that created the integers, is a constructive type. Well, they satisfy various closure conditions. If needed, they can in turn be numerically interpreted. But surely we can do better directly. The following is my attempt to distill this into a precise, easily understood (maybe even "high school") answer. 

I'm sure we will all agree that 

  { f_n | g_n = h_n } 

is a valid set, when f, g, and h are partial computable sequences of logically prior sets (using the expected convention for partial terms). But what is remarkable is that, if we use intuitionistic logic with Church's thesis, we do not need any other sets! I claim the universe of these sets validates all of CZF, plus dependent choices. The constructive and predicative justification is immediate (or, at least, "generalised predicative", since we are using inductive definitions).

To answer an expected question: power sets do not generally exist in this universe. The exponential of two sets always exists, and this is classically equivalent to the existence of power sets; in this universe, however, there is no "set of all truth values" to exponentiate.

To remove any remaining imprecision, I will spell this all out. It won't take much space. Let's take some standard enumeration of the computable partial functions, and write {f}(n) for the result of applying the f'th computable partial function to n. Let's call a computable partial function _well-founded_ if its outputs, when defined, code for well-founded computable partial functions, recursively. (WFCPFs for short.) They are in fact just a slight variant on Church-Kleene ordinal notations. 

Let's interpret the unbound quantifiers as ranging over the codes for WFCPFs. Let's take the bound quantifiers separately from unbound ones. Let's interpret bound quantifiers and the extensional equality and membership relations by mutual induction along these WFCPFs, as follows: 

 - "(there exists g in f) PHI(g)" means (there exists n) {f}(3n) defined, and {f}(3n+1) defined, and {f}(3n+2) defined, and {f}(3n+1) extensionally equal to {f}(3n+2), and PHI({f}(3n))
 - "(for all g in f)" similarly 
 - "f extensionally equal to g" means ((for all h in f) h in g) and ((for all h in g) h in f)
 - "f in g" means "(exist h in g) f extensionally equal to h"

I claim the theorems of CZF are all true under this interpretation. As I say, Church's thesis is required, specifically for strong collection, relativised dependent choices, and subset collection. The latter is the most complicated, so I will sketch a solution: if x = { f_n | g_n = h_n }, and y = { p_m | q_m = r_m }, then let z = { t_i | 0=0 }, where in turn t_i = { u_{i,n} | (g_n, q_{{i}(n)}) = (h_n, r_{{i}(n)}) }, and u_{i,n} = p_{{i}(n)} if f_n is defined. Given the other axioms, restricted separation can be finitely axiomatised by emptyset and binary intersection. The rest is not terribly hard.

More generally, I propose the template { f_n | COND(g_n,h_n,...) }, where COND is some fixed, precise, numerically meaningful condition, and "numerically meaningful" can be stretched to plead for larger set axioms. Or, briefly: *a set is a computable, conditional enumeration of prior sets*. For instance, I believe the universe of { f_n | g_n = h_n and j_n is a WFCPF } validates the "regular extension axiom" and I suspect even something classically equivalent to inaccessible cardinals. 

But if we are not interested in larger set axioms, then we need no conditions beyond extensional equality of two prior sets. 

Regards,
Daniel Mehkeri

-- 



      Découvrez les styles qui font sensation sur Yahoo! Québec Avatars.
http://cf.avatars.yahoo.com/