|
|
Re: THE ANTITHESIS of GODEL'S INCOMPLETENESS THEOREM
Posted:
Nov 20, 2012 11:15 AM
|
|
On Nov 20, 12:13 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> DEFINE a 2 parameter predicate
> PROOF(THEOREM, DEDUCTIONSEQUENCE)
>
> proof( R , [R] ) <- axiom(R)
> proof( R , [R|DED] ) <- if(L,R) & proof( L , DED )
>
> where if(L,R) matches any inference rule in the formal system.
I like to say that the axioms are true statements and the rules map
true statements into new ones (incorporating soundness into the
definition and not generalizing by saying that truth doesn't matter.)
> This is equivalent to MODUS PONENS inference application rule.
>
> theorem(R) <- axiom(R)
> theorem(R) <- if(L,R) & theorem(L) #MP
>
> proof() remembers the deductions used by modus ponens in the argument
> sequence DED.
>
> ----------------------------
>
> [R|DED] - complete deduction sequence right up to theorem R, is a
> finite length string, all the terms are from a fixed alphabet or
> atleast countable.
>
> The HYPOTHESIS which opposes "G=!proof(G)" being significant for
> completeness is
>
> there exists some suitably rich set of axioms such that
> for every well formed formula F
> exist <t1,t2,t3,,,,F>
> or exist <t1,t2,t3,,,~F>
Let:
PR and DIS be the sets of provable and refutable sentence.
P,Q mean that P=Q
-W mean W is not true
TRUE be the universal set.
PR v DIS , TRUE The system is complete
- PR v DIS , TRUE The system is incomplete.
Let TS and FS be the sets of true and false English sentences.
- TS v FS , TRUE The Liar Paradox proves this surprising fact.
(Just apply Godel's proof using TS and FS rather than PR and DIS.)
P => Q is P , P^Q
All of the logic in CBL is represented and carried out using this
formalism.
C-B
> e.g [F | t4 | t3 | t2 | t1 ]
> where t1 and possibly other theorems in the sequence are axioms, i.e
> given as true.
>
> This would imply the existence of a halting theorem decider.
>
> G. COOPER (BINFTECH)
>
> --
> S: if stops(S) gosub S
> G. GREENE: this proves stops() must be un-computable!
> SCI.LOGIC
|
|
