Re: proof of undecidability of halting problem
- From: David C. Ullrich <ullrich@xxxxxxxxxxxxxxxx>
- Date: Mon, 19 Jun 2006 06:55:25 -0500
On 18 Jun 2006 12:35:52 -0700, "Charlie-Boo" <shymathguy@xxxxxxxxx>
wrote:
MoeBlee wrote:
Charlie-Boo wrote:
Norm Megill offered you a hundred bucks to prove that his system allows
anything to be a theorem. You're still claiming that his system allows
anything to be a theorem, even though you have not the slightest proof
of such a thing.
1. Apply 3ecoptocl to F=-, A=3, B=1, C=1 to get (3-1)-1=3-(1-1).
Substitute definitions to get 1=3.
You're just spewing random nonsense.
It's the same thing that he wrote except that I use constants 1, 2 and
3 and function - whereas he uses variables A,B andC and function +.
You ask for a proof and I give you a proof. Now either show what's
wrong with it or admit that NM is a fraud.
Is there a notion of "apply" in Logic? Yes, we apply a Rule of
Inference to a wff. Is there such a thing as "3ecoptocl" in MetaMyth?
Yes, it is listed as a theorem. etc. Which step is wrong?
You just wasted my time tracking down to confirm that your bluff is not
a proof of an inconsistency. I hope not to let myself waste my time
that way again.
You didn't say a word about the contents of my proof.
You didn't give a proof. (3ecoptocl has _hypothses_, by the way.)
Different theorems are shorter or
longer depending on the primitives available.
Speaking of well defined, you just mentioned "shorter or longer
theories." I very much doubt that you even know what at theory is.
No I didn't. I said theorems, not theories.
And that's "violence on TV", not "violins on TV".
For the most part, the fewer the axioms, the longer the
proofs.
No, you have a different theory.
Now I KNOW you don't know what a theory is. A theory can have different
axiomatizations. As well as conservative extensions of theories can
have different languages.
If you have "fewer axioms" and e.g. PA with no redundant (otherwise
provable within the Logic) axioms, then you have fewer theorems so it
is a different theory.
Or, the fewer the primitives, then the more the axioms and
definitions.
No, the longer the axioms and definitions are.
1. Recall that I said "for the most part". 2. You're back to YOUR
undefined "longer". 3. My point is that if you have fewer primitives,
then to abbreviate, you need additional definitional axioms for defined
symbols.
Definitions in MetaMath are added at will ad infinitum e.g. he defines
successor with a set of definitions of the form (N+1) = (N) + 1 e.g.
4=3+1. But then you never prove all of what PA defines because you
have only a finite number of definitions. MetaMath has to be enhanced
to prove additional theorems!
And even some loss of economy is prefereble where a more
economical approach is less intuitive. For example, you can have the
theory of Boolean algebra with just two primitives (including equality)
and one axiom; but such a system doesn't have the clarity as the usual
axiomatization with six primitives (including equality) and the array
of axioms that allow us to see the dualistic nature of the theory.
No. If a subset will do, then you use the subset and highlight the
compositions that represent what the primitives that were to be added
represent. If they can't be represented, then you have a different
system.
I didn't say they can't be defined. So, anyway, since you hold the view
above, I suggest you teach Boolean algebra with just one primitive and
one axiom then spend the entire rest of the course, with the aid of
computers, proving the equivalence with the usual axiomatization.
That's make a great class. Are you familiar with Combinatory Logic
(e.g. "To Mock a Mockingbird" by Smullyan)?
Sometimes the point is just to get to work with a theory and less that
of starting with the fewest primitives and axioms.
No, Occam/C-B's Razor applies.
Set theory is used not just to axiomatize a good amount of arithmetic
and the real numbers but also to allow that amount of arithmetic to be
used WITH the real numbers so that we can have an axiomatization that
expresses such things as real valued sequences and gives their
properties.
That's true of any aleph-0 set. You're not making use of anything
special about the sets.
We're making use of all the axioms of Z set theory. Look it up
sometime.
Not in 2+2=4
Arithmetic is about a particular set (numbers) while Set Theory is
about all sets. This is analogous to Recursion Theory and the Theory
of Computation being about a particular base of computing (Turing
Machines) whereas Logic studies bases of computing in general (that may
be inconsistent whereas no Turing Machine can both halt yes and halt
no.)
That's a very bad analogy. Recursive functions are one paradigm of
computatility; but arithmetic is not itself a paradigm of real
analysis.
You're confused. It's not arithmetic that is the other paradigm
parallel to Computability, it's Logic.
No, you're confused about your own analogy. You compared arithmetic to
set theory as you compared recursion to computability. But what is at
stake is arithmetic in comparision with set theory for analysis.
Arithmetic is to Set Theory as Turing Machines are to Logic.
You have set manipulations in general in Set Theory and the
manipulation of a single set, numbers, in Arithmetic. You have Bases
of Computing in general in Logic (e.g. PA represents the same sets as
Turing Machines) and the single set of the recursive functions or r.e.
sets in Recursion Theory and the Theory of Computation (Computability.)
As I say above, Logic studies
bases of computing in general (that may be inconsistent whereas no TM
is, in the analogy of halt=prove.)
Also, by the way, recursion theory is usually part of set
theory anyway. Also, I'm not asking whatever it is you think you mean
by 'inconsistency' in context of computability,
I say above that consistency is "no Turing Machine can both halt yes
and halt no"
A Turing machine, in the strictest mathematical sense, is not something
that is either consistent or inconsistent. In this sense, a Turing
machine is a certain kind of set of 4-tuples. It's not the kind of
thing we take to be consistent or inconsistent in this context. What
are consistent or inconistent are sets of formulas.
An axiomatic system defines two r.e. sets, sentences provable and
sentences refutable. Turing Machines define two r.e. sets, Turing
Machines that halt yes and those that halt no. A sentence may be
provable and refutable, but no program halts both yes and no. So Logic
is more general than Turing Machines in that PA gives you Turing
Machines but there are also inconsistent systems of Logic.
You're ignorant. The associative law of addition for natural numbers is
also a theorem of set theory.
Show that in MetaMath.
http://us.metamath.org/mpegif/nnaass.html
You can also prove that (3-1)-1=3-(1-1) so 1=3. Follow it to its roots
and it's not ZF.
And I'm very much disinclined to respond to further of your challenges,
since I wasted my time months ago responding to a request for my
definition of something, yet you failed ever to respond to my request
in turn for what reason you required that definition. You're a huge
sink hold of meaninglessness.
and ZF is notIf ALL we wanted to do is arithmetic, then we'd have just axioms for
needed. All we need is the associative law of addition.
arithmetic. But we also want to have such things as real valued
sequences, which are provided for by set theory and not by just axioms
for arithmetic.
I'm talking about for 2+2=4.
No one in set theory does not realize that 2+2=4 can be more easily
proven in, for example, PA. But that is not the point, and you missed
the point again, even as I explained it to you: We need more than such
formulas such as 2+2=4. We also need theorems about such things as real
valued sequences.
That doesn't change the fact that a simpler proof is possible and
preferable, and an inconsistent system is worthless.
And the set theoretic axiomatization provides for
BOTH such theorems of arithmetic as 2+2=4 and for things like real
valued sequences. So we don't need to adopt PA axioms since they are
themselves just theorems of set theory.
Arithmetic needs the associative law of addition. In general, each
branch of Mathematics has its own axioms and rules. This contradicts
the assertion that MetaMath uses only ZF.
You're ignorant. The basics of arithmetic, including the associative
law of addition, are theorems of ZF.
You're just repeating yourself (using multiple repetitions.)
I repeated my correction since you repeated your incorrect assertion.
Since set theory proves the associativity of addition of natural
numbers, it is not going outside of set theory to use the theorem of
the associativity of addition of natural numbers. You just present as
ignorant by claiming otherwise.
In PA we simply define 2 as 0'' and 4 as 0'''' so that 2+2 is (0'')'' .
We then apply the general rule of parentheses that (A)B is AB since
expressions in parentheses are evaluated left to right, to produce
0'''' which by definition is 4. The actual PA proof is fairly trivial,
matching the trivial nature of 2+2=4.
Sure, because PA doesn't need to provide for such things as real valued
sequences. But since we want to have such things as real valued
sequences, we adopt axioms that will provide for them.
That wouldn't make the first proof any longer - conceivably shorter
if anything.
No, since there is a train of theorems leading up to proving the PA
axioms. Once we've proven the PA axioms as theorems, then we can make
any proof of PA just as short in set theory.
You need not change the first proof when you add axioms to the system,
so the first proof would not have to be any longer.
C-B
MoeBlee
************************
David C. Ullrich
.
- References:
- Re: proof of undecidability of halting problem
- From: Charlie-Boo
- Re: proof of undecidability of halting problem
- From: MoeBlee
- Re: proof of undecidability of halting problem
- From: Charlie-Boo
- Re: proof of undecidability of halting problem
- From: MoeBlee
- Re: proof of undecidability of halting problem
- From: Charlie-Boo
- Re: proof of undecidability of halting problem
- From: MoeBlee
- Re: proof of undecidability of halting problem
- From: Charlie-Boo
- Re: proof of undecidability of halting problem
- Prev by Date: Re: Solving equation on Concept Algebra--Answer One a Question
- Next by Date: Re: Frege: Reason's nearest kin
- Previous by thread: Re: proof of undecidability of halting problem
- Next by thread: Re: proof of undecidability of halting problem
- Index(es):
Relevant Pages
|