![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
Difference between revision 9 and current revision
No diff available.companies:
Some less popular (?) ones:
Common Logic is an offshoot/successor to KIF.
IKL is an extension to/successor of Common Logic.
"IKL is a variant of the CLIF dialect of ISO Common Logic [CL], extended with terms which denote propositions and a device for relating names to the character strings which are used to indicate them...IKL achieves its unique expressiveness from its ability to quantify over the propositions expressed by its own sentences, which in effect allows it to be its own meta-language, so it can bring the full expressive power of logic to the task of talking about propositions as well as simply expressing propositions by sentences. This single device can replace a wide variety of 'alternative' logics, including modal, context, temporal and indexical logics, by various ontologies all written in a single logical framework, which facilitates interoperation.." (most quotes here are from the Guide, linked below)
A big principal of IKL is that "when IKL expressions are transmitted across a network or archived for later use, their meaning should be the same at the point of use as it was at the point of origin". Similarly, IKL is transparent (the referent of a name is context-independent, eg you do not have terms like 12 which can mean one thing if you are in a decimal context and another when you are in a binary context; when context-dependent mappings are desired, quoted name conventions should be used), panoptic (all quantifiers range over a single all-encompassing universe of discourse; if you want context-dependent restrictions, include them explicitly), and is not indexical (no words whose meaning changes like here, now, you; you're supposed to use terms from some objective global reference framework instead (my comment: this sounds rather infeasible/impossible; eg if you say "now", sure we can translate that into UTC time, but what if you don't know about UTC time? what if you are referring to a time point, not a time segment, but you dont have enough precision to know which point it is? what about relativity, etc, what if other stuff like that is discovered later, what if we discover reachable 'alternate possible worlds' etc; ok we could try to replace now with 'the instant at which the author of this sentence wrote it', but what if there are multiple authors/editors/versions, etc; this is sort of the ultimate 'modernist' language, which i bet will turn out to be formally provably impossible or at least provably infeasible given a constantly threat of an expanding worldview in the future))
IKL is unsegregated and unsorted (untyped; "there is no logical distinction in IKL between classes and individuals, or between relations and particulars: relations and classes are first-class entities which may themselves be in classes, take part in relations, and so on, with perfect freedom, and one can write axioms which quantify over them, so can speak of a class of classes, and write axioms about all the classes in a certain class of classes, etc.. Although IKL is a first-order logic, the resulting syntactic freedom allows for a great deal of expressive improvement over a conventional first-order syntax."; i don't really understand the distinction between unsegregated and unsorted, they seem the same to me).
How can IKL be a 'first-order logic' if you can quantify over relations, propositions, etc? Here's what the Guide says: "Common Logic has been characterized as "higher-order syntax with a first-order semantics"" and "The quantifier (forall (r... in this example above can be read intuitively as saying 'for all relations'; but 'all' here means only 'all relations which are in the universe', which can be a much smaller set than all mathematically definable relations. Unlike higher-order logics, IKL does not have any comprehension principles built into it which would guarantee the existence of functions or relations (other than propositions): this is what keeps IKL a genuine first-order language. In general, such 'higher-order' quantifications in IKL should be understood as applying only to functions or relations which are indicated by expressions which can be built from the axioms themselves. For normal purposes of expressing real-world knowledge, this is not a real limitation; it becomes an issue only when using the logic to express theorems in higher mathematics.".
I guess i must still not understand the definition of a second-order logic, because i thought it had to do with having higher-order quantification at all, not with whether certain entities exist in your domain? I guess the idea is that it's not really a second-order logic if the domain doesn't really include all of the possible relations etc of the first-order domain. So does that mean that if you have the ten digits 0-9 in your domain, then a logic which can quantify over all finite sets of these digits, or even over all computable sets, is not a second-order logic, but rather only a first-order one? I'm not sure, but if that's right, then i guess to me that makes it pretty attractive to me (i guess i may be some sort of 'reductionist' (weak finitist/quasi-finitist/pseudo-finitist, might be a better term) as defined in [3]), and i guess i like ideas like a 'relativized' (Feferman) or 'extended' (Godel, according to that link) or 'generalized' (Bernays/Sieg, according to that link) Hilbert's Programme; see also Feferman's Explicit Mathematics; see also [4]). Otoh [5] claims an important connection between second-order logics and computational complexity, in which case maybe i wouldn't want to throw it away just yet (and i bet some of the relativized/extended/generalized Hilbert's Programmes would allow at least enough second-order logic for this sort of thing... i wonder if IKL does? the more i get into transfinite stuff the more i think that the diversity of opinion, the plethora of paradoxes, and the ease of doing without it almost all of the time, demonstrates that one of these weakened Hilbert's Programmes is probably the way to go).
IKL connectives:
IKL quantifiers:
IKL functions:
IKL classes:
examples:
"any two distinct names in a certain set Base of names must denote distinct entities": (forall ((x charseq)(y charseq)) (if (and (Base x)(Base y)(not (= x y))) (not (= (tnb x)(tnb y))) )
"The only 'formatting' characters used in IKL syntax are the parentheses and whitespace, although the single and double quote marks, the backslash character, and the ellipsis (three consecutive dots) all play lexical roles."
Links:
See also:
