#### paulmdrdo

##### Active member

- May 13, 2013

- 386

it's a joke anyway.I have discovered a small error in your proof: since it leads to a contradiction, you must have divided by zero. The correct conclusion should be:

no = -1.

- Thread starter anemone
- Start date

- May 13, 2013

- 386

it's a joke anyway.I have discovered a small error in your proof: since it leads to a contradiction, you must have divided by zero. The correct conclusion should be:

no = -1.

- Feb 15, 2012

- 1,967

Indeed, I realize that. And, see, my reply is a joke, too, because I am responding as if a "joke" were "serious math" which is sheer lunacy.it's a joke anyway.

- Jan 30, 2012

- 2,528

Be it as it may, a large portion of the "proof" actually makes sense.it's a joke anyway.

Here is a code for the Coq proof assistant.\[\begin{aligned} \text{study} &= \text{no fail}\\ \text{no study} &= \phantom{no }\,\text{fail}\end{aligned}\]

If we add these two expressions together, we see that

\[\text{study}+\text{no study} = \text{no fail}+\text{fail}\]

This implies that

\[(1+\text{no})\text{study} = (1+\text{no})\text{fail}\]

Cancelling out the common term now leaves us with

\[\text{study} = \text{fail}\]

Code:

```
Variables study fail : Prop.
Hypothesis h1 : study <-> ~fail.
Hypothesis h2 : ~study <-> fail.
Lemma l1 : study \/ ~study <-> fail \/ ~fail.
Proof. rewrite h2, h1; tauto. Qed.
Definition prop2_plus (f1 f2 : Prop -> Prop) (P : Prop) :=
f1 P \/ f2 P.
Infix "+" := prop2_plus.
Lemma l2 : (id + not) study <-> (id + not) fail.
Proof. apply l1. Qed.
```

The formulas (study \/ ~study) and (fail \/ ~fail) have the same shape, so the idea is to factor out this shape. A similar thing can be done with numbers. The expressions $2+3\cdot2^2$ and $5+8\cdot5^2$ look similar. We can define a function $f(x,y)=x+yx^2$ and represent the two expressions as $f(2,3)$ and $f(5,8)$, respectively. In the same way, we define a function that takes and returns propositions: $f(P)=P\lor{\sim}P$, and say that $f(\text{study})\leftrightarrow f(\text{fail})$.

To make it even more similar to (1 + no)study = (1 + no) = fail from the original proof, we define a higher-order function prop2_plus that takes two functions of type (Prop -> Prop) and returns a similar function. It is basically a pointwise disjunction. It is needed because we cannot apply regular disjunction, which has type Prop -> Prop -> Prop, to the identity function id and the negation not : Prop -> Prop. And voilà,

(id + not) study <-> (id + not) fail.

The only thing is that this is not multiplication, but function application. And since (id + not) is not injective, unlike multiplication by a nonnegative number, we cannot conclude that study <-> fail.

This ability to define functions not only on datatypes like numbers and strings, but also on propositions, as well as the ability to define higher-order functions (those that take functions as arguments) are characteristics of the so called type theory, on which Coq is based.

OK, I'll crawl back into my nerdy hovel now...

- Aug 30, 2012

- 1,207

I think I watched a Dr. Who episode based on this.Be it as it may, a large portion of the "proof" actually makes sense.

Here is a code for the Coq proof assistant.

Here Prop is the type of propositions, i.e., the type of Boolean formulas. Disjunction is denoted by \/ and the negationCode:`Variables study fail : Prop. Hypothesis h1 : study <-> ~fail. Hypothesis h2 : ~study <-> fail. Lemma l1 : study \/ ~study <-> fail \/ ~fail. Proof. rewrite h2, h1; tauto. Qed. Definition prop2_plus (f1 f2 : Prop -> Prop) (P : Prop) := f1 P \/ f2 P. Infix "+" := prop2_plus. Lemma l2 : (id + not) study <-> (id + not) fail. Proof. apply l1. Qed.`

notis denoted by ~.

The formulas (study \/ ~study) and (fail \/ ~fail) have the same shape, so the idea is to factor out this shape. A similar thing can be done with numbers. The expressions $2+3\cdot2^2$ and $5+8\cdot5^2$ look similar. We can define a function $f(x,y)=x+yx^2$ and represent the two expressions as $f(2,3)$ and $f(5,8)$, respectively. In the same way, we define a function that takes and returns propositions: $f(P)=P\lor{\sim}P$, and say that $f(\text{study})\leftrightarrow f(\text{fail})$.

To make it even more similar to (1 + no)study = (1 + no) = fail from the original proof, we define a higher-order function prop2_plus that takes two functions of type (Prop -> Prop) and returns a similar function. It is basically a pointwise disjunction. It is needed because we cannot apply regular disjunction, which has type Prop -> Prop -> Prop, to the identity function id and the negation not : Prop -> Prop. And voilà,

(id + not) study <-> (id + not) fail.

The only thing is that this is not multiplication, but function application. And since (id + not) is not injective, unlike multiplication by a nonnegative number, we cannot conclude that study <-> fail.

This ability to define functions not only on datatypes like numbers and strings, but also on propositions, as well as the ability to define higher-order functions (those that take functions as arguments) are characteristics of the so called type theory, on which Coq is based.

OK, I'll crawl back into my nerdy hovel now...

-Dan

- Thread starter
- Admin
- #30

- Feb 14, 2012

- 3,909

Answer: On the bottom of the page.

2. River Ravi, flows in which state?

Answer: Liquid State.

3. What can you never eat for breakfast?

Answer: Lunch and Dinner

4. What looks like half an apple?

Answer: The other half.

5. What is the main reason for divorce?

Answer: Marriage

6. In which battle did Napoleon die?

Answer: His last one.

- Aug 18, 2013

- 76

The first one orders a pint, the second one a half pint, the third one a quarter pint...

"I understand", says the bartender - and pours two pints.

- Thread starter
- Admin
- #32

- Feb 14, 2012

- 3,909

- Thread starter
- Admin
- #33

- Feb 14, 2012

- 3,909

- Feb 9, 2012

- 33

So the Hilbert Hotel also has a Hilbert Bar and Hilbert himself is tending bar with Cantor as the 'BOUNCER'

The first one orders a pint, the second one a half pint, the third one a quarter pint...

"I understand", says the bartender - and pours two pints.

- Moderator
- #35

- Jan 26, 2012

- 995

[HR][/HR]

A Statistician, Engineer and Physicist go to the horse track. Each have their system for betting on the winner and they're sure of it.

After the race is over, the Statistician wanders into the nearby bar, defeated. He notices the Engineer, sits down next to him, and begins lamenting: "I don't understand it. I tabulated the recent performance of all these horses, cross-referenced them with trends for others of their breed, considered seasonal variability, everything. I couldn't have lost."

"Yeah," says the Engineer, "well, forget that. I ran simulations based on their weight, mechanical ratios, performance models, everything, and I'm no better off."

Suddenly, they notice a commotion in the corner. The Physicist is sitting there, buying rounds and counting his winnings. The Engineer and Statistician decide they've got to know, so they shuffle over and ask him, "what's your secret, how'd you do it?"

The Physicist leans back, takes a deep breath, and begins, "Well, first I assumed all the horses were spherical and identical..."

[HR][/HR]

A mathematician, a physicist, and an engineer are given the task of finding how high a particular red rubber ball will bounce when dropped from a given height onto a given surface.

The mathematician derives the elasticity of the ball from its chemical makeup, derives the equations to determine how high it will bounce and calculates it.

The physicist takes the ball into the lab, measures its elasticity, and plugs the variables into a formula.

The engineer looks it up in his red rubber ball book.

- Moderator
- #36

- Jan 26, 2012

- 995

And one more (as a picture, though)!

- Feb 15, 2012

- 1,967

A: Because of Cantor.

(Warning: Educated non-mathematicians may find this joke slightly funnier).

- Aug 30, 2012

- 1,207

- Aug 18, 2013

- 76

BTW, if you already know some of the basics of group theory and want to get into more advanced material as well as applications, I recommend David Joyner's

A reporter approaches a Saudi, a Hindu, a North Korean,

and a New Yorker.

He says, "Pardon me, what is your opinion on the beef shortage?"

The Saudi says, "What is a

The Hindu says, "What is

The North Korean says, "What is an

The New Yorker says, "What is

- Aug 18, 2013

- 76

That was actually quite offensive.

- Jan 26, 2012

- 644

- Thread starter
- Admin
- #43

- Feb 14, 2012

- 3,909

- Admin
- #44

- Thread starter
- Admin
- #45

- Feb 14, 2012

- 3,909

- Aug 18, 2013

- 76

There are 10 types of people in the world: those who understand base 16, and F the rest.

- Thread starter
- Admin
- #47

- Feb 14, 2012

- 3,909

- Mar 22, 2013

- 573

- Mar 22, 2013

- 573

- Feb 15, 2012

- 1,967

International Choice of Urinal Protocol...ohemgee!