Further Reduction of the General Incompleteness Principle

The basic problem is to generate theorems like the following 4 theorems
of metamathematics:

1. Godel's 1931 1st. Incompleteness Theorem based on Soundness and
Smullyan's Dual Form Theorem (difference not represented here)
2. Rosser's 1936 extension
3. Godel's 1931 1st. Incompleteness Theorem based on w-consistency

-~PRx |-P -> P
-~PRx, PRx |-P => ~|-~P
~PRITx (aA)|-P(A) => ~|-~(aA)P(A)

E.g. the top proof states that if the set of unprovable sentences is
not representable, then if every provable sentence is true then the
logic is incomplete.

(As in earlier post: -~PRx means the nontheorems are not r.e. (or not
representable). PRx means the theorems are r.e. (or representable).
~PRIT means relation "X does not prove Y" is r.e. (or
representable.))

Complete means ~|-P => |-~P. Now drop the x (all statements are of the
form Px P is r.e.) and let:

A = |- It is provable that
B = ~ Not
C = (aA) For all A
P = 0 empty string

and we have:

-~PR A => 0
-~PR , PR A =>BAB
~PRIT CA => BABC

and BA => AB for Complete as exact formalizations of G1-I & S1, R1 and
G1-B. Then consider:

[-] [+] [if] [then]
~PR - A 0
~PR PR A BAB
- ~PRIT CA BABC

Each proof (line) is 4 mutually incompatible conditions:

1. The relations under the [+] are representable.
2. The relations under the [-] are not representable.
3. If the [if] is true for any wff, then the [then] is true for the
same wff.
4. The logic is complete: BA => AB.

This 4 by 3 display gives the 3 proofs that express the theorems. How
do we extend it with more rows?

1. Develop a system (axioms, rules?) to generate these.
2. Generate others.
3. Manually solve other sets of Px and -Px wffs
4. Other relations besides PR, PRIT

C-B

.

Relevant Pages

  • Re: Goedel - interesting problem?
    ... >> with the set of axioms. ... Why is it wrong for Theorems to pop into my head when I hear ... enough to express arithmetic must have true theorems that can not be proven ... Godel's Incompleteness Theorem (actually there is more than one, ...
    (sci.logic)
  • Re: Presburger arithmetic proves godels incompleteness theorem wrong
    ... arithmetic proves godels incompleteness theorem wrong ... there any sufficiently powerful and consistent finitely axiomatizable ... both these theorems are proven wrong by Presburger arithmetic ... Presburger proved that his arithmatic was both consistent and decidable ...
    (sci.logic)
  • Re: Goedel - interesting problem?
    ... that explain Goedel's true statements as true theorems that cannot be ... Gödel's Incompleteness Theorem states that any formal system powerful ... Godel's Incompleteness Theorem (actually there is more than one, ... Theoremhood comes from axioms. ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... >PRA isn't strong enough to prove Goedel's theorems, ... According to Shankar's _ Mathematics, Machines, and Goedel's Proof _; ... ``Goedel's incompleteness theorem represents a significant landmark in ...
    (sci.math)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... >PRA isn't strong enough to prove Goedel's theorems, ... According to Shankar's _ Mathematics, Machines, and Goedel's Proof _; ... ``Goedel's incompleteness theorem represents a significant landmark in ...
    (sci.logic)