Consistency of Theories of Ideas
Proceedings of the Sixth International Joint Conference on Artificial Intelligence. .
© 1979 International Joint Conferences on Artificial Intelligence
Abstract
Inconsistency Is a problem with first order predicate calculus theories In which Ideas are treated as objects. This paper presents general results on Inconsistency, Including an Interesting restriction on the relation of knowing. A theory having a uniform method of expressing Ideas, Ideas of ideas, and so on, is sketched. It Is shown how to restrict some of the axioms of this theory In order to obtain consistency. The method of obtaining consistency seems to have some generality.
- Lyndon, Roger C. (1966) Not1s on Logic, Van Nostrand, New York.
- McCarthy, J. and Hayes, P. J. (1969) Some Philosophical Problems from the Standpoint of Artificial Intelligence, In B. Meltzer and D. Michie (eds.) Machin1 lntelligtnce -#, i6S-502, Edinburgh: Edinburgh University Press.
- McCarthy, J. (1977) Epistemological Problems of Artificial lntelli~ence, 19'l'l1JCAI Proceedings.
- McCarthy, J. (1979) First Order Tlltorits of Individual Concepts and Propositions, Stanford AI Lab, AfM-S25.
- Moore, Robert C. (1977) Reasoning about Knowledge and Action, 19'l'l!JCAI Procudtngs.
- Moore, Robert C. (1979) Reasoning about Knowl1dg1 and Action, Ph.D. Dissertation, Comp.Sci.Dept., MIT.
References were extracted automatically from the PDF and may contain errors.
Full text extracted automatically from the PDF; figures, tables and equations may differ. The PDF is the version of record.
1. INTRODUCTION
As has been noted, for example, In [i], one of the problems with first order predicate calculus (PC) theories that objectify ideas Is Inconsistency. The next section describes a consistent theory that treats Ideas as objects. It describes the ax loms A X of this theory. Indicates the restrictions that make the theory consistent, brleny discusses the notion of constructive Idea, and then deals with some of the details of the formulation. After that, It Is shown how easily inconsistency can arise In such theories. Then there Is stated a theorem which says that in spite of these Inconsistency results the theory described here, along with a number of Its extensions, Is consistent
2. THE THEORY
The axiom system A X . of the theory states that everyone knows the axioms of logic and all that Is logically deducible from them. The axiom system also states that whatever anyone knows Is true, and that If one knows something then one knows that one knows lt. There are also axioms that state what It means for a variable to be (ret ln a string, as well as what It means for one string to be frtt !Jr a variable in another string (these standard concepts of Joglc are used in specifying the logical axioms in the PC).
Most Important for consistency considerations are the axioms that specify the relation of denotation. It Is desired that every (closed) string should dtnott its value, or In other words, that . the string should denote what It namts (examples of naming are given below). As will be seen In the section on Inconsistency, such a desire can easily lead to paradox. Instead we make the weaker assumption (axiom ai) that every (closed) determinate string denotes its value. (Determinate strings, defined In the next section, are a very general class of strings, yet they avoid paradox.) By thus weakening the assumption about denote, one can prove that any of a variety of extensions of the axiom system AX are consistent.
The final .axioms of the system state that whatever Is a logical consequence of any of these axioms and Is determinate, is known by everyone In all states (these last axioms are defined Inductively). I do not see that the determinate restriction In these final axioms is necessary, but I have not yet seen how to prove consistency without It At this point the notion of constructlvt can be brleny mentioned. One can optionally Introduce this notion Into the formulation (the consistency results below apply In either case). A constructive Idea, together with a fixed body of knowledge, allows a person to identify the object named by the idea. The notion Is related to the distinction between "being aware of" and "actually knowing". Thus the Idea "number-of-people-ln(room I)" makes one aware of a number without actually knowing what the number Is. A person may be able deduce facts about a number (without actually knowing the number), but one actually knows the number only after deducing that the idea denotes the same thing as a constructive idea. In the notation illustrated later,
3 U constructlve(U) "
K(p, ... (number-of-people-ln·(roomt·),U), s).
The notion of "can" is defined not only u knowing, but constructively knowing that an action will achieve a condition.
The remainder of this section sketches some of the details of the theory.
The language L of the theory Is a (first order PC) language with sorts. It contains a set of basic symbols, and these can be starrtd any number of times to produce new symbols. For example, the starred versions of, say, symbols "K ", "> ", or "g" are "K ··, "> ··. or ·s··, while the starred version of these are "K ···. "> ···, or ·s···; these are nine distinct symbols.
For purposes of explanation, Ideas are concretized as strings of L (the word "string· Is used to mean either a term or formula of L). There wlfl be no Indication of the sorts, although variables that range over strings are In upper case, variables ranging over variables are In gothic, and usually, but not necessarily, lower case is reserved for variables that range over objects other than Ideas.
For examples of the intended use of the symbols of L and of the notion of naming, consider, Strings 1-3 name Ted, 3, and safe1, res~lvely. On the other hand, 4-6 name the strings ,.eel., ·s·, and "saf'e1", respectively.

String 7 says that 5 is greater than 3, and therefore it names true (this Is a truth independent of states). Strings 8-9 name the strings ">(5,3t and "> ·(5·,3·t. respectively. Whether 10 names true or false depends on the value assigned to the variable x.
String 11 names the string ">(x,st. What 12 names depends on the value assi1nec1 to the variable X; If X Is assigned "6";7+3", or "y+6 , then 12 would name ">(6,3)", ">(r+S,3t, or ">(y+6,3t, respectively. The string IS names true since there Ia a number greater than 3, while 14 names the string "3 x >{x,3r. What 15 names de~nds on the value assigned to !-; If'!-were assigned "x", "y , or "1", then 15 would name "3 x >(x,S)", "3 y >(x,S)", or "3 1 >(x,S)", respectively.
One Important relation Is that of knowing. This relation has three arguments; the first argument Is a person, the second argument a string (of the sort that names a truth value), and the third argument a state. The Intended Interpretation Is that In the state the person knows that the string Is true. Thus, the first of
- K(Ted,> ·(5·,3·),statel)
says that In state 1 Ted knows that ">(5,3)" is true, or, that 5 is greater than 3; formula 17 says that In state I Ted knows that In state2 Ted knew (will know) that 5 Is greater than 3. Another special relation Is that for denotation, represented by the relation symbol "denote". Examples are,
- denote(3·,s)
- ( 19) denote(3·(x·,> ·(x·,o·)),TRUE).
The first says that the string "3" denotes 3, the second that the string "3 x >(x,O)" denotes true.
For the purpose of conveniently specifying axiom schemas, two mappings from strings to strings are defined: these mappings are not functions In the model. If B is a formula, (cl B) Indicates the closure of B,l.e., B with all Its free variables universally quantified. Thus,
A string will be said to be clos1d If It has no free variables; so If B Is closed, then (cl B) Is the same as B.
The mapping td replaces all symbols by their starred versions, changing quantifiers Into functions.

Another convention for specifying schemas Is that B and C are syntactic variables that range over strings; they are not variables of L
To Illustrate these conventions consider the axiom schema
(24) K(p,td(B),s) ;:, (cl B), where B Is any formula.
This says that whatever anyone knows Is true. By taking B as "3 x >(x,y)" or "3 sl recl(blockl,sl)", one gets two of the instances of this schema:
- K(p,3·(x·,> ·(x·,y·)),s);:, V y 3 x >(x,y)
(26) K(p,3·(s1·,red·(blockl· ,sl·)),s);:, 3 s1 recl(blockl,sl).
Some examples of the axioms and axiom schemas A X of the theory are
- (al) v u V p s [ K(p,;:,·(u,;:,·(v,u))s) 1
- (a2) V V W [ K(p,v;s)" K(p,;:,·(V,W),s);:, K(p,W,s) 1
- (aS) V !- V [ K(p,V ,s) ;:, K(p,v·(,.,V),s) ]
(a4)denote(td(B),B), for every closed determinate string B
(a5) V U x y [denote(U,x) Adenote(U,y) ;:, (x ·' y)l
Axiom a I states that In all states all people know that the string (S I ;:, (S2 ;:, S I)) is true for all formulas S I and S2. Axiom a2 states that in any state If someone knows S I and (S I ;:, S2), then In that state they know 52, where S I and 52 are any formulas.
Axiom schema a4 states that every closed determinate string denotes its value, while axiom a5 says that a string can denote at most one thing.
S. DETERMINATE STRINGS
We define d1tmntnat1 string Inductively as follows. A single variable or constant is determinate. The string F(x l, ... ,xn) Is determinate for any variables x l, ... ,xn and an1 function (or relation) symbol F othtr than "K · or "denote . If x l, ... ,xn are some of the free variables In a determinate string B(x l, ... ,xn), and If B I, ... ,Bn are determinate strings, then B(B I, ... ,Bn) Is determinate. If B Is determinate, then so are (V x B) and (3 x B). Finally, If B Is determinate, and if u,p,and s are variables (of the appropriate sort), then (denote(td(B),u)) and (K(p,td(B),s)) are determinate.
Notice that an' string that does not contain the symbols "K · or "denote" Is determinate (the string may contain starred symbols, Including K·· and "denote··. since these are distinct from "K · and "denote"). In general, a string is determinate If every first argument of a "denote" in the string, as well as every second argument of a "K · in the string, Is an td of some determinate string. Some examples of determinate strings are
- (e I) V x (x > y)
- (e2) Ted
- (e3) denote (Ted·,x)" K<f,> ·ix·,y·),s)
- (e4) 3 p K(p,denote·(Tecl ·,x ).s)
- (e5) denote(denote·(Ted··,x·),denote(W,y)).
Some examples of strings that are not determinate are
- (e6) K(p,> ·<x.y·).s)
- (e7) denote(V,x)
- (e8) denote(denote·(v·,x·),u).
4. INCONSISTENCY
The results In this section show how lnconsistenct considerations restrict both the ·denote· and the ·K relation. These results are fairly general because only the few conditions explicitly stated In this section will be used: the axioms In the other sections are not assumed. In the following, Sub(u,vw) and Tr(u) are formulas. For reference purposes, we list,
(sbl) Vu v wl w2(Sub(u,v,wl)ASub(u,v,w2)=>wl·'w2) (sb2)Sub(id(B),id(C(v)),id(C(id(B)))), for all strings B and C
(trl) Tr(id(B)) · (B · TRUE), for all closed formulas B (dn I) denote(id(B),B), for all closed formulas B
(k I) V p s (K(p,td(B),s) => cl(B)l for all formulas B
(k2) cl(B) => 3 p s K(p.td(B),s), for every formula B.
One may think of sb I and sb2 as saying that the formula Sub(u,v,w) expresses substitution; of trl as saying that the formula Tr(u) expresses truth; of k I as saying that whatever anyone knows Is true; of k2 as saying that whatever Is true is known In at least one state by at least one person; of dn I as being an unrestricted version of the "denote" relation·. (In the foflowing, when we say that one of these schemas Is provable or Is true, we mean that every Instance of It Is provable or is true.)
Theorem. Let A be a set of formulas. Suppose that there is a formula Sub(u,v,w) such that sbl and sb2 are provable from A. Furthermore, suppose either that dn I Is provable from A or that there Is a formula Tr(u) such that trl Is provable from A. Then A is Inconsistent.
This Is Tarskl's theorem (see for Instance pg 85 of (I)) converted to a sort system. One might rephrase this theorem by saying that If substitution Is definable In A, then one can allow neither the unrestricted version dn I of the denotation relation (cf. axiom ai) nor an unrestricted version tr I of the truth relation.
Inconsistency results also place restrictions on the relation of knowing.
Theorem. Let A be a set r;>f formulas. Suppose that Sub(u,v,w) is a formula such that sbl and sb2 are provable from A. Suppose also that kl and k2 are provable from A. Then A Is Inconsistent.
This theorem has an Interesting formulation In terms of models and never known truths.
Theorem. Let Sub(u,v,w) be a formula and let M be a model of sb l,sb2, and k I (i.e., sb I, sb2, and k I are true of M). Then in M, there Is a "never known truth·, which Is to say, there Is a formula C such that (cl C) is true of M and such that (Vp s ~K(p,td(C),s)) Is true of M. In other words, If in M substitution Is expressible, and If in M whatever anyone knows Is true, then there is a truth that no one in any state ever knows.
There are variations and generalizations of these four theorems. Instead of using substitution as given In sb I and sb2, one can use Peano axioms together with a certain relation betwen strings. There are likely many such variations. The last theorem can be generalized In a further direction: the set of never known truths In M is Infinite In number, and cannot be ·delimited In certain ways·.
5. CONSISTENCY
On account of the previous lnconsistency,results, the consideration of consistency Is an important one. Let S be a set of formulas that satisfies either cl or c2.
(c I) S is consistent, and no part of any formula In S refers to an Idea, which is to say, S speaks only of objects that are not ideas.
(c2) No formula In S contains the symbols ·denote· or "K· (though they may contain such symbols as "denote·· and "K ··), and there Is a model of S (I.e., a structure In which all the formulas of S are true) such that the ideas In the model are the strings of L, and such that the connection between the starred symbols and the model Is as Illustrated by the explanations of examples 1-15.
Theorem. The union of S together with the axioms AX of the theory described earlier Is consistent.
For example, the axioms AX together with the Peano axioms and axioms expressing a variety of string substitutions and relations Is consistent.
6. CONCLUSION
The axiom system AX was motivated by the desire to have a powerful set of axioms so that the consistency results would be stronger; no overall attention was paid to efficiency of proofs (6).
The results presented here are fairly general. The inconsistency results depend on few assumptions, and those could be modified in many ways. The proof of the consistency theorem Is more complicated. A model of the axioms Is created In an Infinite sequence of stages, with "denote" and "K · appropriately extended at each stage by what has a fixed value (is "determinate") no matter how the rest of the stages are completed. This method seems general, going beyond the particular theory above or Its formulation.
@inproceedings{ijcai1979p53,
title = {Consistency of Theories of Ideas},
author = {Elschlager, Bob},
booktitle = {Proceedings of the Sixth International Joint Conference on
Artificial Intelligence, {IJCAI-79}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Bruce G. Buchanan},
year = {1979},
month = {8},
url = {https://ijcai.org/proceedings/1979/53},
}
TY - CPAPER TI - Consistency of Theories of Ideas AU - Elschlager, Bob T2 - Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79 PB - International Joint Conferences on Artificial Intelligence PY - 1979 UR - https://ijcai.org/proceedings/1979/53 ER -Copied
Machine-readable versions of this paper, for tools and AI agents: