SUO: Re: ontology as science
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Chris,
Mathematics is a practical human activity, and
proving theorems is a practical human activity.
The theorem provers that I trust are human beings,
that work in communities over periods of time, and
in such a way that they can check each other's work.
There are people that prove theorems, most of the time
redoing classical school figures and established results
as a means to the end of learning the subject matter, but
every now and then, by steadily retracing the old familiar
haunts and systematically pushing into every adjoining corner
of the available theorem space, it becomes possible to open up
whole new worlds of truth.
And then there are people who have theories about this
practical activity, and how it might be or ought to be
done, typically basing their theories on the syntactic
properties that a finished proof can be found to have,
as observed in what are largely very trivial cases.
But if you want to form a theory of how some practical
human activity is, or might, or ought to be done, say,
for the sake of automating the automatable portion of
that task, then it's the same standard advice with
motorizing math as any other software support job.
You have to study how it's really done, and not
keep insisting on some a prior theory of proof
that merely describes a formal, very partial
property of the target activity as a whole.
And that is one thing that I've learned.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o