Numerical quantifiers

[fabianneuhaus]

I would like to work on this issue next. I assume that by these "numerical quantifiers" we don't mean just quantifiers of the form (exists 2 (x) (dog x)) where the number position has to be filled by a specific numerical because this can be treated just as syntactic sugar for (exists (x y) (and (dog x) (dog y) (not (= x y))))

What we are talking about are quantifiers like (forall (n integer) (exists n (dog x)) that are not expressible in FOL.

I see two issues. One minor issue is that this is yet another way that CL will go beyond classical FOL. Of course, there is nothing sacrosanct about classical FOL, but it has the advantage of being well studied, and I think we should add extensions to the language very carefully.

The other issue has to do with making numeric quantification work in the context of restricted domains (aka modules). I discussed this and (provided an example) in http://common-logic.1085828.n5.nabble.com/Definitional-extensions-in-CLIF-are-not-conservative-tp2457p2559.html

One straight forward way to address the issue is (a) change the notion of CL interpretation by adding a special predicate (e.g., cl:Integer), which has a fixed interpretation, namely the set of integers. (b) allow for special quantifiers that do not quantify over the extension of cl:Integer regardless of whether the integers are in the local domain of discourse.

One could generalize this approach to other datatypes, and introduce like OWL data type maps to include all kinds of datatypes. Of course, the difference would be that in CL the quantifiers would range over "normal" entities as well as datatype entities -- unless one explicitly restricts the domain of quantification explicitly to "normal" entities. Providing this ability might make it easier to integrate OWL ontologies in CL. Also, I always thought that it is arbitrary that CL recognizes positive integers, but not negative integers or real numbers.

This should not be too hard to do. But I'd like your comments before I try it.

[whitten]

fabian, perhaps I'm missing something here, but I understood the use of the structured elipsis i.e. using ...Name allows for infinite recursion and the syntax you mention: (forall (n integer) (exists n (dog x)) is a special case of that since negative values of n are not really intended. To my knowledge, Common Logic was intending to address numeric identifiers but handle numbers as numeric values, math, etc, in an extension, not in the core Common Logic. I certainly think the ability of Common Logic to have variables that range over the entire Universe of Discourse should not be broken in the attempt make it more powerful.

David

[CL-mailing-list]

David, I apologize, my example was corrupt, which probably lead to some confusion. I meant to write (forall (n integer) (exists n (x) (dog x)))

If these quantifiers are a special case of sequence markers, how do you define them with sequence markers? Best Fabian

On Feb 26, 2013, at 4:22 PM, David Whitten wrote:

fabian, perhaps I'm missing something here, but I understood the use of the structured elipsis i.e. using ...Name allows for infinite recursion and the syntax you mention: (forall (n integer) (exists n (dog x)) is a special case of that since negative values of n are not really intended. To my knowledge, Common Logic was intending to address numeric identifiers but handle numbers as numeric values, math, etc, in an extension, not in the core Common Logic. I certainly think the ability of Common Logic to have variables that range over the entire Universe of Discourse should not be broken in the attempt make it more powerful.

David

— Reply to this email directly or view it on GitHub.

---

CL mailing list CL@philebus.tamu.edu http://philebus.tamu.edu/cgi-bin/mailman/listinfo/cl

[CL-mailing-list]

On Feb 26, 2013, at 10:03 PM, John F Sowa sowa@bestweb.net wrote:

On 2/26/2013 2:12 PM, fabianneuhaus wrote:

What we are talking about are quantifiers like (forall (n integer) (exists n (dog x)) that are not expressible in FOL.

This is another issue that would be solved by adding an annex with something along the lines of the Z mathematical toolkit.

Well, a little more generally put, instead of moving to a higher-order logic you could add some additional first-order axioms for sets and numbers (or, if you add enough set theory, just sets).

The base CL semantics would not change. The annex would contain an ontology for integers, countable sets, and sequences.

Countability isn't first-order. You just have to let in whatever sets are consistent with your axioms, and if they're first-order, you can't rule out sets of any size. Of course, if you leave out the power set axiom then there's no proving there are uncountable sets, and if you leave out infinity, there's no proving there are even denumerable sets.

Also, I don't see where sequences enter the picture here.

Then the English sentence "There are n dogs" would map to the following CLIF:

(exists ((s Set) (n Integer)) (and (= n (Count s)) (forall (x) (if (in x s) (Dog x)) ))

"Count", of course, is the cardinality operator. You could axiomatize it for finite sets it á la Frege:

(iff (= (Count s) 0) (not (exists (x) (in x s)))) (iff (= (Count s) (+ n 1)) (exists (x) (and (in x s) (= (Count (\ s (setof x))) n)))

where \ is the "subtraction" operator on sets and (setof ...) yields the set {...}.

-chris

[CL-mailing-list]

On Feb 27, 2013, at 12:07 AM, John F Sowa sowa@bestweb.net wrote:

On 2/26/2013 11:30 PM, Christopher Menzel wrote:

This is another issue that would be solved by adding an annex with something along the lines of the Z mathematical toolkit.

Well, a little more generally put, instead of moving to a higher-order logic you could add some additional first-order axioms for sets and numbers (or, if you add enough set theory, just sets).

I completely agree with the principle.

I was just suggesting where to put the definitions. I believe they should go in an annex, not in the main body of the standard.

I'm not sure it matters much where they go so long as there is — somewhere — a clear delineation between basic first-order CL and various supersized CLs you get by adding stuff that renders it semantically incomplete or negation incomplete — seq vars, number/set theory, higher-order quantifiers, etc.

-chris

[CL-mailing-list]

On Feb 27, 2013, at 9:21 AM, John F Sowa sowa@bestweb.net wrote:

On 2/27/2013 9:18 AM, Christopher Menzel wrote:

I'm not sure it matters much where they go so long as there is — somewhere — a clear delineation between basic first-order CL and various supersized CLs you get by adding stuff that renders it semantically incomplete or negation incomplete — seq vars, number/set theory, higher-order quantifiers, etc.

1. Chris noted that if the set theory is sufficiently rich, it could support arithmetic as well. However, many prominent mathematicians (Kronecker, Peirce, Brouwer, and Lesniewski, for example) claimed that no version of set theory is as well established as arithmetic

Ancients, all of them, vis-á-vis modern set theory. Set theory didn't even exist as such in the time of Kronecker (he died four years before Cantor's Beiträge was published) and Peirce was almost 70 when Zermelo published his first axiomatization in 1908). Even Lesniewski died before the end of WWII.

and that it would be better to define basic arithmetic without requiring set theory as a foundation.

That's a different point. I obviously agree that it would be silly to introduce set theory only for the purpose of having arithmetic at one's disposal. But it would be nearly as silly to introduce number theory separately if one had enough set theory to derive it.

1. I admit that set theory has progressed much further during the past century, but there are many respectable mathematicians who prefer other foundations, such as category theory

True.

or some version of metrology.

I take it you meant "mereology". If so, name one mathematician who prefers it as a foundation. I can think of a couple of Sobocinski students, but that's about it. :-)

For these reasons, I believe that the standard should have a clearly defined core with modular extensions. The criteria for conformance would be defined in terms of the choice of modules.

The question of whether to publish the modules in the body of the

standard or some normative annexes is less important. One option would be to put the definitions of all the modules in the body. Then there could be a normative annex that defines a recommended selection of modules to support sets, sequences, and arithmetic.

Sounds pretty good to me.

-chris

ps: Why are you not cc'ing to the github.com address as well?