[FOM] Weak system for SO logic
rgheck at brown.edu
Fri Apr 3 22:19:15 EDT 2009
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 G Heck Jr
Professor of Philosophy
More information about the FOM