Editorial, part 3
MECHANIZED DEDUCTION
Should it serve as a model for AI success?
There is a long way from Leibniz's arithmetical machine (the picture on the left) to the mechanized reasoning carried out by provers and checkers. The final success is due to physicalization of information as well as formalization and algebraization of logic.
In a germinal form, physicalization started with mechanical contrivances like those of Pascal and Leibniz, but the real physical flesh it needed did not appear until the era of electronics. Formalization germinated in the medieval notion of logical form, to be by Leibniz combined with Thomas Hobbes' idea that reasoning is like computing. However, the logical tools to implement that idea have not been invented until in our century.
A next step toward AI should consist in mechanizing conceptualization. The achievements in proving crucial theorems, like those of Cantor or Goedel, are due to surprisingly new ideas. Were such concepts mechanically produced, we would enjoy an artificial Cantor, artificial Goedel, etc. This test is a bit more difficult than Turing's; anyway, for AI enthusiasts there is nothing for it but to accept the challenge (even if more demanding than that narrated in S. Lem's "Trurl's Electronic Bard"). [*1]
This part of Editorial is to discuss a source of advances of mechanized deduction (Section 1) and put the question regarding possibilities of mechanized conceptualization (Section 2).
1. The source of success: physicalization and logical resolution
To examine the relationship between information in general and the physical stuff in which it materializes, we need terms to denote some portions of either of them. Let them be coined according to the following terminological proposal (which does not repeat any existing conventions but does not oppose them, either).
I shall speak of data as discrete physical records of information, for instance, symbols written down with pencil, configurations of electric impulses, of magnetized spots, etc. By the very fact of such recording, a continouous flow of information gets segmented, hence it is in order to speak of pieces of information assigned to respective data, for example the number zero assigned to the inscription "0". As shown in this example, information pieces belong to the domain of abstract objects (cf. item 1.3 in the survey "Mechanization of Reasoning").In arithmetical machines, pieces of information are numbers represented by physical states, be it configurations of cogs, be electric impulses, etc. Hence an indispensable way to physicalizing any thought consists in its arithmetization, that is, expressing it in numbers; for instance, in such conventional way as the numbering items of a vocabulary and then using numbers instead of words to express concepts.The other part of physicalization consists in constructing logical gates, ie, physical devices (mechanical, electric, etc) to realize logical functions such as negation, conjunction, disjunction. The possibility of mechanizing reasonings is due to the idea of logical function which evolved from a historical process, going back to medieval attempts at establishing algorithms which would mechanically yield valid inferences. Arguments of logical functions are like atoms in the universe of proof procedures, while specially devised rules make it possible to resolve any proof into such elementary constituents. The so obtained set of atoms has some physical properties which automatically decide whether a sequence of strings is a valid proof. [*2]
The process of resolution has the algorithmic, or mechanical character owing to the fixed order of steps which is determined by the structure of formulas occurring in the proofs. Here arises the interesting issue of the difference between humans and computers as far as the mode of reasoning is concerned. Theoretically, people can reason in the same way, that is, using the resolution algorithm. But they never do, and have serious reasons to proceed in their own way. The situation may be compared to the difference between programming in a machine code and that in a high level language. People can do the former too, and sometimes, if necessary, actually do, but the efficiency of this method when applied by humans is so low that in a long run it would stop any progress in programming. Anologously, had mathematicians reasoned with the resolution algorithm, this would have stopped mathematical progress.
The usual way of human reasoning was discovered already by Aristotle and described by him as the search for a middle term. To endorse this view, we just need to understand this expression in a broader sense, as the search for intermediary links between assumptions and conclusion, if the entailment is not obvious. The linking proposition should be such that it be obvious both that if follows from the assumptions and that the conclusion follows from it. How many such links should be looked for, depends on what kinds of following are regarded as obvious. In this respect there are notable differences between individuals, groups and cultures, as indicated by historians of mathematics. [*3]
Interestingly, such subjective differences can be simulated by automatic provers or checkers with varying degrees of obviousness. For instance, one checker accepts (ie "regards as obvious") the joint use of ponendo ponens and instantiation in a single step, while another one, instead, requires two separate steps.
Fortunately, in the first-order predicate calculus such differences in logical intuition do not harm the objective validity of logical rules since there holds equivalence between the method of resolution, as used by computers, and the method using classical inference rules, suitable for humans, as ponendo ponens, substitution, etc. This is a great success in that field of AI research that we have methods of mechanized proving and proof-checking and, moreover, enjoy the certainty that human and mechanical reasoners can assist each other in reasoning. Is it possible to repeat such a success in other cognitive activities, particularly in concept formation, or conceptualization?
2. A project of machine-oriented research in conceptualization
Some rudiments of conceptualization are not unfamiliar to robots, for example, they can learn class descriptions from samples. However, if machines are to assist humans in a way comparable to mechanized reasoning, much more is required. In particular, they have to see such connections as those appearing in the use of pictures and metaphors at the very start of creative scientific thinking (cf. footnote 1, at its end). Not less important is to perceive connections between various objects of the same domain.
To explain the latter, let us take advantage of some basic notions of Peano's arithmetic: "number", "zero", "sucessor", and "addition". In order to state, or even to understand, axiom 1 (that 0 is a number) one has to see a relation between 0 and the set of numbers; after he realized it, he understands both what 0 is, and what a number is, better than he did before realizing the connection. To proceed further in constructing the theory of arithmetic one must perceive the connection between the function of successor and that of addition (the former being a special case of the latter). Again, the understanding of the nexus increases the understanding of the nature of its members, though at some earlier level the latter was a prerequisite for the former (as is also the case in the previous example).
Thus we encounter a remarkable and very important cognitive feedback between understanding a whole and understanding its parts. This and some previous observations hint at what should be fed into a machine to make it capable of producing and using concepts, namely.
(1) A set of logical and ontological categories which are like tools for producing concepts of any kind whatever. Such are categories of class, membership, equality, equivalence relation, ordering relation; thing, property, fact, event, state, whole, part, etc.Items from the first list are those which are involved in defining connexions crucial for forming, developing, and understanding concepts. This is why such intellectual equippment is an important component of intelligence.
(2) Moreover, the machine should be equipped with a suitable knowledge concerning the domain in question, eg arithmetic, medicine, economics.However, before one properly defines a connection, one has to notice it. Such intellectual perceptiveness is an enormously important factor of intelligent conceptualization; it belongs to what in another place is called inventiveness. Its results should be critically assessed, and then imbedded into a system, but it is up to it to yield what is necessary to start with.
This is a substantial hint for an engineer who would build a conceptualizing machine. Besides a vast memory, it should possess an enormous ability of
scanning all the relevant items stored in the memory (like Trurl's electronic bard - cf. footnote 1 - who must have searched two enormous repertoires of words to match their erotic and mathematical meanings and, morever, to match sounds for rhyming). It can be easily noticed that the ability of rapid subconscious scanning is not evenly distributed among human minds. There must be a mechanism responsible for these variations; its examining should be involved in projects of constructing artificial minds. In fact, at least part of the problem reduces to such physical parameters as speed of signals and density of network connections. Optimalizing of these two factors should form a major task in cognitive engineering.
Productivity is a necessary but by no means sufficient condition of intelligence. It is not enough to produce a lot of inferences or a lot of concepts. The products should be somehow "good". Owing to formalization, we have methods of critical and precise assessing of deductive reasoning; it reduces to the mechanically testable validity, eg by applying resolution. Unfortunately, no such direct answer is available with regard to conceptualizations.
However, we can try an indirect way, even if less reliable, which leads to the goal via mechanization of reasoning. Again, the example of Peano arithmetic is to render services. We have grounds to believe that the concepts occurring in its axioms are cognitively good because we obtain an enormous set of consequences, and we did not find any inconsistency among them. Moreover, there exist consequences of a colossal cognitive value. It is the set of axioms which should be praised for these merits, and the same appraisal is due to the concepts involved. Thus we win a paradigm of indirect checking cognitive value of concepts. Such a paradigm is really functioning in physics and other empirical sciences, with the additional feature that among the conclusions deduced there are observational statements.
Do we need mechanized deduction for this purpose? Is it not enough to rely on the human art of deduction? This is a vast problem, not a one to be answered in a single short essay. A partial but well documented answer in the affirmative is found in a project of computerized organization of mathematical knowledge; this project, expressed in "QED Manifesto" - as vital for the modern Mathesis Universalis - is reprinted in this issue.
At the very last, it is in order to put a metaphysical question, that concerning possibility of artificial intelligence which would match, or even surpass, natural intelligence in reasoning and conceptualization. The answer is not without an impact on practical research, since it may influence the statement of goals, and - obviously - it is interesting by itself. Among varying answers there is one relatively little known to philosophers engaged in the AI questions, namely that suggested by Leibniz (in that stream of his thought which is represented by Monadology). An audience interested in these Leibniz's ideas will find them sketched in the last part of this Editorial.
Go to the top of this text
[*1] In: Stanislaw Lem, The Cyberiad, translated from Polish, Mandarin, London 1990. Trurl and Klapaucius, supeinteligent robots, are constructors of intelligent machines, eagerly competing with each other. When Trurl boasted of his new AI masterpiece, Klapaucius suggested the following task to test its talents."Let's have a love poem, lyrical, pastoral, and expressed in the language of pure mathematics. Tensor algebra mainly, with a little topology and higher calculus, if need be. But with feeling, you understand, and in the cybernetic spirit."The following poem, produced by the machine immediately after the constraints were stated, exemplifies a sophisticated manner of concept formation, namely that resorting to metaphors (why not to use mathematical ones to express machine's erotic phantasies?). Only if the art of metaphor is mastered by a machine, it can be said to match humans.Come, let us hasten to a higher plane,
Where dyads tread the fairy fields of Venn,
Their indices bedecked from one to n,
Commingled in an endless Markov chain!
Come, every frustum longs to be a cone,
And every vector dreams of matrices.
Hark to the gentle gradient of the breeze:
It whispers of a more ergodic zone.
In Riemann, Hilbert or in Banach space
Let superscripts and subscripts go their ways.
Our asymptotes no longer out of phase,
We shall encounter, counting, face to face.
I'll grant thee random access to my heart,
Thou'lt tell me all the constants of thy love;
And so we two shall all love's lemmas prove,
And in our bound partition never part.
For what did Cauchy know, or Christoffel,
Or Fourier, or any Boole or Euler,
Wielding thier compasses, their pens and rulers,
Of thy supernal sinusoidal spell?
Cancel me not---for what then shall remain?
Abscissas, some mantissas, modules, modes,
A root or two, a torus and a node:
The inverseof my verse, a null domain.
Ellipse of bliss, converge, O lips divine!
The product of our scalars is defined!
Cyberiad draws nigh, and the skew mind
Cuts capers like a happy haversine.
I see the eigenvalue in thine eye,
I hear the tender tensor in thy sigh.
Bernoulli would have been content to die,
Had he but known such ax cos 2 phi!Metaphors and pictures appear as sources of scientific concepts at first, most inventive, stages of creating a scientific theory. How, for instance, Niels Bohr was aware of that with regard to his atom model, s reported in a remembering by Werner Heisenberg. Bohr is said there to have stated the following.
We should clearly see that the language can be used here just like in a literary narrative which does not pretend to describe facts in an exact manner; it tries, instead, to produce pictures in the minds of audience and thereby to establish some connections between thoughts. (Werner Heisenberg, Der Teil und das Ganze. Gespraeche im Umkreis der Atomphysik. DTV, Muenchen 1993. Ch.3, p.14; ad hoc translation by this Editor.)In the quoted "poem", the remarkable humour arises out of using abstract terms as metaphors for sensual experiences instead of doing, as usual, the reverse. However, this stresses even the more the relation between creativity and seeing (from any end whatever) connections and analogies of various things or thoughts. [-> back to main text][*2] A conspicuous description of resolution procedure addressing beginners is found in Patrick Henry Winston's Artificial Intelligence, 2nd ed. Addison-Wesley, Reading (Mass.) etc 1984. The same subject in historical arrangement is discussed in W.Marciszewski and R.Murawski, Mechanization of Reasoning in a Historical Perspective". Editions Rodopi, Amsterdam 1995, in Sec. 7.3 (detailed description of its contents is found in this issue). [-> back to main text]
[*3] Cf. Raymond L. Wilder, Mathematics as a Cultural System. Pergamon Press, Oxford 1981. The following passage of this book (p.40) is concerned with historically changing standards of exactness. "It is ordinarily asserted that mathematical proof rests on logic. Ideally, this may be correct; actually it is generally incorrect. Analyze the general run of mathematical proof and it will be found to contain hidden assumptions [...] generally accepted in the contemporary mathematical culture. The classic example is that of Euclid, whose geometry was for centuries held up as the ideal example of rigorous proof. We know now that it contains geometric assumptions, unstated, that invalidate some of the proofs." This is a thought-provoking comment though it goes too far in its relativism; there were, indeed, some mistakes in Euclid, which were not detected until logic provided most reliable means for checking proofs, but owing to this logic such failures should not occur in the future. The problem is extensively discussed in this MU issue within a project of making mathematics secure up tu the highest degree as attainable in the era of mechanized reasoning; this is a claim of QED Manifesto. [-> back to main text]
File put on WWW server 17-02-96.