I had some further offline discussions on this thread, and I'd like
to discuss some comments and corrections suggested by Chris and Pat. (01)
The first is that I added a C to Shoenfield's official misspelling
of Schônfeld. Following is a copy of the discussion about axiom
schemata from my earlier note with the spelling correction: (02)
> I would also like to mention another way of relating the CL
> method of quantifying over relations to Russell's hierarchy of
> types. Please note that all of arithmetic can be formalized
> in FOL. One of the first textbooks to adopt that approach is
>
> Shoenfield, Joseph R. (1967) Mathematical Logic, Reading, MA:
> Addison-Wesley.
>
> What Shoenfield does (and most authors since then) is to replace
> the second-order axiom of induction with an axiom schema: a pattern
> for asserting a new FOL axiom for each relation to which induction
> is being applied. In effect, that provides a potentially infinite
> number of axioms, but in any proof, only a finite number are used.
>
> In Common Logic, it's not necessary to introduce an axiom schema
> because each statement that quantifies over relations covers all
> and only those relations in the current domain.
>
> This example shows how Common Logic is able to prove theorems
> that would typically require higher order logic, while preserving
> a first-order style of proof. You could take any proof for
> which Schoenfield (or anybody else) uses axiom schemata and
> replace each axiom schema with an ordinary CL statement. The
> two proofs would be line-by-line equivalent. (03)
Chris Menzel noted that this summary is too brief to explain all
the issues. In particular, Shoenfield stated his axiom schema
in terms of patterns of *formulas*, not just *relation names*. (04)
Following is what Shoenfield wrote on p. 204 (with some further
explanation in brackets and with his formula rewritten without
subscripts and with "for all x" instead of an upside-down A): (05)
> If A is a formula of [Peano's theory stated in first-order
> logic that contains a free variable x], then the formula
>
> A(0) & (For all x (A(x) -> A(S x))) -> A
>
> is called an _induction axiom_. The theory obtained from
> [Peano's axioms by omitting his second-order axiom] and
> adding all the induction axioms as new induction axioms as
> new nonlogical axioms is called _Peano Arithmetic_. (06)
This statement adds one new axiom for every possible formula A
that contains a free variable x. (That's a lot of formulas.) (07)
Chris pointed out that just replacing that infinity of formulas
with a single CLIF statement that has a quantifier ranging over
monadic relations is not sufficient: (08)
> (forall (A) (if (and ((A 0)
> (forall (x) (if (A x) (A (s x))))))
> (forall (x) (A x))) (09)
Chris's point is that this formula with Peano's other axioms
does not guarantee that a CL model would contain all the
relations you need for an application. (010)
A model for second-order logic with a hierarchy of infinities
would contain much more than you need. Russell's method would
give you uncountably many relations, but Shoenfield's schema
only provides countably many. Both are infinite, but a
countable number is much more manageable. (011)
Pat Hayes said that there is a very simple way to ensure that
a CL model contains those relations you need for any particular
application. For any relation R you want, just assert that R
exists and use the equivalence operator 'iff' to define it.
For example, (012)
> (exists (R) (forall x (iff (R x)(= (+ x 1)(+ 1 x))) )) (013)
For any application, this method allows you to define all
the relations you want in advance, and any CL model for a
theory with those definitions would contain those relations. (014)
But Chris said that Shoenfield's schema guarantees that you
would have all the relations you define in advance plus any
others that you might define in the future. For example,
some intermediate step of a proof might require a temporary
definition that is just used during that proof. (015)
To provide the full power of Shoenfield's schema, you would need
to quantify over all first order formulas. But CL only supports
the option of quantifying over functions and relations. To provide
that additional power, Chris suggested a "comprehension schema": (016)
> (exists (R) (forall (x) (iff (R x) φ)))), for arithmetical φ. (017)
where φ is an arbitrary formula in arithmetic. In effect, this
would permit any new relation to be defined as needed at any
time. But it would still add a countable number of axioms
to the theory -- the same ones as Shoenfield's schema. (018)
However, there is another way to eliminate the infinity of axioms:
the proposed IKL extension to Common Logic. That extension allows
quantified variables to range over any CL statement *and* to relate
the variables to the propositions they state. That would enable
any schema by Shoenfield to be translated directly to an IKL formula. (019)
The idea of extending the Common Logic with the IKL proposal has been
suggested for the next version of the CL standard, and this example
is another reason for doing so. (020)
In summary, you don't need the hierarchy of uncountable infinities
in order to define arithmetic, set theory, and similar systems.
The method of first-order axiom schemata supports them by adding
countably many axioms. The IKL extension to CL allows each schema
to be translated to a single IKL axiom. (021)
John (022)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (023)
|