[FOM] Weak system for SO logic

[rgheck]

praatika at mappi.helsinki.fi wrote:
> Usual axiomatic systems (or rules of inference) for "Second order  
> logic" involve some kind of comprehension scheme, either predicative  
> of full (or these can be derived).
>
> However, Takeuti, in his book Proof Theory, first introduces a system  
> BC, "basic calculus", for SOL which, in his words, "does not contain  
> any 'comprehension axiom'" (p. 135-6 in the 1st ed.).
>
> Is anyone more familiar with this system, and its properties? I would  
> be especially interested in knowing whether there is some natural  
> counterpart of this system in natural deduction?
>
> * * *
>
> This is related to the study of subsystems of SO arithmetic. These  
> axiom systems must be equipped with some rules of inference. But  
> exactly what? Surely not the ones which amount to (full or even  
> predicative) comprehension... But perhaps one would like to have  
> *some* rules for the SO quantifiers too?
>
>   
I don't know Takeuti's book, but there's certainly a system that fits 
these words. Let's say we're dealing with a natural deduction system for 
FOL. Then we add second-order quantifiers to the language, and take as 
rules the obvious analogues of the first-order rules, viz:
(F)(...F...) |- ...G...
...G... |- (F)(...F...), subject to the usual restrictions
and corresponding rules for \exist, viz:
...F... |- (EG)(...G...)
and I won't do EI. Note the UI and EG here require instantiation by a 
VARIABLE. 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)
It's reasonably obvious that the system adds little to FOL.

Richard


-- 
-----------------------
Richard G Heck Jr
Professor of Philosophy
Brown University