Question on Rosser/Godel Theorems
From: Charlie-Boo (chvol_at_aol.com)
Date: 10/11/04
- Next message: Bill Modlin: "Re: Coextensive properties?"
- Previous message: Bill Modlin: "Coextensive properties?"
- Messages sorted by: [ date ] [ thread ]
Date: 11 Oct 2004 10:40:22 -0700
The goal being the formalization of Rosser's 1936 theorem (extending
Godel's theorem to apply to any consistent system) and its reduction
to as simple a form as possible, consider the following two programs A
and B (A1, B1 and B2 signify points in the programs):
A:
FOR every Proof X (coded as natural numbers)
IF X proves that A Loops THEN Halt [A1]
B:
FOR every Proof X (coded as natural numbers)
IF X proves that B Loops THEN Halt [B1]
IF X proves that B Halts THEN LOOP [B2]
Propositional variables A1, B1 and B2 state that the corresponding
points in the programs are reached. CONS states that our proof system
in consistent (provable and refutable are disjoint.) HALT(z) and
LOOP(z) are the propositions that z halts and z loops, respectively,
where z=A or B.
Now consider the following properties of A and B:
1. A1 = HALT(A)
2. A1 => |- LOOP(A)
3. HALT(B) => |- LOOP(B)
Explanation:
1: We reach point A1 in program A iff program A halts. That is
because we do halt if we reach point A1 and there is no other point in
program A where we halt.
2: We reach point A1 only if we can prove that program A loops. That
is because we must pass the IF X proves that A Loops test to reach
point A1.
3: Program B halts only if we reach point B1, which is reached only if
X proves that B Loops for some proof X.
Question: What other properties of A and B may we conclude?
C-B
(Note: A actually proves Smullyan's Dual Form theorem, not Godel's 1st
Theorem based on soundness, despite what popular texts say.)
- Next message: Bill Modlin: "Re: Coextensive properties?"
- Previous message: Bill Modlin: "Coextensive properties?"
- Messages sorted by: [ date ] [ thread ]
Relevant Pages
|
