Re: [Caml-list] Unsoundness is essential

[Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>]

[-- Attachment #1.1: Type: text/plain, Size: 3303 bytes --]

Andrej Bauer a écrit :
> 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 said
>> (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ödel Completeness theorem for predicate
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ödel 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).

-- 
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 
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #1.2: Christophe.Raffalli.vcf --]
[-- Type: text/x-vcard, Size: 310 bytes --]

begin:vcard
fn:Christophe Raffalli
n:Raffalli;Christophe
org:LAMA (UMR 5127)
email;internet:christophe.raffalli@univ-savoie.fr
title;quoted-printable:Ma=C3=AEtre de conf=C3=A9rences
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


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 249 bytes --]