[FOM] Weak system for SO logic
rgheck at brown.edu
Sat Apr 18 10:50:47 EDT 2009
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
> 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.
Richard G Heck Jr
Professor of Philosophy
More information about the FOM