-----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
~                3. P 	Assumption
~                4. Q 	1,3 MP
~                5. Q ¢ª ¢ÌP 	2,3 MP
~                6. ¬P 	4,5 MP
~                7. P & ¬P 	3,6 Conj
8. ¬P

Ergo: P = not-P. ;)

(Note: The character are UTF-8, in case you can't see them.)

The complete discussion of this proof:
http://www.iep.utm.edu/p/prop-log.htm#SH5e

Godel's first theorem:
"For any consistent formal, recursively enumerable theory that proves
basic arithmetical truths, an arithmetical statement that is true, but
not provable in the theory, can be constructed. That is, any effectively
generated theory capable of expressing elementary arithmetic cannot be
both consistent and complete."

Which drives logicians mad, since abstract logic has to be both complete
and non-contradictory. ;)

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.

- --
Phillip Gawlowski
Twitter: twitter.com/cynicalryan

Abstain from wine, women, and song; mostly song.
%Abstinence is as easy to me, as temperance would be difficult.
~ -- Samuel Johnson
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkgHUnAACgkQbtAgaoJTgL/phACeMJaxYkj54DGzqYcLTQNO5a3X
WgwAnjWRPr2Og+LrUGgmELEYUFDvJkJo
=sZ1C
-----END PGP SIGNATURE-----