[FOM] second-order logic once again

[Patrik Eklund]

Even so called first-order, i.e. logic at 'fons et origo' does not have a 
"perfectly well-determined set of formulae", obviously since "set" is not 
defined, and the recursion theorem is not at hand.

Foundational logic does not respect the order in which logic building
locks are created. The underlying signature is also in the grey zone e.g. 
since type constructors cannot be formalized in te 'fons et origo' logic.

The sequence should be the following:

- fix the signature, i.e. fix the set of terms
- fix the set of sentences (and close the door to the set of sentence)
- fix entailment (and not even to mention logical consequence and models)
- then discuss proof calculi

And we should not be allowed to call "|- P" a sentence just because "P" is 
a sentence. Of course, a century ago it was allowed, but I believe we 
should distinguish between completeness when allowing "|- P" to be a 
sentence in "fons et origo logic" from completeness as analyzed in 
logics e.g. as formally constructed within category theory.

The set of terms is a good example where the "English language definition" 
is ok. It states basically that "the smallest set that contains variables, 
and whenever we have terms and an operator, operating on those terms gives 
another term". This set can be formalized in ZFC. Can anybody point at a 
paper or book where this formal construction actually is presented?

The set of lambda terms is a excellent example where the "English 
language definition" is not sufficient, e.g. since it leads to renaming 
problems. We somehow say that this definition is basically ok, but we have 
to remedy the situation to take care of some strange situations. Type 
theory then goes into serious flaws when foundational issues re-enter the 
scene. Schönfinkel's, Curry's and Church's foundational ideas didn't 
really reach out, did they? And Kleene ignored the issue for too long.

Mixing metalanguage and object language is the root of many things.

So basically, I never understood the prefectly precise meaning of 
"second-order".

Patrik

On Mon, 3 Sep 2012, Robert Black wrote:

> As everyone on this list knows, the completeness theorem fails for 
> second-order logic.
>
> Those of us who, like myself, are card-carrying second-orderists can say what 
> this means: the set of second-order validities, *a perfectly well-determined 
> set of formulae*, is not r.e. (indeed not even remotely: it's not definable 
> in nth-order arithmetic for any n and so on and so on).
>
> But suppose you're not a card-carrying second-orderist, so you don't think 
> there's a perfectly determinate 'set of second-order validities'. (Perhaps 
> you balk at the consequence that CH must have a truth-value.) How do you 
> state the incompleteness theorem?
>
> Of course any r.e. set is determinate, so if the set of second-order 
> validities isn't determinate, it can't be r.e.. But surely that's not what 
> the incompleteness theorem says.
>
> So what does it say? (In your answer, don't use expressions like "any model" 
> unless you're sure they aren't presupposing the determinacy of second-order 
> logic).
>
> Robert
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>