The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 26.10.2012 00:45, schrieb Pierre-Marie Pédrot:
> Drugs are bad, mkay?

Shucks, you should've told me before : (

> (More seriously, I would like to have any fallacious theorem like 
> Gödel/Descartes ontological existence of God formalized in any 
> trustworthy theorem prover to see which exact definition you need to 
> prove such theorems. 

That might be interesting! But in fact I believe that formalizing those 
existence proofs will only show the tautological structure of these 
proofs. But even if they do, Descartes would just say "You are a fool 
for trying, because God can not be formalized". That's Descartes for you : (

Goedel might be a lot more interesting. But also a lot more tedious. I 
wonder if there is a slightly different proof that does not rely on the 
natural numbers and goedilization that much, but rather on, say, lambda 
calculus+decidable typing and some way to allow meta-statements? (Like, 
x :: T being an expression with type Prop where z : x::T if and only if 
z is a typing derivation that proves x:T)

> Anyway, as « all you need is love », that implies in particular:
>
> Theorem : love -> False.

I see what you did there! But I think we can get out of this tight spot 
by saying: "all you need is love" is just idealistic stuff that's not 
true. In particular, people need food and water, too.

> Thus, « Come back Grothendieck, they've become crazy! »)
>
> Uninformatively yours,
> PMP