[FOM] Why not this theory be the foundational theory of mathematics?

[Patrik Eklund]

Some comments from my side mostly concerning category theory (even if 
Zuhair does not bring it up, but Thomas does).

See below.

Patrik

On 2019-03-27 14:21, Thomas Klimpel wrote:
> Dear Zuhair,
> 
> you ask "Why not this theory be the foundational theory of 
> mathematics?"
> 
> I would say it is simply not sufficiently different from ZFC. Remember
> that reference to ZFC implies the possibility to add some inaccessible
> cardinals if necessary. For example, HoTT with propositional
> truncation and choice on the level of sets needs two inaccessibles,
> and this is not considered to be a big deal. But HoTT itself is so
> different from ZFC in its basic approach that it is worthwhile to use
> it as an alternative foundation.
> 
> Also category theory would be very different from ZFC, but it is not a
> foundational theory. It is not, because it is too vague,

Saying "too vague" does not mean so much here unless explained more in 
detail.

> and implicitly uses higher order quantifiers. (The category of all sets 
> is
> specified by a sort of "last word quantification", but this is
> troublesome for a foundational theory. A foundational theory should
> lay down the first words, not insist on having the last word.)

There is indeed a debate within category theory about its set theoretic 
foundations, Grothendieck's being mostly adopted, but also in a 
generalized view that there are universes over universes over universes. 
Set theory stops at sets and classes, and needs to pay attention to 
quantification as involving sets and classes.

This is indeed intuitively about the last word.

But the first words are troublesome for fons-et-origo foundations. Like 
Peano once said, "in mathematics we usually put characters side by 
side". That could algebraically be seen as magma, but at fons-et-origo 
of logic we have nothing, do we? We have sets, that's all. Then we 
create terms (expressions) using operators saying, in natural language, 
things like "if t is a term, and w an operator, then w(t) is a term". In 
category theory the term functor can be made very precise and departs 
from the "putting characters side by side" natural language lego 
approach. The tricky thing happens when we add quantifiers as characters 
and treat them as formal symbols (unlike lambda which Church said was an 
informal symbol). Then we similarly create "formulas" by putting symbols 
in sequence, using natural language to say how and how not these 
characters can be legoed together. Category has been successful in 
dealing with lambda terms, but dealing with formulas involving 
quantifiers is tricky. Church used iota as a type for terms/expressions, 
and this can be made precise also in category theory, but Church's o 
type for sentences/formulas is troublesome. Typing and justifications 
e.g. a la Artemov is nice, but the "algebra" of combining justifications 
drops down out of the blue, so as to say, and those formulas are formed 
a bit different as just characters side by side. Rules for forming 
Artemov's formulas are also explained basically in natural language. 
There is kind of a magna for the "justification constructor" appearing a 
bit like the function type constructor in lambda calculus. Modalities 
come into play, but modalities are more operator like than quantifiers. 
In programming, like HOL, Coq, Haskell, etc., quantifiers are treated as 
operators, but then the justification of it boils down to believing that 
the compiler is "foundationally correct".

So personally I have much more difficulties with those first words than 
with the last ones.

> 
>> The following is a link to clearer exposition of this theory:
> 
> I don't see how this should be clearer than your initial email. It
> contains fewer information and references, and doesn't explain
> anything not explained in your initial email.
> 
> 
>> All axioms of class theory and set theory can be interpreted in a 
>> first order
>> theory (with equality) plus primitives of set membership "\in", and 
>> "W" standing
>> for some fixed set.
> 
> I remember having seen the use of an explicit constant for the class
> of all sets before. I just checked some references, but failed to find
> it again.
> 
>> This theory also fulfill all of F.A. Muller's criteria for a founding 
>> theory of mathematics!
>> for Muller's criteria see:
>> http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF
> 
> Muller's article also uses an explicit constant for the class of all
> sets, but he uses "V" instead of "W". Assuming you based your theory
> on the description from Muller's article, why did you replace "V" by
> "W"? How is your axiomatic theory related to the axiomatic theory
> presented in Muller's article? Is it the same? Or is it more powerful?
> 
> 
>> 2. Set Comprehension schema: if \phi is a formula in the pure language 
>> of set
>> theory [i.e., doesn't use the symbol "W"], then:
>> 
>> x_1,..,x_n \in W -> [\forall y (\phi -> y \subset W) -> \forall y(\phi 
>> -> y \in W)],
>> 
>> is an axiom.
>> 
>> In English: any pure set theoretic formula from parameters in W, that 
>> only
>> holds of subsets of W; also only holds of elements of W.
> 
> I don't remember having seen this axiom scheme before, but I may be
> wrong. Is this your invention, or is this basically equivalent to the
> "Axiom of Completeness (Compl). The class of all sets V is complete,
> i.e. all classes contained or included in sets are sets."
> from Muller's article (or some axiom scheme from another reference)?
> 
> 
>> Why wan't such a simply presented natural theory qualify as the 
>> foundational theory of mathematics?
> 
> We already know that there cannot be a perfect foundational theory of
> mathematics. ZFC serves the role as a foundation of mathematics well
> enough for the moment. The described axiomatic theory is not really
> that different from ZFC, with respect to foundation. It may be
> different with respect to class and set theory. So studying it as an
> alternative set theory could be interesting. In fact, there are many
> alternative set theories, and their study is a valid and interesting
> field of mathematics.
> 
> Regards,
> Thomas
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom