Re: Quibbling about definitions of "proof"

[hallam@w3.org]

>> 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