FOM: categorical pseudofoundations: Friedman and Kanovei

[Torkel Franzen]

  Colin McLarty says:

  >>The axiomatization I gave using axiom schemes uses only very few axioms -
  >>not infinitely many. This is because an axiom scheme is a *single axiom* in
  >>the appropriate form of predicate calculus which uses the obvious rule of
  >>substitution. I.e., you replace a schematic letter with any formula.
  >
  >That's a nice idea. Certainly it is not standard. 

  As I mentioned in my earlier comments on Feferman's "Does
mathematics need new axioms", this is a view of schematic predicate
logic theories (close to the thinking of Zermelo and) much touted in
Feferman's later work. His JSL paper "Reflecting on incompleteness"
makes a particularly intriguing use of this point of view. Charles
Parsons also develops this line of thought from a philosophical point
of view, e.g. in "The impredicativity of induction" and "Objects and
logic".  I'm not prepared to make any definite assertions about the
historical course of events as regards the interpretation of schematic
theories, but it does seem that at present many tend to take it for
granted that the choice is between thinking of e.g. PA either in terms
of infinitely many first-order axioms or as a second-order theory,
where the latter is associated with set theory.