Information Technology Reference
In-Depth Information
(1) accept the proposed answer as correct, (2) reject it as incorrect, or (3) decide
that it is insufficient as a proof, i.e. that it contains gaps that need to be filled. In
the case of the proof shown in Fig.
18.2
, the agent (e.g., the overall supervisor
A
)
may decide that the diagram alone is not a proof and create a new subtask based
on it, asking for a proof that the division of the small squares can be made in all
cases of triangles, and also with ruler and compass (the condition imposed upon
the solution). Then, for each such request, a codelet would be added in the system
pool, and get involved in the proof-event as soon as an agent (prover) undertook
the requested task of formally proving that the pieces of the division do add up to
the large square.
Notice that agent
A
1
may be simultaneously supervising (i.e. acting as interpreter)
several possible divisions that have been proposed and are being checked by
various agents (provers) in various codelets (children of
). We have
conceived of the supervising role of
A
1
as including the duty of filtering some
purported solutions to subtasks as correct or not. However, in reality the final
evaluation of a proof and its acceptance as such is granted not by any single
member of the mathematical community, but by the community as a whole. Thus,
in a system like the one we envision here a final subtask should always be created
by
A
1
whenever a full proof of
PT
1
seems to have been successfully completed;
namely, the subtask that posts the proof and asks the interpretation agents to
“verify the correctness of this proof”.
Finally, consider the case that the same agent
A
1
finds two or more partitions of the
squares. Thus, a single codelet like
A
1
,
PT
1
A
1
,
PT
1
may report two or more solutions
to its supervising agent
A
(in a communication facilitated by the system), who
then posts an equal number of codelets in the pool, asking for the corresponding
verifications of the correctness of proofs.
2.
might instead be asked to come up with ideas of using other theorems
of geometry, already accepted as true by the community, so as to give a geo-
metrical proof of
PT
. Thus,
A
2
might post two (or more) tasks of the kind “use
Theorem
A
2
,
PT
2
in order to prove
PT
”. For a concrete example,
A
2
might create the
following two tasks: “Use the Intersecting Chords Theorem in order to prove PT”
and “Use the Socrates' Theorem in order to prove
PT
”. The former theorem was
first proved by Euclid in his
Elements
(Proposition 35 of Book III). It represents
the outcome of a proof-event that took place during the Hellenistic period, in
which Euclid, as an agent (prover), communicated it to interpreters. The name of
the latter theorem is due to the right isosceles triangle used by Socrates in Plato's
Meno (84c) in an argument communicated to a young slave, during a proof-event
of solving the problem of Duplication of the Square.
2
[
X
]
As in the previous case, each agent that is engaged with one of those subtasks
(i.e., engaged in the proof-event) will lead to the creation of a codelet. Proofs
2
The reason Socrates discusses a geometrical result in a philosophical text is in order to argue that
knowledge pre-exists in minds, and so all that is needed is a suitable “midwife” who will deliver
the knowledge to the consciousness of the mind.
Search WWH ::
Custom Search