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.
Except that it all starts with language and developes through set theory.
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.
And yet it is all based on observations at the initial set theoretic level.
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.
And indded, we are people which gives us some common context.
[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).]
I was taught 1+1=1 in boolean algebra.
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.
But in computers, we are living in a mathematically defined system (except for physical issues which have been suppressed to a very large extent by the design of statistically low error-rate systems) which follows very precisely the logic of its design. Thus proofs work since we are working in this well formed domain.
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.
More specifically, within the logic dictated by the hardware designed to assure that the system remains within the mathematical structure defined by its design. -- -> See: Info-Sec Heaven at URL http://all.net Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236