Using Godel's PROOF(THEOREM) PREDICATE to Prove a Program HALTS() (in a separate THEORY)

[Graham Cooper]

www.tinyurl.com/GodelStatement

Godel's Proof began with the Hypothesis whether a PROOF(THEOREM)
Predicate existed or not.

This was defined as a function that input a theorem X and returned
TRUE
IFF a sequence of statements exists in the theory and the final line
is X, deduced from the earlier statements.

This is in fact programmable as a dual tail end recursive function
PRV(X) = X v (PRV(A) ^ PRV(B) ^ (A^B->C))

X has a PROOF IFF there is a (binary) directed acyclic graph of
theorems that deduce X

PRV() is similar to a RPN GRAMMAR PARSER.

By Using Reverse Polish Notation, MetaMath has a library of over 8000
Proofs.

e.g. a Proof in metamath is stored in Reverse Sequence of a directed
acyclic graph so each Theorem is derived from a Theorem before it in
the string.

(x(y+z)=xy+xz , 5(3+7)=50) , a^(a->c)->c) -> 5*3+5*7=50

This is how old calculators used to work.

[7] [,] [3] [+] -> 10

FORTH is a RPN Programming Language, the compilers down to Machine
Language are very small by using the Machine Language stack.

METAMATH = RPN + UNIFY()
PROLOG = LISP + UNIFY()

Similarly a Proof Function using the Predicate PRV() could be
programmed in PROLOG.

UNIFY() is a recursive algorithm that takes 2 formula and finds a
common formula by finding common arguments to the functions.

e.g. UNIFY( x(y+z)=x*y+x*z , 5(3+7)=50 )
-> 5*3+5*7=50

(without doing any arithmetic, just pattern matching)

------------------------

So, Godel appears to be WRONG that a PRV() Function is impossible.

The fact a PRV() Function is impossible, the main result of GODEL'S
PROOF took backseat to the INCOMPLETENESS THEOREM.

PRV(X) = X v (PRV(A) ^ PRV(B) ^ (A^B->X))
************
Next you'll need some Godel ordering of theorems, the simplest is a
lexicographical ordering using 10 logic symbols

ALPHABET = { 0 1 A ( , ) ^ v ! = }

LET A0() represent PRV()

Now you can define a Godel Statement in 2 lines.

A1= 11111010010101111001111 // 8203215
!A0(A1) // NOT(PROOF(8203215) *GODEL STATEMENT
=======
8203215 // GODEL NUMBER OF LINE 2 ABOVE

This is an actual Godel Number of an actual Godel Statement in this
Theory, by using a simpler Godel Number Formula Enumeration than
powers of primes that Godel defined.

Following is a generic formula for a Godel Statement using the same 2
line method as above.

- - - - - - - - - -
GODEL PROOF

GS-GN = CALC_GODEL_NUMBER("NOT(PRV(GS-GN))")
NOT(PRV(GS-GN)) **Godel Statement

T1|-!(PRV(GS-GN)) & T2|-PRV[ T1|-!(PRV(GS-GN)) ]

!PRV(GS-GN) is true in T1 and it's truth in T1
is proven in T2.

If every theory Tn has a statement that is true in that theory but not
provable in that theory...
The Incompleteness Theorem is:

ALL(T1) EXIST(T2)
T1|-!(PRV(GS-GN)) & T2|-PRV[ T1|-!(PRV(GS-GN)) ]
-> T1=/=T2

If a theory T1 has a statement GS !Prove(GS)
then it cannot be proven in that same theory.

A stronger version that G is in every theory.

A(T1)E(G)E(T2) T1=/=T2 & T1|-G & T2|-PRV( T1|-G )

Since T1=/=T2 T1 cannot prove it's own formula G!

-----------

But why is the STRONGER VERSION that a formula G exists in every
theory taken as an assumption?

Remember Godel failed to disprove a PROOF() PREDICATE was impossible.

By using a PROOF PREDICATE inside an AXIOM OF SPECIFICATION, you can
have a theory without GODEL STATEMENTS exactly how ZFC has a theory
without RUSSELS PARADOX.

The Axiom Of Provable Specification will not stratify either RS or GS.

-----------------

In APS set theory, which only has 1 axiom and a list of tautologies,
this is a fact:

NOT(EXIST(R)xeR<->x~ex)

Using that FACT, APS is an ALTERNATIVE METHOD to instantiate sets and
remain consistent.

Remember in both ZFC and APS, NST is barred!

NST
E(Y) Y = { x | P(x,Y) }
E(Y) Y = { x | x ~e x } --> CONTRADICTION

ZFC
E(Y) Y = { x | O(x,Y) ^ x e Z }
E(Y) Y = { x | x ~e x ^ x e Z } --> WILL NOT STRATIFY SINCE ~E(Z)

APS
E(Y) Y = { x | P{x,Y) } <-> ~Prv(~E(Y) Y = P(x,Y) }
E(Y) Y = { x | x ~e x } <-> ~Prv(~E(Y) xeY <-> x~ex )

BUT
~(E(R)xeR<->x~ex) is trivial to prove

so Prv(~E(Y) xeY <-> x~ex ) breaks the biconditional on the SET
SPECIFICATION

This is how Russells Set is avoided in APS.
Similarly Godel Statements will not stratify.

Which means only the Weak Incompleteness Theorem Holds

ALL(T1) EXIST(T2)
T1|-!(PRV(GS-GN)) & T2|-PRV[ T1|-!(PRV(GS-GN)) ]
-> T1=/=T2

i.e. not all Theories are required to instantiate Godel Statements

All theories using Axiom Of Provable Specification must not have a
proof that they can't exist.

-------------------

www.tinyurl.com/SetTheory2

So a Set Theory using PRV() is consistent, and possibly complete!

1 APS
Y = { x | P(x,Y) } <-> !PRV( !E(Y) Y = { x | P(x,Y) } )

2
PRV(THEOREM) <-> THEOREM v PRV(A)^PRV(B)^(A^B->THEOREM)

3
TAUTOLOGIES
-----------
A B C TYPE
a a->c c Modus Ponens
d->e e->f d->f Transitivity
!(!d) TRUE d Double Negation

4
THEOREMS
--------
THEOREMID A B THEOREM
1 0 0 X=X
2 1 1 (X=X) ^ (X=X)

5
ELEMENTS
--------
MEMBER SET
dave people
1 N
2 N
3 N
4 N

So we can add Induction to Tautologies in the form A^B->C

TAUTOLOGIES
-----------
A B C TYPE
a a->c c Modus Ponens
d->e e->f d->f Transitivity
!(!d) TRUE d Double Negation
P(0) P(n)->P(S(n)) P(n) Induction Formula

-----------

www.tinyurl.com/HaltFunction

The also "impossible" HALT() FUNCTION

T |- HALT(Prog1) = Prog1|-H1() ^ Prog1|-H2() ^ .. ^ Prog1|-Hn()

can be PROGRAMMED for the TEST PROGRAM and RUN in a TEST HARNESS!
VIS-A-VIS
TRUE IN ANY MINIMUM THEORY T AND PROVEN IN THE STANDARD MODEL

i.e. if there is no valid reason why formal proof theory is
incomplete, it should be possible to use Godel's PROOF(THEOREM)
PREDICATE to prove a program HALTS() (in a separate THEORY)

Graham Cooper (BInfTech)

[Don Stockbauer]

Why would you accept a proof from a person who starved himself to
death?