# FOM: Axioms:reply and two corrections

Colin Mclarty cxm7 at po.cwru.edu
Sun Feb 1 02:40:15 EST 1998

```	Charles Silver said it seems that some people on each
side of the SET/TOP debate regard simple formal axioms as a
criterion for fom, and he is probably right. But I do not
regard it as a criterion. I think simplicity of axioms is one
nice goal. I like the axiom systems Harvey gave, and freely
agree they have an aesthetic unity mine lack. On the other hand
I claim that 15 is substantially less than infinite, and in this
sense my system is simpler than his. Neither fact seems to me
decisive for fom. I posted my axioms because Harvey and Steve
Simpson asked me to. They are certainly not how I see the
subject.

I do think any candidate for fom must be first order
expressible, I do not think the particulars of the expression
weigh very heavily on the question of whether something can
be fom.

Niel Tennant and Soren Riis both pointed out a typo:

>> 2.  (f,g,h)(there exist A,B,C) [ (f:A-->B and g:B-->C) iff
>>        (for some h)M(g,f;h)]

The "h" in the first quantifier (which, technically, is idle
anyway) should be deleted. And the openning square bracket should
go before the existential quantifier.

(f,g) [ (there exist A,B,C)(f:A-->B & g:(B-->C)  iff

Soren Riis made me notice my subobject classifier axiom only says
subobjects have classifying arrows, where it should also say
every arrow to *W* classifies a subobject. This makes a comprehension
axiom. Here I quote the original and follow it with the addition:

> 12.  (f,A,B) [If (m(f) & f:A-->B) then (there exists a unique
>u:B-->*W*)
>        such that (h,k,j)[If (M(k,t;j) & M(u,h;j) then
>                (there exists a unique v such that M(f,v;h))]]

& (u,B) [ If u:B-->*W* then (there exist f,A)(f:A-->B and
(h,j,k)[If (M(k,t;j) & M(u,h;j) then
(there exists a unique v such that M(f,v;h)]]

I apologize for any confusion this caused. Soren developed a rather
good sketch of a model for the axioms as I gave them, clearly