Re: Le cerveau n'est pas logique

Je précise ici ma réponse sur ZF vu comme un langage dynamiquement typé. On pourra continuer la discussion de cette sous-question sous ce commentaire et laisser celle sur la physique à un autre fil.

Je comprend bien l’idée, mais l’analogie trouve ses limites vu que la logique du premier ordre n’est pas constructive.

Ici tu confonds deux choses : la logique du premier et la logique intuitionniste. La première concerne les règles de formation des jugements, la seconde traite des règles d'inférences ou raisonnements. J'ai déjà écrit ailleurs un commentaire, en réponse à une question de Michaël, sur la différence entre les deux notions, le rapport entre programmes et preuves de théorème (correspondance de Curry-Howard) et la distinction entre les systèmes de types de OCaml et de Coq.

Si x n’appartient pas à Oméga, ben, rien, ça ne pose pas de problème.

Si ça pose problème : dans un cas l'énoncé est prouvable dans ZF (c'est un théorème) dans l'autre il est réfutable, et cela selon les règles intuitionnistes (sans raisonnement par l'absurde). Exemples :

Le premier se paraphrase en français ainsi : tout ordinal fini est soit vide, soit le successeur d'un ordinal fini. Le second se paraphrase ainsi : tout ensemble est soit vide, soit le successeur d'un autre. Tu remarqueras, au passage, que le français est tout à fait apte à exprimer de tels énoncés, sans recourir à un symbolisme quelconque. ;-)

Le premier est trivialement vrai, le second est trivialement faux dans ZF. Le premier exprime le type de la fonction prédécesseur. En OCaml, on écrirait cela ainsi :

type nat =
 | O : nat
 | S : nat -> nat
let pred_nat n = match n with
 | O -> O
 | S m -> n
val pred_nat : nat -> nat = <fun>

En Coq, cela se formalise de manière assez similaire :

Inductive Nat :=
 | O : Nat
 | S : Nat -> Nat.
Fixpoint pred x :=
 match x with
 | O => O
 | S n => n
 end.
(* j'y adjoins la preuve du théorème *)
Theorem pred_spec :
 forall (n : Nat), n = O \/ exists (m : Nat), n = S m.
Proof.
intro n.
destruct n.
- left; reflexivity.
- right; exists n; reflexivity.
Qed.

Ici la fonction pred est sous-spécifiée (elle a pour type Nat -> Nat), mais on pourrait lui donner un type plus précis analogue à ce qu'exprime le théorème, qui est la traduction en Coq du premier énoncé pour ZF. En revanche les contraintes de typage statique de l'un ou l'autre langage ne permettent pas d'exprimer le second énoncé. Contrairement à Python :

>>> def pred(x):
... if type(x) == int :
... if x == 0:
... return 0
... else:
... return x - 1
... else:
... return "not an int"
... 
>>> pred(2)
1
>>> pred("a")
'not an int'
>>> pred_unsafe = lambda x: x - 1
>>> pred_unsafe("a")
Traceback (most recent call last):
 File "<stdin>", line 1, in <module>
 File "<stdin>", line 1, in <lambda>
TypeError: unsupported operand type(s) for -: 'str' and 'int'

La fonction pred avec vérification dynamique de type s'apparente au premier énoncé, tandis que la seconde fonction pred_unsafe s'apparente au second.

J'espère que la chose te semble plus claire maintenant. Il vaudrait mieux, du moins, car c'est une promenade de santé par rapport au problème du rapport entre le kantisme et ce qu'il entend par réalité. Ma réponse à ce sujet viendra plus tard, peut être ce midi ou en fin de journée si je trouve le temps qu'il faut pour la rédiger.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.