Re: Contradiction or paradox

On May 25, 8:54 am, Charlie-Boo <shymath...@xxxxxxxxx> wrote:

You don't have any system at all, primtives or not. Your rules depend
on a vague stipulation as to presuming some other theorems regarding
computability that are not proven in your own system.

They are axioms. (In other systems they are theorems or definitions
DEF.)

Oh, so now your rules of interence depend on taking as axioms an
unspecified set of theorems proven in mathematics and computability. I
think you should name your system "Quiksand".

Moreover, Godel-Rosser can be proved in a language with just ONE non-
logical primitive predicate symbol (and the logical symbols can be as
spare as just one quantifier, just one connective, and a denumerable
set of variables) in a system that is ACTUALLY (as opposed to
pretending as you do) formalized so that there is a mechanical
procedure to check whether any given sequence of sequences of symbols
is a proof in the system.

You can't give a proof anywhere close to as short and simple as that
created by CBL. (PR=provable, DIS=refutable)

You don't know what a formal proof is.

Thm. DIS/PR => ( (PR =>~DIS) => ~PR(M) + ~DIS(M) )
"If refutability is representable then if the logic is consistent then
there is a sentence that is not provable and not refutable."
1. DIS/PR : Refutability is representable
2. PR => ~DIS : If Consistent
3. ~PR => DIS : If Complete
4. DIS => ~PR : Modus Tolens, Double Negative 2
5. ~PR , DIS : Then the provable sentences coincide with the
irrefutable ones 3,4
6. ~PR/PR : SUB 1,5
7. ~P/P : SUB 6
8. -~P/P : Incompleteness Axiom
9. False 7,8
qed

Therefore -~PR => DIS (the logic is incomplete) so (eM) ~PR(M) +
~DIS(M) i.e. there is a wff that is not provable and not refutable.

The strange thing is that all of the theorems (Godel, Rosser, Turing)
from Incompleteness in Logic (except those that relate only rules e.g.
w-consistent => consistent) have -~P/P at their root. I have yet to
figure out what the true formalization of the wff for Incompleteness
in Logic should be (despite having formalized all of the fundamental
theorems)!

Let me know when you figure out how to define the rules of inference
in your system without appeal to an unspecified set of theorems from
mathematics and computability.

And, no, I'm not going to post such a proof. That's a lot of work and
a lot of typing that is not necessary for me to perform.

No, it would be no longer than "If consistent and complete then the
unprovable sentences coincide with the refutable ones, but the latter
is r.e. while the former is not."

That's incorrect. You ignore that I've pointed out to you that if a
theory is consistent and complete, then the set of unprovable
sentences IS (you use the word 'coincide') the set of refutable
sentences, so it is impossible that the set of unprovable sentences be
recursively enumerable while the set of refutable sentences is not.

Just look in
ordinary textbooks in mathematical logic;

How big are the proofs given by Rosser (1936), Turing (1937) and
Smullyan (1990's)?

You need to stop for a minute counting how long proofs are and instead
start by finding out what proof IS.

if you see something that
can't be done in ZFC, then let me know about it.

Meanwhile, how's it going with your looking up that proof of "S and
its complement are recursively enumerable implies S is recursive" I
pointed out to you in Boolos et. al?

Which reminds me, Charlie-Boo, how is it going with your looking up
that proof of "S and its complement are recursively enumerable implies
S is recursive" I pointed out to you in Boolos et. al?

I mean, you ASKED me to show you such a proof. So now that I have, I'm
curious whether you even looked it up.

MoeBlee

.

Relevant Pages

  • Re: Contradiction or paradox
    ... on a vague stipulation as to presuming some other theorems regarding ... unspecified set of theorems proven in mathematics and computability. ... I pointed out that the first application of an inference rule in your ... nor even specified any certain formalization or even formal theory in ...
    (sci.logic)
  • Re: Contradiction or paradox
    ... the general subject of computability. ... depend on referring to some unspecified set of theorems proven in the ... CBL is an axiomatization of computability is ridiculous. ... applicable) CBL is to the problem of formalizing Computer Science ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... Theorems of *what system*? ... systems that meet the axioms given in CBL that refer to PR and TW. ... definition of a Turing Machine here.) ... formalization of metamathematics. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... Theorems of *what system*? ... systems that meet the axioms given in CBL that refer to PR and TW. ... definition of a Turing Machine here.) ... CBL is a formalization of Metamathematical Logic. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... theorems and where are they proven? ... then take that formalization and apply it ... in the language for ZFC extended by definitions. ... Does this undifficult proof use only ZFC's axioms or do we make up ...
    (sci.logic)