Re: Turing completeness of the functional paradigm?

On Mon, 18 Jul 2005 23:32:19 +0100, Robert Low <mtx014@xxxxxxxxxxxxxx> said:
> Chris Menzel wrote:
>> On Mon, 18 Jul 2005 17:42:09 +0100, Robert Low <mtx014@xxxxxxxxxxxxxx> said:
>>>By 'formalism' do you mean 'first order'? Because there are certainly
>>>sets of axioms which uniquely define the natural numbers: the second
>>>order Peano axioms do this.
>> Assuming, of course, a standard model theory for second-order languages.
>> 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.
>
> Nope, I wasn't even aware of my ignorance in this regard :-(

See Herb Enderton's text, Ch 4, IIRC.

>> Hence, so interpreted, second-order PA has nonstandard models.
>
> So where do they live?

Same place the nonstandard models of first-order PA live. :-)

> I was under the impression that the (second order) PA axioms were
> categoric, which meant that there was essentially only one model.

They are categorical *relative to standard second-order model theory*.
Standard model theory for a second-order language L requires that the
(1-place) predicate quantifiers of L range over the entire power set of
the domain of a given model. (Generalize appropriately for n-place pred
quantifiers.) General model theory requires only that they range over a
*subset* of the power set of the domain; you only need to ensure that,
roughly, all the *expressible* subsets are present and accounted for.
Where it's PA we're talking about, this requires only countably many of
the uncountably many subsets of one's domain ("properties" of natural
numbers) to be quantified over in a model. This is the loophole that
lets nonstandard models back in.

> I can't see any other way for the inductive axiom (any set containing
> zero and closed under successor is the whole of N) not to give
> uniqueness

That's where the condition requiring all the expressible subsets comes
in.

> except that 'any set' doesn't mean what I think it ought to.

That's certainly one way to frame the issue. Alternatively (preferably,
by my all-too-dim lights), first-order logic just isn't powerful enough
to fully nail down what you know 'any set' means!

>> You also need to make an assumption about the background model theory
>> relative to which you are defining what it is for a theory to define
>> a certain class.
>
> I'm sure I was taking that for granted; I didn't even realise I had
> any choice in the matter...

Highly recommended reading: Stewart Shapiro, Foundations Without
Foundationalism: A Case For Second-Order Logic. Oxford University Press,
Oxford, 1991.

Chris Menzel

.

Relevant Pages

  • Re: For All x
    ... in the sense of model theory need not be the universal ... here is a model of the above axioms: ... At the object level,with the definition of R as proposed, ... object language, and neither does the notation. ...
    (sci.logic)
  • Re: FOL Compactness Theorem
    ... order axioms. ... If for every finite subset To of T there is a model of ... all the axioms in To, then there is a single model of all the axioms ... Hodges, Model Theory, Cambridge University Press. ...
    (sci.logic)
  • Re: FOL Compactness Theorem
    ... order axioms. ... If for every finite subset To of T there is a model of ... all the axioms in To, then there is a single model of all the axioms ... Hodges, Model Theory, Cambridge University Press. ...
    (sci.logic)
  • Re: Models and consistency
    ... Not the axioms of ZF alone. ... L is a universe for a model. ... Are you using NBG for your model theory then? ... What books and what sections in them are getting your notions from? ...
    (sci.logic)