From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 51D2FBC69 for ; Thu, 4 Oct 2007 17:57:52 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAO+pBEfAXQImh2dsb2JhbACOOAEBCQon X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="asc'?vcf'?scan'208";a="2382790" Received: from discorde.inria.fr ([192.93.2.38]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 17:57:51 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l94Fvh9L025749 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 17:57:51 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAO+pBEfUGyodimdsb2JhbACOOAEBCQQGIAc X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="asc'?vcf'?scan'208";a="17297882" Received: from smtp3-g19.free.fr ([212.27.42.29]) by mail4-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 17:57:51 +0200 Received: from smtp3-g19.free.fr (localhost.localdomain [127.0.0.1]) by smtp3-g19.free.fr (Postfix) with ESMTP id 0566117B537; Thu, 4 Oct 2007 17:57:51 +0200 (CEST) Received: from Tocksi.local (unknown [82.253.223.12]) by smtp3-g19.free.fr (Postfix) with ESMTP id 9F26817B540; Thu, 4 Oct 2007 17:57:50 +0200 (CEST) Message-ID: <47050D7E.2010708@univ-savoie.fr> Date: Thu, 04 Oct 2007 17:57:50 +0200 From: Christophe Raffalli User-Agent: Thunderbird 2.0.0.6 (Macintosh/20070728) MIME-Version: 1.0 To: Andrej.Bauer@andrej.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] Unsoundness is essential References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <1191462724.7542.76.camel@rosella.wigram> <47049A6D.6020201@univ-savoie.fr> <4704AAA8.9080602@lix.polytechnique.fr> <470500F9.1080301@fmf.uni-lj.si> In-Reply-To: <470500F9.1080301@fmf.uni-lj.si> X-Enigmail-Version: 0.95.3 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="------------enigA8ED37E3347C2CE81BCF8493" X-Miltered: at discorde with ID 47050D77.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 christophe:01 raffalli:01 univ-savoie:01 andrej:01 theorems:01 model:01 axioms:01 model:01 chablais:01 73376:01 univ-savoie:01 compulsive:98 wrote:01 X-Attachments: cset="ISO-8859-2" cset="utf-8" name="Christophe.Raffalli.vcf" name="Christophe.Raffalli.vcf" type="application/pgp-signature" name="signature.asc" name="signature.asc" This is an OpenPGP/MIME signed message (RFC 2440 and 3156) --------------enigA8ED37E3347C2CE81BCF8493 Content-Type: multipart/mixed; boundary="------------070707000702040706080609" This is a multi-part message in MIME format. --------------070707000702040706080609 Content-Type: text/plain; charset=ISO-8859-2 Content-Transfer-Encoding: quoted-printable Andrej Bauer a =E9crit : > I too have a compulsive obsession to talk about logic, so here is my > contribution. > > Logic is about details. It is only to be expected that in a > willy-waving competition on a mailing list like ours everyone will get > something wrong about such a tricky thing as Goedel's theorems (me > included). For example: > > Christophe Raffalli: >> - first if a type system does not contain arithmetic nothing can be sa= id >> (this implies ML), but in this case, the meaning of complete needs to >> be clarified. >> Indeed, there are complete type system ... > In logic complete usually means: for every sentence A the system > proves A or it proves not A. This has nothing to do with being able to > interpret arithmetic. We can define completeness without reference to > arithmetic. Sorry, I see now that I was not clear enough : Complete (at least in french) has many meanings, the one you said and the fact that something true in every model is provable (which make a lot of meaning depending to the models you are considering). The two meanings are unrelated, because arithmetics is complete as is any first order theory (this is G=F6del Completeness theorem for predicat= e logic), but incomplete because there are formula A such that neither A nor not A are provable. This is quite confusing. But in both case complete means "there are enough rules/axioms in the system to do what I want". You are just making the "what I want" more or less strong. For type systems, if you replace proving by inhabited, they are usually incomplete, but then, you can look for completeness relative to some model (like realizability) ... and the answer is yes in some cases. This is generally a good idea to search for a set of models large enough for your type system to be complete ... because sometime you realize that you forgot some usefull typing rules in your type system. > > (Presumably, a type system is complete if for every (closed) type A, > A is inhabited or A -> void is inhabited. At least this would be the > reading of completeness under propositions-as-types.) > > Christophe Raffalli: >> - The 1st incompleteness theorem states that no theory containing >> arithmetic is complete. > > No _sound_ theory interpreting arithmetic is complete. Ok, this was implicit. > > Arnaud Spiwack wrote: >> Anyway, back to Mr. G=F6del and his theorem. What he stated indeed is >> that truth and provability never coincide (provided we're talking of >> something at least as expressive as arithmetic). This is Tarski's result .... (actually Tarski proved that truth can not even be defined by a formula of arithmetic, which imply that provability and truth do not coincide because provable formula are definable). --=20 Christophe Raffalli Universite de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tel: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univ-savoie.fr www: http://www.lama.univ-savoie.fr/~RAFFALLI --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution=20 can check this signature. The public key is stored on www.keyserver.net --------------------------------------------- --------------070707000702040706080609 Content-Type: text/x-vcard; charset=utf-8; name="Christophe.Raffalli.vcf" Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename="Christophe.Raffalli.vcf" begin:vcard fn:Christophe Raffalli n:Raffalli;Christophe org:LAMA (UMR 5127) email;internet:christophe.raffalli@univ-savoie.fr title;quoted-printable:Ma=3DC3=3DAEtre de conf=3DC3=3DA9rences tel;work:+33 4 79 75 81 03 note:http://www.lama.univ-savoie.fr/~raffalli x-mozilla-html:TRUE version:2.1 end:vcard --------------070707000702040706080609-- --------------enigA8ED37E3347C2CE81BCF8493 Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.7 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFHBQ1+i9jr/RgYAS4RAs5iAJwMBBb11He6yFbtTl0xefJ2mnDLbgCeLkyj CTEEpbU0gSWUj+sk1bO/brM= =OLDx -----END PGP SIGNATURE----- --------------enigA8ED37E3347C2CE81BCF8493--