FOM: Re: "categorical foundations" -- an oxymoron

[Michael Thayer]

Steve recently took Colin to task with the following comment:


>They [Colin's axioms L1-L4]don't do what foundations of
>X are normally expected to do: explain X in terms of basic concepts
>and indicate the essential relationships between X and the rest of
>human knowledge.
...
>
>This entire posting by McLarty is an excellent example of how
>structuralism is anti-foundational, because it disrupts virtually all
>of the essential ties and links between various subjects or branches
>of human knowledge.


Maybe Steve could clarify his complaint in light of his paper "On the
Strength of K¨onig's Duality Theorem
for Countable Bipartite Graphs".

In the abstract Steve explains his result as follows:

Let CKDT be the assertion that, for every countably infinite bipartite
graph G, there exist a vertex covering C of G and a matching M in G such
that C consists of exactly one vertex from each edge in M . (This is a theo-
rem of Podewski and Steffens [12].) Let ATR0 be the subsystem of second
order arithmetic with arithmetical transfinite recursion and restricted in-
duction. Let RCA0 be the subsystem of second order arithmetic with
recursive comprehension and restricted induction. We show that CKDT
is provable in ATR0 . Combining this with a result of Aharoni, Magidor
and Shore [2], we see that CKDT is logically equivalent to the axioms of
ATR0 , the equivalence being provable in RCA0 .

In what way do the systems ATR0 and RCA0 (reading 'CKDT' for 'X' in the
following)
 "explain X in terms of basic concepts and indicate the essential
relationships between X and the rest of human knowledge."??

I would not suppose that "arithmetical transfinite recursion" was a basic
concept, and the only essential relationships I see here are between CKDT
and various technical issues in set theory.

Is this an unfair question, because this paper was written BEFORE Steve
started to do foundations?

I am not trying to be too confrontational here, but frankly all I see in
Steve's work is a bunch of interesting technical results in set theory and
the implied promise to some day relate these results to basic foundational
issues which would be clearly of general intellectual interest.  Possibly a
sketch of Steve's program would make the whole thing clearer.