Assume the following: TR := the set of all total-recursive functions PR := the set of all partial-recursive functions S undecidable logic L_S the class of formulae in the language of S G G in PR and G:L_S->N (partial-recursive bijection from formulae in L_S to integers) Th(S) := {Phi: S |= Phi} (true formulae in L) GTh(S,G):= {G(Phi) : Phi in Th(S)} (the godel numbers of valid formula in S) Enum(p in TR, C) := the set of integers which are enumerated by the function p Len(p) := the number of symbols in the definition of p K(p in TR,C) := mu.len(q) (q in TR and Enum(q,U) = Enum(p,C)) (the size of the smallest recursive function that enumerates the same interger sequence as p) D(p,S,L_S,G,C) := {G(Phi): (Phi in L_S and G(Phi) in Enum(p,C) xor G(!Phi) in Enum(p,C))} Stronger(p,q) iff (subset-of Intersection(D(q,S,L_S,G,C),GTh(S,G)) Intersection(D(p,S,L_S,G,C),GTh(S,G))) Larger(p,q) iff (K(p,C) > K(q,C)) Then Also, (forall p in TR (not (exists q in TR (forall p in TR (and (exists q in TR (Larger(q,p)) (and (Stronger(q,p))))) (not Larger(q,p)) (Stronger(q,p)))))) # to be continued