[FOM] Weak system for SO logic

[Richard Heck]

praatika at mappi.helsinki.fi wrote:
> Quoting rgheck <rgheck at brown.edu>:
>
>   
>> we add second-order quantifiers to the language, and take as
>> rules the obvious analogues of the first-order rules ...
>>     
>    :  :
>   
>> This is what makes the system weaker than with predicative
>> comprehension. You won't be able to derive something like:
>> (EH)(x)(Hx <--> Fx & Gx)
>>     
>
> Thanks, Richard, that's what I (vaguely) thought.
>
> Now the question arises, is there any really good reason to take the  
> more usual rules (which entail even impredicative comprehension) as  
> more *natural* logical introduction and elimination rules for SO  
> quantifiers than the above neutral ones?
>
>   
Well, I guess people will disagree about whether there is any "really
good reason". But it's worth thinking about the analogy between the case
of second-order logic and the case of first-order logic with function
symbols. In the latter case, one can formulate UI as: From(x)(...x...)
infer ...t..., for any term t. This will then entail the more familar:
(Ex)(t = x), for any term t. One might think that this sort of axiom was
similar to the comprehension principles, and that the more general
version of UI was similar to what you call "the more usual rules". I'm
not necessarily defending that, just mentioning it.

That said, I think nowadays "the more usual rules" aren't really very
usual. That is how Frege formulates the rules in _Begriffsschrift_, but
even in _Grundgesetze_ he shows some awareness that there are really two
things going on. It's worth disentangling these, which of course is what
happens when we formulate the rules as simply as possible and add
comprehension axioms. Of course, you can place the same sorts of
restrictions on the rules that you might place on comprehension, so it's
not as if you can't consider (say) a predicative system with just rules,
rather than comprehension. But, as I said, it seems more confusing that way.

Richard