Re: Godel, Rosser and Turing in 1 Easy Step - and Why would we want to?

On Dec 23, 6:11�pm, Charlie-Boo <shymath...@xxxxxxxxx> wrote:
The results of Godel (1931, proof based on soundness), Rosser (1936)
and Turing (1937) boil down to the following 3 theorems:

1. If "x proves y" is expressible, then provability does not coincide
with truth.

2. If "x proves y" is representable, then provability does not
coincide with unrefutability.

3. If "x halts at iteration y" is r.e. (true), then the set of
programs that don't halt is not r.e.

Note that we now have formal specifications for these theorems. �This
is in contrast to published accounts which say that the requirement
(premise) of (1) and (2) is that "a certain amount of arithmetic can
be represented", a vague ("represented") and incomplete ("certain
amount") description that doesn't specify a theorem at all.

This is exact because it is extracted from the ultra-short formal
proofs generated by CBL. �The formal representations are:

PRIT / TW --> - PR , TW
PRIT / PR --> - PR , ~DIS
YIT / YES --> - ~(YES v NO) / YES

PRIT(a,b) : "a proves b"
TW(a,b) : Wff a with b substituted for its free variable is true.
PR(a,b) : Wff a with b substituted for its free variable is provable.
DIS(a,b) : Wff a with b substituted for its free variable is
refutable.
YES(a,b) : Turing Machine a halts yes on input b.
NO(a,b) : Turing Machine a halts no on input b.
- : statement negation
, : equivalence
v : or

Let us further distill these pillars of Mathematical Logic and
concentrate on the 3 premises:

Why would we believe that the following are true?

1. "x proves y" is expressible.
2. "x proves y" is representable.
3. "x halts at iteration y" is r.e.

I believe it is the same reason as why d/x (e^x) is (e^x): That's the
way it (e) was chosen. �In this case, what was chosen was the 6
relations PRIT, TW, PR, DIS, YES and NO. �I believe they represent
sets that have the above 3 properties, in some way. �But how?

I leave it to others.

C-B

What has truth to do with arithmetic and logic? Truth is empirically
determined, and neither of these disciplines employ a contingency in
their definitions.
.

Relevant Pages
Quantcast