On Jan 18, 2010, at 10:37 PM, John F. Sowa wrote: (01)
> Chris,
>
> All I was trying to say is what you have just affirmed:
>
> CM> If you simply mean a *list*, then obviously no infinite set can
>> be specified extensionally; but that's not very interesting.
>
> I agree. But Pat seemed to object. (02)
I did not object to this, which is obvious. (03)
>
> CM> For instance, the following specifies the set ω of finite
>> von Neumann ordinals in ZF set theory:
>>
>> ω = the smallest set x containing ∅ and such that,
>> if y∈x, then y∪{y}∈x.
>
> That is what I was calling a specification by a finite statement
> of some rule or axiom for determining the elements of the set. (04)
This does not specify what the elements are of the *smallest* set
satisfying the conditions are. Chris' description does not give any
way to determine the elements of that set, it only describes
conditions on the set itself, of the form: if this is in it, then this
other thing must be. (05)
> But Pat seemed to object.
>
> JFS>> Grammar rules:
>>>
>>> N -> 0
>>> N -> S N
>>>
>>> This is a finite specification that generates a denoting expression
>>> for all and only the natural numbers. You can add a few Peano-style
>>> axioms to get the standard model without the weird number-like
>>> things
>>> of the non-standard models.
>
> CM> If one were to formalize the grammar above as a first-order
> theory,
>> even an infinite, undecidable theory (which of course wouldn't be
>> much
>> of a theory), there would be no way to rule out nonstandard
>> interpretations of the constant "N".
>
> I agree. But I did *not* formalize it in FOL. What I did was to
> *formalize* it as a grammar. A formal grammar is just as formal as
> any statement in any version of logic. But nobody talks about
> nonstandard models of a grammar. (06)
They could, and some do. The grammar is a set of assertions, and these
assertions have non-standard models, AKA non-minimal fixpoints. For
example, your grammar can be satisfied by the minimal interpretation N
= {0, s0, ss0, sss0, ...}, which you have in mind; but also by an
infinite number of non-standard solutions, such as the 'transfinite'
solution {0, s0, ss0, sss0, ...., A, sA, ssA, sssA, ...} or the
'intermediate-point' solution {0, H, s0, sH, ss0, ssH, sss0,
sssH, ...}, etc.. What rules out these interpretations? You cannot
actually generate all the numerals and check the total set in
extension. You rely on the same intuition that we rely on when we use
the numerals and arithmetic operators in the usual way, and believe
that we are talking about the standard model. (07)
> They talk about "all and only
> those sentences generated by the grammar." That last clause
> goes beyond ordinary FOL. (08)
Yes. And if they are speaking more exactly, they might refer to the
*smallest* set which satisfies the recursive equations, as Chris did.
This clause hides a rather powerful semantic assumption. If we
formalize this, it becomes the minimal fixedpoint operator, AKA the
Landin Y-combinator. And if you spell out the details of the resulting
formalism (lambda calculus) carefully, then there is a semantic
assumption built into it which itself cannot be finitely axiomatized.
Put another way, the lambda-calculus itself has nonstandard models.
There is just no way to escape this. The set of sentences true in the
standard model of arithmetic is not recursively enumerable, by any
finitely describable computational process of any kind. (09)
>
> CM> Seems to me clear that we "know" the standard model or we wouldn't
>> recognize the distinction between it and the nonstandard ones.
>
> Yes indeed. We recognize that difference very well because we know
> excellent formalizations of the standard model:
>
> The model of Peano's axioms that is limited to those numbers that
> are denoted by the numerals generated by the above grammar. (010)
Of course, if we allow ourselves to make recursive specifications
(like your grammar) AND insist that only minimal fixed-points are
allowed as models, then indeed we can 'capture' unaxiomatizable
things. But this begs the question, because recursive descriptions do
have other fixed-points, and the formalism itself isn't ruling those
out: your intuition is. We do this (ignore the nonstandard models)
routinely for grammars just as we do for arithmetic, but the semantic/
formal situation is the same in both cases. (011)
>
> The fact that something cannot be formalized in FOL, by itself,
> does not mean that it cannot be formally specified. (012)
Goedel's theorem shows that for any formalization of arithmetic (not
just one using FOL, but any) which can be finitely described as some
kind of computational process (eg by drawing conclusions from a
finitely generatable set of assumptions using a finite number of
rules), there will be a sentence which, under an appropriate encoding
of the system into arithmetic, asserts that it itself is not provable
in the formal system. This sentence is either provable (in the system)
or not. If it is, the system is inconsistent. If not, the sentence is
unprovable, and hence, ironically, true (since that is what it
asserts). So there is a truth of arithmetic that cannot be proved by
the system. Nothing here about FOL in particular. This applies to
*any* formalization, in *any* finitely describable formalism. (013)
Pat (014)
>
> John
>
>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/uom-ontology-std/
> Subscribe: mailto:uom-ontology-std-join@xxxxxxxxxxxxxxxx
> Config/Unsubscribe: http://ontolog.cim3.net/mailman/listinfo/uom-ontology-std/
> Shared Files: http://ontolog.cim3.net/file/work/UoM/
> Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?UoM_Ontology_Standard (015)
------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 mobile
phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes (016)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/uom-ontology-std/
Subscribe: mailto:uom-ontology-std-join@xxxxxxxxxxxxxxxx
Config/Unsubscribe: http://ontolog.cim3.net/mailman/listinfo/uom-ontology-std/
Shared Files: http://ontolog.cim3.net/file/work/UoM/
Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?UoM_Ontology_Standard (017)
|