gruninger / Common-Logic

Documents for the developments of ISO 24707 Editiion 2 (Common Logic)
8 stars 3 forks source link

Inconsistency between Definitions 3.12 and 3.22 for "individual" and "term" #45

Open greenTara opened 11 years ago

greenTara commented 11 years ago

Section 3, page 4.

The current language is:

3.12 individual one element of the universe of discourse NOTE The universe of discourse is the set of all individuals.

3.22 term 〈Common Logic〉 expression which denotes an individual, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms

This is not consistent with the definition of interpretations in 6.2 where the universe of discourse may be a proper subset of the universe of reference.

Proposed: 3.22 term 〈Common Logic〉 expression which denotes an element of the universe of reference, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms

CL-mailing-list commented 11 years ago

On May 17, 2013, at 9:07 AM, Tara Athan notifications@github.com wrote:

Section 3, page 4.

The current language is:

3.12 individual one element of the universe of discourse

Seems to me this should read "an element of the universe of discourse". "one element…" has a reading that suggests there is one particular element of the UoD that is THE individual of that UoD.

NOTE The universe of discourse is the set of all individuals.

3.22 term 〈Common Logic〉expression which denotes an individual, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms

This is not consistent with the definition of interpretations in 6.2 where the universe of discourse may be a proper subset of the universe of reference.

Yes, if it is taken to imply that every name is a term. But the thing that gives rise to the inconsistency here is the first clause (" expression which denotes an individual" — and why is "Common Logic" inside angle brackets here?). If 3.22 is a formal definition (is it?), that clause shouldn't be there, since "term" is a purely syntactic notion. As it stands, the definition (if it is a definition) is mixing syntactic apples with semantic oranges. Also, despite the use of "recursively" above, the definition (if it is a definition) isn't really recursive, since it is using the notion "functional term" rather than simply "term" (and "functional term" isn't even introduced explicitly in this section).

Proposed: 3.22 term 〈Common Logic〉 expression which denotes an element of the universe of reference, consisting of either a name or, recursively, a function term applied to a sequence of arguments, which are themselves terms

I guess I don't understand why there is a disconnect between the definitions (if they are definitions) in §3 and those in §6. I mean, if 3.22 is really a definition (is it?), it should at least be extensionally equivalent to the definition of "term" given in 6.1.1.10, e.g.:

3.22 term A name or, recursively, (i) a term applied to a sequence of terms or sequence markers, or (ii) a term with an attached comment.

Of course, this requires that a definition of "sequence marker" be added to §3.

-chris

greenTara commented 11 years ago

Good points, Chris.

Repeating a definition in two places is not only a maintenance nightmare (as demonstrated here), but is not best practice in standards, in my experience. It would make sense to me if section 3 either a) only includes definitions that are not spelled out elsewhere, with some other terms defined in other sections (especially appendices) with a clear method of labeling so the definitions could be referenced from their points of use; b) includes all definitions, which are then referenced from elsewhere.

For example, the definition of "interpretation" in the section 3 could provide a definition of a model-theoretic interpretation in general, while a separate definition is stated, either in section 3 or section 6, of a Common Logic interpretation. Not every mention of "interpretation" in the standard is referring to a Common Logic interpretation.