ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] Type Systems for Common Logic

 To: "[ontolog-forum]" "John F. Sowa" Tue, 23 Aug 2011 11:48:58 -0400 <4E53CBEA.2040203@xxxxxxxxxxx>
 ```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) ```
 Current Thread [ontolog-forum] Type Systems for Common Logic, John F. Sowa Re: [ontolog-forum] Type Systems for Common Logic, Dr. Mohammad Reza Beik Zadeh Re: [ontolog-forum] Type Systems for Common Logic, John F. Sowa Re: [ontolog-forum] Type Systems for Common Logic, John F. Sowa Re: [ontolog-forum] Type Systems for Common Logic, John F. Sowa <=