Automated Proof Checking

[Don Blazys]

Can someone please help me verify this proof

 

http://donblazys.com/02.pdf

 

by computer, or at least help me write it out in

"first order logic" or whatever symbols that are

most often used for this sort of thing.

 

The necessary contradiction in the form "P and not P"

would be as follows:

 

If Beal's Conjecture is false, then [math]Z>2, z>2[/math] and "P and not P"

 

where "P" is the assertion that [math]T\neq{c}\rightarrow\frac{T}{T}\neq\frac{c}{c}[/math]

 

and "not P" is the assertion that [math]T=c\rightarrow\frac{T}{T}=\frac{c}{c}[/math]

 

and the required resolution would be:

 

If Beal's Conjecture is true, then [math]Z=1, z=2[/math] and "not P"

 

Thanks in advance,

 

Don.

[Qfwfq]

where "P" is the assertion that [math]T\neq{c}\rightarrow\frac{T}{T}\neq\frac{c}{c}[/math]

 

and "not P" is the assertion that [math]T=c\rightarrow\frac{T}{T}=\frac{c}{c}[/math]

The second thing is not the negation of the first.

 

If you call the first proposition P, then "not P" should be the assertion that it is possible for [math]\frac{T}{T}=\frac{c}{c}[/math] to hold along with [math]T\neq{c}[/math]

Edited October 21, 2010 by Qfwfq
dumb mistakes

[Don Blazys]

The second thing is not the negation of the first.

 

If you call the first proposition P, then "not P" should be the assertion that it is possible for [math]\frac{T}{T}=\frac{c}{c}[/math] to hold along with [math]T\neq{c}[/math]

 

Thanks Qfwfq,

 

That does make a lot more sense because if [math]Z>2[/math] and [math]z>2[/math],

 

then the condition [math]T\neq{c}[/math] applies to each and every [math]T[/math]

 

so we cannot substitute [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math].

 

 

On the other hand, since [math]\frac{c}{c}=\frac{T}{T}[/math] is obviously an equality,

 

it seems that we can substitute [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math] when [math]T\neq{c}[/math].

 

 

 

(What a great contradiction!!!) :Exclamati :Exclamati :Exclamati

 

 

 

However, if [math]Z=1[/math] and [math]z=2[/math],

 

then the condition [math]T\neq{c}[/math] doesn't exist,

 

which obviously and unequivocally allows us to substitute [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math],

 

and is thereby the resolution to the contradiction !

 

 

 

I'm sure we can agree that the contradiction, as stated above, exists.

 

 

 

Please keep in mind that the language of "predicate calculus" remains entirely foreign to me,

 

so your help is still badly needed and much appreciated.

 

If we can verify this through an "automated system", then we will be much closer to the prize,

 

which we can both share in, and perhaps even buy a reasonably priced supercomputer for "Hypography Central".

 

(There's nothing wrong with dreaming, if we are willing and able to do the work.)

 

Don.

[Don Blazys]

Beal's Conjecture is false [math]\rightarrow[/math] [math]Z>2, z>2[/math] [math]\rightarrow[/math]

 

[math]a^x+b^y=\sqrt{((b^y-a^x)^{2}+4*a^x*b^y)}=\sqrt{(c^Z)^{2}}=c^Z=\left(\frac{T}{T}\right)*c^Z=T*\left(\frac{c}{T}\right)^{\frac{\frac{Z*ln©}{ln(T)}-1}{\frac{ln©}{ln(T)}-1}}[/math]

 

[math]\wedge[/math]

 

[math]a^x+b^y=\sqrt{((b^y-a^x)^{2}+4*a^x*b^y)}=\sqrt{(c^z)^{2}}=\left(c^{\frac{z}{2}}\right)^{2}=\left(\left(\frac{T}{T}\right)*c^{\frac{z}{2}}\right)^{2}=\left(T*\left(\frac{c}{T}\right)^{\frac{\frac{\frac{z}{2}*ln©}{ln(T)}-1}{\frac{ln©}{ln(T)}-1}}\right)^2[/math]

 

[math]\leftrightarrow[/math] [math]T\neq{c}[/math] [math]\rightarrow[/math] [math]\frac{T}{T}\neq\frac{c}{c}[/math] [math]\wedge[/math] [math]\frac{T}{T}=\frac{c}{c}[/math]

 

 

Beal's Conjecture is true [math]\rightarrow[/math] [math]Z=1, z=2[/math] [math]\rightarrow[/math]

 

 

[math]a^x+b^y=\sqrt{((b^y-a^x)^{2}+4*a^x*b^y)}=\sqrt{(c^1)^{2}}=c^1=\left(\frac{T}{T}\right)*c^1=T*\left(\frac{c}{T}\right)^{1}[/math]

 

[math]\wedge[/math]

 

[math]a^x+b^y=\sqrt{((b^y-a^x)^{2}+4*a^x*b^y)}=\sqrt{(c^2)^{2}}=\left(c^{1}\right)^{2}=\left(\left(\frac{T}{T}\right)*c^{1}\right)^{2}=\left(T*\left(\frac{c}{T}\right)^{1}\right)^2[/math]

 

[math]\rightarrow[/math] [math]T=c[/math] [math]\rightarrow[/math] [math]\frac{T}{T}=\frac{c}{c}[/math]

 

Therefore, Beal's Conjecture is true.

 

The above is my attempt at using the symbols of "predicate calculus"

in order to express the argument in my proof: http://donblazys.com/02.pdf

 

Did I make any mistakes? Is the syntax okay? Is there a better way to do it?

Are there a latex symbols for "therefore" "is true" and "is false"?

Am I supposed to assign the words "Beal's Conjecture" a symbol?

 

My inquiring mind want's to know!

 

If we can write this entire proof using the symbols of "predicate calculus"

then we will have not only a proof of Beal's Conjecture and Fermat's Last Theorem

that can be verified by computer, but we will also have a "publication ready"

version that can be sent to various snooty math journals !

 

This proof took only ten minutes to discover, but has not been verified

(or refuted) by the math community (exept for a few brave souls ) in over eleven years!

 

That's sheer insanity, and the math community will never live it down.

They will have egg on their faces for the rest of eternity, and a collective

"black eye" that will last forever!

 

Really folks, it's time to let the computers take a crack at it.

 

 

Don.

[Qfwfq]

Don, exactly how does division by zero prevent the substitution of: [imath]\frac{c}{c}[/imath] for: [imath]\frac{T}{T}[/imath] in equations (1) and (2) as you say in your paper?

 

This proof took only ten minutes to discover, but has not been verified (or refuted) by the math community (exept for a few brave souls ) in over eleven years!

Which brave souls? Edited October 28, 2010 by Qfwfq
dumb mistake

[Don Blazys]

Quoting Qfwfq:

Which brave souls?

 

I can't give their names out over the internet, but they know who they are.

One such "heavy hitter" (whose initials are B.B.) has Phd's in both mathematics and physics.

He is the one who, several years ago, suggested that I present this proof in various internet forums.

Well,he was right because if you Google search "Beal's Conjecture Proof", then you will find that

my proof now consistently occupies three or four of the top five positions!

Consequently, I am now getting e-mails all the time.

Many are from students who feel that they will never understand

Wile's proof of Fermat's Last Theorem, but find my proof of Beal's Conjecture,

which is the "general case" of Fermat's Last Theorem easy to understand.

I haven't had the time to update my website for quite a while now, but if you go here:

 

http://donblazys.com/letters_and_articles.pdf

 

then you will find a few more of those "brave souls" who put their support in writing.

There are a lot more besides them, and judging from my e-mails,

the number of people who understand and support my proof is growing exponentially!

 

This doesn't surprise me at all.

People naturally gravitate towards truth, beauty and simplicity.

My proof does not require some painstakingly long drawn-out lawerlike argument.

It is simply a direct consequence of an extraordinarily elegant and original equation.

Thus, it is a lot more powerful and compelling than Wile's two hundred page's of mental gymnastics.

 

 

Don, exactly how does division by zero prevents the substitution of: [imath]\frac{c}{c}[/imath] for: [imath]\frac{T}{T}[/imath] in equations (1) and (2) as you say in your paper?

 

Here's my proof: http://donblazys.com/02.pdf

 

Clearly, we can't divide by zero.

 

That prevents the substitution of [math]c[/math] for [math]T[/math] in equations (1) and (2).

 

Obviously, we can't substitute [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math] without also substituting [math]c[/math] for [math]T[/math].

 

That prevents the substitution of [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math].

 

A variable cannot represent one value on one side of an equation

and another, different value, on the other side of that same equation.

(That would require two different variables and would compromise

the fact that one side was derived from the other.)

Thus, we cannot substitute [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math], or equivalently, [math]c[/math] for [math]T[/math] on one side only.

 

Anyway, all of this is way off topic.

What I need is some help in writing up this proof using the symbols of

predicate calculus or first order logic. Can you help me with that?

What do you think of my last attempt?

Did I make any mistakes? Is the syntax okay? Is there a better way to do it?

Are there a latex symbols for "therefore" "is true" and "is false"?

Am I supposed to assign the words "Beal's Conjecture" a symbol?

 

Don.

[Qfwfq]

Here's my proof: http://donblazys.com/02.pdf

 

Clearly, we can't divide by zero.

Er... Don, when I said "in equations (1) and (2) as you say in your paper" it might have been clear that I had looked at your paper, so linking again to your paper isn't much use as a way of showing me your proof.

 

I also looked through the other link, including your letter to Mr. Romer wherin you claim likewise about division by zero. As I don't see the use for dividing by two, allow me to write it as follows:

 

[math]\frac{TU^v}{T}=T\left(\frac{U}{T}\right)^{\frac{v\log_T U - 1}{\log_T U - 1}}[/math] (1)

 

Equality to the third expression is clear, by the usual manner of converting base. Equality between the above two isn't too hard to establish; by manipulating the exponent, using [imath]1=\log_T T[/imath] and likewise exploiting base conversions I can get [imath]U^{v}[/imath] without excessive difficulty and this clearly equals the right hand side above. After manipulating the exponent:

 

[math]\frac{v\log_T U - 1}{\log_T U - 1}=\frac{v\log_T U - 1}{\log_T U - \log_T T}=\frac{v\log_T U - 1}{\log_T\frac{U}{T}}[/math]

 

Knocking out the denominator in the third expression of the exponent is clearly a conversion of the base to [imath]T[/imath] in the rhs of (1) as follows:

 

[math]T\left(\frac{U}{T}\right)^{\frac{v\log_T U - 1}{\log_T U - 1}}=T^{1+v\log_T U -1}=U^v[/math]

 

Can you show me where the divide by zero is lurking unseen to me?

[Don Blazys]

Quoting Qfwfq:

Er... Don, when I said "in equations (1) and (2) as you say in your paper"

it might have been clear that I had looked at your paper,

so linking again to your paper isn't much use as a way of showing me your proof.

 

I put that extra link to my proof there for several reasonable reasons.

The first and foremost reason is expedience and convenience.

I simply don't want my gentle readers to be inconvenienced

by having to scroll back and search for that link.

 

The other reason I put it there was to remind us to stay on topic.

The purpose of this thread is to get my proof written in

the language of "predicate calculus" or "first order logic".

Thus, we need not argue the correctness of this proof because

ultimately, it's correctness will be determined by computer.

 

Quoting Qfwfq:

I also looked through the other link, including your letter to Mr. Romer

wherin you claim likewise about division by zero.

 

In my proof, I don't "claim likewise about division by zero".

In fact, the only thing I claim about division by zero in my proof is that

we can't do it, which means that we can't substitute [math]\frac{c}{c}[/math] for [math]\frac{T}{T}[/math] when the exponents are greater than [math]2[/math] .

 

Quoting Qfwfq:

[math]T\left(\frac{U}{T}\right)^{\frac{v\log_T U - 1}{\log_T U - 1}}=\left(\frac{T}{T}\right)T^{v\log_T U}=\left(\frac{T}{T}\right)U^v[/math]

 

[math]\left(T\left(\frac{U}{T}\right)^{\frac{\frac{V}{2}\log_T U - 1}{\log_T U - 1}}\right)^{2}=\left(\left(\frac{T}{T}\right)T^{\frac{V}{2}\log_T U}\right)^{2}=\left(\left(\frac{T}{T}\right)U^\frac{V}{2}\right)^{2}[/math]

 

 

 

Can you show me where the divide by zero is lurking unseen to me?

 

 

Sure! With regards to my proof, the divide by zero is lurking... stealthily... silently... patiently... waiting and...

 

ready to pounce on us and kill us if we even think about substituting [math]U[/math] for [math]T[/math] or equivalently [math]\frac{U}{U}[/math] for [math]\frac{T}{T}[/math].

 

Therefore, if (in this case) [math]v>2[/math] and [math]V>2[/math] then we can't substitute [math]\frac{U}{U}[/math] for [math]\frac{T}{T} [/math]

 

However, if [math]v=1[/math] and [math]V=2[/math] then we can substitute [math]U[/math] for [math]T[/math] or equivalently [math]\frac{U}{U}[/math] for [math]\frac{T}{T}[/math], which proves the conjecture.

 

(By the way, in your derivation, you forgot to include the cancelled [math]T[/math]'s,

so I put them back in for you and included the original terms in the letter)

 

 

But... again we have gone way off topic!

 

The correctness of the proof is not in question because the proof is literally the equation itself

and doesn't require (as I said before) a long drawn out lawerlike argument.

 

That letter to Mr. Romer has absolutely nothing to do with the purpose of this thread.

In fact, it's a completely different issue altogether, (but it is important,)

so since you brought it up, I will start a new thread on that particular issue

in the physics and mathematics section of this great forum.

 

Now, please... let's get back to the purpose of this thread.

 

What I need is some help in writing up this proof using the symbols of

predicate calculus or first order logic. Can you help me with that?

What do you think of my last attempt?

Did I make any mistakes? Is the syntax okay? Is there a better way to do it?

Are there a latex symbols for "therefore" "is true" and "is false"?

Am I supposed to assign the words "Beal's Conjecture" a symbol?

 

Don.

[Don Blazys]

This is really frustrating!

 

The symbol [math]\bot[/math] means "false" as in "the statement [math]\bot[/math] is unconditionally false".

 

The symbol [math]\bot[/math] also means "is co-prime to" as in " [math]14\bot15[/math].

 

So how in the heck are we supposed to use this hopelessly ambiguous symbol in a proof

that contains both the notion of co-primality and an assumption that the conjecture is false?!?!

 

Don.

[Turtle]

...What I need is some help in writing up this proof using the symbols of

predicate calculus or first order logic. Can you help me with that?

...

Don.

 

i don't know isabelle, but i ran across "her" in that gödel link i gave in the consitency thread. hope it...erhm...she...helps. (bolednation mine.)

 

Isabelle Theorem Prover

The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover.

...

Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license....

 

Isabelle Website: Isabelle: University of Cambridge

[Don Blazys]

Thanks Turtle,

 

There's a lot of information there...

 

plenty of links etc...

 

Much to investigate.

 

Much obliged!

 

Don.

[Don Blazys]

Here is a "symbols only" version.

 

http://donblazys.com/03.pdf

 

Is it easier to understand than the other versions?

 

Don.