[FOM] Weak system for SO logic
praatika at mappi.helsinki.fi
Fri Apr 3 10:57:16 EDT 2009
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?
Ph.D., Academy Research Fellow,
Docent in Theoretical Philosophy
Department of Philosophy
University of Helsinki
E-mail: panu.raatikainen at helsinki.fi
More information about the FOM