[FOM] Weak system for SO logic

[praatika@mappi.helsinki.fi]

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?



Best, Panu




Panu Raatikainen

Ph.D., Academy Research Fellow,
Docent in Theoretical Philosophy

Department of Philosophy
University of Helsinki
Finland


E-mail: panu.raatikainen at helsinki.fi

http://www.mv.helsinki.fi/home/praatika/