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.