[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
>> 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
>> are subjective except with resepct to a system of being the demand for proof
>> consistency of proof is an extension of the requirements for proof as
>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
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
This implies that A is false. Thus although it is not possible to
prove A true it is possible to prove it false.