|
Perhaps the most striking of Llull's anticipations was the idea of
having a finite set of rules as well as a finite set of truths -"basic
concepts", axioms or whatever you call it-, so that you can then
generate from them a (presumably infinite) set of derived truths.
Nowadays we would describe the idea more simply, and say that Llull
had just come across the idea of a generative system. In linguistics
such a finitistic device is called a grammar (a set of rules to
manipulate strings from an alphabet beginning with some initial axioms)
and the generated strings are the language. In Computer Science the
device is called a machine and what is being generated is the set of
output configurations in a tape. As is well known today, the same
mechanism can run backwards: the same grammar that is capable of
generating a language is also capable of accepting or recognizing its
strings as belonging to it. Or the same machine which computes the
batch of acceptable results is also capable of recognizing a correct
calculation. (That those two dual processes are slightly asymmetric
in computational terms is a corollary of Gödel's first incompleteness
theorem and should not bother us here.) Llull was the first to notice
this reversible duality: in his terms, the same system that he
proposed to derive new truths from a reduced set (an abridged
"compendium" of them) and that he called "truth-finding procedure"
("art de trobar veritat" in Catalan or "ars inveniendi" in
Latin) and that in Logic we now call simply inference (or "forward
chaining") had a dual quality and could be executed in reverse, so
that we then have a recognizing or accepting system he called
"truth-proving procedure" ("art de demostrar", "ars
demonstrandi") and we name simply proof (or "backward chaining" or
"goal-oriented search" in AI). Thus, to Llull, if one were
confronted with proving some specific statement, one would have to
invent no new system: the one that allowed the user to explore new
truths would suffice to certify the intended truth, the certification
procedure itself being the proof.
|
|