Re: Turing completeness of the functional paradigm?



Robert Low <mtx014@xxxxxxxxxxxxxx> said:
>> there are certainly
>> sets of axioms which uniquely define the
>> natural numbers: the second
>> order Peano axioms do this.


Chris Menzel replied:
> Assuming, of course, a standard model theory
> for second-order languages.

This assumption has in fact been made.
SEriously, it is just part of the general context.
There is one standard semantics that people mean
when they talk about second-order logic. All lesser
others REALLY ARE lesser and really are, BECAUSE they
are lesser, NON-standard.

> As I'm sure you know, though,
> there is also a "general" model theory for
> second-order languages that Henkin introduced
> in proving the completeness of simple type theory,
> and second-order languages interpreted by this model
> theory are no more expressive than first-order
> languages.

But if you want to use the Henkin semantics, you HAVE to SAY
"I'm using the Henkin semantics". If you DON'T say that
and INSTEAD just say "I'm using 2nd-order logic", then you
are LEGITIMATELY presumed to be using the full/standard
semantics. There are GOOD reasons for this. You hinted
at one of them regarding this Henkin alternative: it makes
the second-order languages no more expressive than 1st-order
ones -- in other words, if you do this, you're fundamentally
NOT using 2nd-order logic AT ALL -- you might as well have
stayed at 1st: you're (conversely from the original metaphor)
a sheep in wolf's clothing.

The better reason, of which the first was basically an
instance or corollary, is that set theory itself -- AT FIRST
order -- is, in the ORIGINAL metaphor, "the wolf in sheep's
clothing", i.e., once you start talking, even in first-order
language, about powersets of infinite sets, you are ALREADY
DOING something fundamentally 2nd-order. You
already have (if you believe such beasts exist at all) models
where the powersets Really Are "full", as standard 2nd-
order semantics requires them to be. Unfortunately, because
of the Lowenheim-Skolem theorem, you also have lesser models
(interpreting "all" as less than what you naturally/naively
mean by it, but still consistently). But since every semantics
other than the full/standard one is necessarily sparser, the
question always arises, is it SO sparse that you could've
achieved the same thing in first-order model theory? In the
case of the Henkin semantics, the answer is yes, and that is
one of the more FAMOUS alternatives. To the extent that other
alternatives are also simulatable at first-order, they are
similarly irrelevant, if 2nd-order logic is what we want to
talk about.

> >> Hence, so interpreted, second-order PA has nonstandard models.
> >
> > So where do they live?
>
> Same place the nonstandard models of first-order PA live. :-)

Not really.
To get what you call non-standard models of 2nd-order PA,
you have to use a non-standard semantics for 2nd-order
logic. But the non-standard models for 1st-order PA occur
in the STANDARD semantics of 1st-order logic. The standard
model of FIRST-order PA is NOT special, from the exterior
viewpoint of the logic. The standard model of
2nd-order PA IS special: it is (up to isomorphism) the ONLY
model you can have with the standard semantics OF THE LOGIC,
as a whole. The situation at first order is DIFFERENT.

.

Relevant Pages

  • Re: what follows from denying an axiom
    ... Second-order languages have a generalized model theory (from ... The Henkin semantics IS NOT SECOND-ORDER ANYTHING ... It is an issue if indeed I am making false or confused claims because I ...
    (sci.logic)
  • Re: Is C99 the final C? (some suggestions)
    ... This would violate the division between preprocessor and compiler too ... much (the preprocessor would have to understand quite a lot of C semantics). ... ...This is legal C (as per the Standard), but it overflows the stack on ...
    (comp.lang.c)
  • Re: Countable models of ZFC
    ... When I say "M is a set", I don't mean it's a set living in some model, ... If so, WHAT IS THE DEFINITION (of standard, ... the WHOLE of first-order semantics with it. ... you'd best at LEAST concede that M was a proper class. ...
    (sci.logic)
  • Re: what follows from denying an axiom
    ... to do with SECOND-order ANYthing, ... is just to make things more tractable BY DESCENDING TO FIRST-order. ... second-order language as a many-sorted first-order language. ... That is, for a sentence σ to be valid in the general semantics, it must ...
    (sci.logic)
  • Re: what follows from denying an axiom
    ... Chris Menzel is the first person I have ever heard say "second-order ... Reasoning was never an issue in my response to Daryl. ... language purely syntactically. ... Formal system has no semantics. ...
    (sci.logic)