[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Quibbling about definitions of "proof"
All this quibbling about the "validity" of proof checkers is philosophically
inept. It is a basic property of logic that it proceeds from axioms to
conclusions. No proposition can be understood except by reference to some
It is not possible to objectively observe anything, all observation is made
through a mechanism which is imperfectly analysed and thus the observation
is subjective to the extent that the interpretation is unknown.
We may obtain an objective statement from a subjective observation by reference
to the source of subjectivity. If however the subjective assumptions are shared
by all participants within the system of being any statement which follows from
only those assumptions may be regarded as objective. Objectivity is thus not
an atomic fact but a relation, a fact cannot have the property of objectivity
except with respect to a system of being.
[Thus I may assert 1+1=2 as an objective fact since the assumptions upon which
it is based are commonly shared. If however someone wished to question this
statement (e.g. phenomological bracketing) then in the context of that
discussion I would accept it as being subjective).]
The question of prooving the proof checker is thus an extension of a more
fundamental problem, providing proof of proof. Since a proof is a fact and facts
are subjective except with resepct to a system of being the demand for proof of
consistency of proof is an extension of the requirements for proof as normally
The requirement for "prooving" a program is thus significantly less onerous than
asserted. It is not necessary to provide a trancendental proof, merely to
establish consistency with respect to a commonly accepted set of axioms.