Every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in EFA. EFA is the weak fragment of Peano Arithmetic based on the usual quantifier-free axioms for 0, 1, +, ×, exp, together with the scheme of induction for all formulas in the language all of whose quantifiers are bounded.On the other hand, Harvey Friedman is also well known for
… attempts to justify large cardinal axioms by demonstrating their necessity for deriving certain propositions considered "concrete".I think the “giant ant” I mentioned here was part of that research. On the gripping hand, the concrete propositions look like statements that logicians pulled out of a vulgar body aperture just to be ornery.
I was puzzled by this for a while. He was arguing in favor of one conclusion while providing something that might be evidence against it. I then realized what he was doing: He was trying to falsify a statement. This is so rare in philosophy, that it was hard to recognize. Philosophers have talked about falsification for years but it always seemed to for others to do. Now that a philosopher is applying the concept of falsification, it might be time for philosophy to climb the science hierarchy.