On Tue, Sep 24, 2002 at 12:18:36PM +0200, Bruno Marchal wrote:
> You are right. But this is a reason for not considering classical *second*
> order logic as logic. Higher order logic remains "logic" when some
> constructive assumption are made, like working in intuitionist logic.
> A second order classical logic "captures" a mathematical structure in a very
> weak sense. My opinion is that the "second order *classical* logics" are
> misleading when seen as logical system. Why not taking at once as axioms
> the set of all true sentences in the standard model of Zermelo Fraenkel (ZF)
> set theory, and throw away all rules of inference. This "captures", even
> categorically, the set universe. But it is only in a highly technical sense
> that such a set can be seen as a theory.
If we can take the set of all deductive consequences of some axioms and
call it a theory, then why can't we also take the set of their semantic
consequences and call it a theory? In what sense is the latter more
"technical" than the former? It's true that the latter may require more
computational resources to enumerate/decide (specificly it may require the
ability to compute non-recursive functions), but the computability of the
former is also theoretical, since currently we only have access to
bounded space and time.
> "Logically" you are right, and what you said to Brent is correct.
> I just point here that the use of second order classical logic can be
> misleading especially for those who doesn't have a good idea of what is
> a *first order* theory.
Some would argue that it's first-order theory that's misleading. See
Stewart Shapiro's _Foundations without Foundationalism - A Case for
Second-Order Logic_ for such an argument.