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 other proposition. 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 understood. 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. Phill Hallam-Baker