On Thu, Apr 17, 2008 at 3:36 PM, Phillip Gawlowski
<cmdjackryan / googlemail.com> wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
>  Hash: SHA1
>
>  Eivind Eklund wrote:
>
>  |
>  | No.  A computer language is a different kind of beast; it is not a way
>  | to state truths about things, but a set of rules for mathematical
>  | operations.
>
>  Which makes it a complete logical system, though not necessarily in the
>  sense of abstract logic.
>
>
>  | I have no idea what you are trying to say here.  Could you reformulate?
>
>  Sure.
>
>
>  | Specifically, the following makes no sense to me:
>  |
>  | "In a complete system, any proof is valid" (this seems to depend on
>  | some weird definition of complete system)
>
>  Logically complete. That is, a system that implements abstract logic in
>  tis entirety. Abstract logic is at the root of Godel's incompleteness
>  theorem. Essentially, you either have something that can be expressed
>  with abstract logic. But that means, that there are things that cannot
>  be proven with abstract logic *within the logical system itself*.
>  Whence, an incompleteness theorem.
>
>
>  | "There are logical proofs that P is non-P" (this seems like either an
>  | example of a proof with subtle errors or proof-by-contradiction
>  | proving that a particular statement X is false; ie, if we can prove
>  | P!=P if we assume of X, then we know that X is false.)
>
>  1. P ¢ª Q        Premise
>  2. P ¢ª (Q ¢ª ¢ÌP)         Premise
De falsum quodlibet, nice try ;)
IOW You can prove anything with a wrong premise as false -> X is
always true indeed what you proved was
false -> (P && !P)
which is correct of course.
<snip>
>  Anyway: Computer languages that are Turing complete are both complete
>  and contradictory (since Godel's theorem exists), given a sufficient
>  algorithm. However, in >=90% of cases, this doesn't matter.
>
>
>  |
>  | If we knew we had a perfect spec and could practically prove all the
>  | relevant aspects of  transformation from spec to software/hardware, I
>  | guess we would be able to just say "Prove spec to software" instead of
>  | having any other standard.  Alas, to make software and hardware is a
>  | human endeavor - even assuming we could prove halting properties of
>  | our real world state machines on a perfect computer, this is only a
>  | small part of systems development.
>
>  Not really, thanks to Godel. If we can prove it, it's either incomplete
>  (so we don't have the perfect specs), or contradictory (so we don't have
>  the perfect specs either).
>
>  I hold the opinion that Godel's Incompleteness Axiom is a misnomer, and
>  it should be called Godel's Incompleteness Paradox.
Is it really called an axiom? An axiom cannot be proven, it should be
called a Theorem.

Cheers
Robert

>



-- 
http://ruby-smalltalk.blogspot.com/

---
Whereof one cannot speak, thereof one must be silent.
Ludwig Wittgenstein