[FOM] Weak system for SO logic

[rgheck]

praatika at mappi.helsinki.fi wrote:
> Richard Heck wrote:
>   
>> I think nowadays "the more usual rules" aren't really very usual.
>>
>>     
>
> I based calling them "more usual" simply to my quick check in few  
> books and papers I was more familiar with: e.g. van Dalen, Logic and  
> Structure; Troelstra & Schwichtenberg, Basic Proof Theory; Prawitz,  
> "Ideas and results in proof theory"; and Leivant, "Higher order logic"  
> - all (if I read them correctly) present the rules amounting to the  
> full impredicative comprehension, and only them.
>
> In addition to Takeuti, at least Manzano, in Extensions of First-Order  
> Logic, mentions other options. She refers back to the classic (Henkin  
> 1953).
>
> But it seems to me that at least in the sources with deal with natural  
> deduction, these really are the "more usual" ones. However, I would be  
> very interested in learning about contrary evidence...
>
>   
Yes, I suppose that if you're committed to natural deduction and natural 
deduction only, then the rules will need to be formulated in such a way 
that e.g., from (F)(...F...) you can infer ...A..., where A is a 
formula, not just a variable. But of course, one can restrict what kind 
of formula is permitted, and thereby get the same kind of restriction as 
by the usual restrictions on comprehension.

My reference to what is "usual" had in mind more the work on reverse 
mathematics, subsystems of PA^2, and the like, where restrictions on 
comprehension are in focus. There, the standard way to proceed is with 
weak rules and explicit comprehension.

rh


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