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.
That is not necessarily the case. It all starts with communication of which language is a form, logic is a more perfect form of communication because its validity is most widely shared. It is perfectly consistent to deny the supremacy opf logic. Wittgenstein was wrong to assert that it is impossible to step outside the logical framework. The mind may be characterised by logical inferences but that does not mean that it is bounded by logical inferences. The observer might take a hallucinatory drug for example and thereby participate in an extra-logical ontology.
And yet it is all based on observations at the initial set theoretic level.
Only if you accept that the logical positivists were right and that there is no thought that cannot be characterised in that manner. The problem with this approach is that it prevents consideration of the real issue which philosophy should consider, the questions of being, time and spirit. We might conisder that the logical positivists found and aswer to the wrong question while the continetal school found an unsatisfactory anwer to the right one.
And indded, we are people which gives us some common context.
Exactly we can communicate because we participate within the same system of being and that provides sufficient common reference points for us to convince ourselves that we are communicating the same ideas. We cannot prove that we are in fact achieiving this goal for we cannot objectively determine that we both observe the same things.
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.
But that mathematically defined system is still subject to the constraint that we cannot analyse the thing in itself. Instead we must step outside the system to analyse it. We do not in fact define LISP in LISP what we actually do is to define LISP in a language that looks like LISP and demonstrate that the two are compatible. It is important to distinguish a demonstration of meta-consistency from a proof within the logic of that logic. We might assert correctly that a program have been proven correct using a proof checker. We do not need to explain that the proof is of correctness with respect to a set of axioms for that is the nature of proof and is thus no more necessary when considering proofs of computer programs than of any other type of proofs. The meta-form of this proof is "A Therefore B where B is independent of A". We cannot however assert that we have used the program checker to prove itself. That would have a meta-form "A Therefore A". This form does not contain any information. The only meta form of A concerning A that carries information is "A Therefore (not A)". This implies that A is false. Thus although it is not possible to prove A true it is possible to prove it false. Phill Hallam-Baker