Impredicativity

Lukasz Stafiniak sent me this about impredicativity. I had seen the concern before, but never seen why it was worth any worry. Impredicative comprehension principles are a big convenience for normal mathematics, and don't lead to any paradoxes that we know of.

However, looking at it again, I realised that the basic complaint could be read as "impredicative comprehension is not valid in Kripke's theory of truth." This is more concerning to me. In fact, the concern can be stated just in terms of the Tarski hierarchy: 2nd-order logic does not exist at any stage in the Tarski hierarchy. I was foolishly thinking that there was a direct correspondence between stages in the hierarchy and orders of logic. There is, if we use predicative comprehension! But, impredicative comprehension is "too powerful" to exist at any stage of any recursive hierarchy.

This causes trouble for me, because impredicative comprehension is necessary to my understanding of the natural numbers (and other important things).

Fortunately, the article suggests a solution: impredicative quantifications should be understood at the level of provability. IE, we aren't stating that all instances are true; we are stating something stronger, that they are all provable. (But we use infinitary logic, so that this is not as much of a restriction.) This is a very intuitionistic suggestion.

Unfortunately, we can see that this really just introduces another metalanguage (the language of provability). Hence, comprehension interpreted this way does not include all possible predicates after all (even if we extend the provability interpretation to the point where it covers all cases of 2nd-order comprehension): it skips the predicates which can be defined in terms of provability.

Building a self-referential theory of logical implication which follows the rules we want is hard. The obvious way of doing it just leads directly to Curry's paradox. I still have not finished reading Hartry Field's "Saving Truth from Paradox", but it includes an account of implication which may be helpful. These posts also contain some notes which may be helpful.

I should have known for about a year now that the immediate challenge is to built up to 2nd-order logic, not to build up to set theory. However, this made it hit home: I can't rely on 2nd order logic to be there for me when I need it. I don't yet know what 2nd-order logic is, or where it comes from.

Still, the fact remains that 2nd-order logic is a fairly natural, very useful, and almost certainly consistent set of axioms. It seems probable that aliens would stumble upon it, etc. It does not just poof out of existence. Even just as a syntactic entity rather than one with a semantics, it's still important!