Notation et existence implicite

Malheureusement, la réponse est décevante: ça dépend. En maths on utilise des abréviations, et parfois on utilise une même abréviation pour deux choses qui ne sont pas équivalentes, mais ne sont équivalentes que quand elles sont "utilisées dans les contextes où on veut les utiliser de toute manière".

Ici, c'est le cas: lorsqu'on a une fonction $f$ où $f(x) = z$ est défini par une formule (ici $z=\frac{1}{x}$ est défini par $\varphi(x,z) := (xz =1)$), et une propriété $P$, $P(f(x))$ peut vouloir dire deux choses : ou bien "il existe $z$ tel que $z=f(x)$ et $P(z)$", ou bien "pour tout $z$ tel que $z=f(x), P(z)$".

Lorsque $f(x)$ est défini en $x$, et de manière unique (i.e. "il existe un unique $z$ tel que $\varphi(x,z)$"), les deux formules sont équivalentes et donc on n'a pas de problème pour écrire $P(f(x))$.

Par contre, lorsque $f$ n'est pas définie en $x$ (i.e. il n'y a pas de $z$ tel que $\varphi(x,z)$), les deux ne sont plus équivalentes, et donc la réponse à "est-ce que $P(f(x))$ ?" n'est plus claire : c'est exactement ta situation ici, tu demandes si "est-ce que, pour $b=0$, $\frac{a}{b} = 0$ ?". La réponse est "ça dépend de ce qu'on entend ici par cette abréviation".

C'est une des raisons pour lesquelles on essaie de faire gaffe quand on écrit $\frac{a}{b}$ :-D C'est le danger des abréviations (ou du non typage)

Moi je croyais (enfin Christophe m'a dit) que $a/b = \{x \ \vert \ xb = a\}$. Si $b=0$, c'est vide, et sinon c'est un singleton, et on admet l'usage qui consiste à confondre, de temps en temps, un singleton et sa réunion (son seul élément).

Et puis il faut un mécanisme syntaxique de construction d'ensemble: $P\mapsto \{x|P(x)\}$ ou plutôt pour éviter les ennuis: $E,P \mapsto \{x|x\in E \wedge P(x)\}$. Je ne dis pas que c'est impossible de faire ça mais bonne chance pour le décrire proprement. Il y en a un dans les topos par exemple, et il y a des dizaines de pages à lire pour comprendre ce qui se passe.

Oui Thierry, cependant si on n'a pas $\tau$, comment fait-on?

@Cloud, je réponds à ton premier post. L'implication de droite à gauche ne te posant pas de problème, je regarde l'implication que la négation de droite vers la négation de gauche.

Elle dit (j'utilise $\to$ pour l'implication):

$$ (a\neq 0\to \frac{a}{b} \neq 0)\ et \ (b=0\to \frac{a}{b} \neq 0)$$

Qu'en penses-tu?

@christophe c
C'est plutôt: "il faut pouvoir écrire le chat dans le langage X", si on me répond "bin le chat en prose" je n'obtiens pas ce que je veux.

@Foys: menfin, ce n'est rien d'autre que $\mapsto$^, non? On en a souvent parlé.
Au commencement de tout il y a l'égalité (comme si c'était en dur) de
$$
( u\in \{x\mid R(x)\} )= R(u) $$ ainsi que de $$ [(x\mapsto R(x))(t) ]= R(t)

$$
@Martial:
$(R(\varepsilon sR(s)) \to[\forall x: R(x)]$
$\forall x [R(x)\to (R(\tau yR(y)))]$
ou faut peut-être intervertir, je ne me rappelle pas. L'un choisit un élément $x$ tel que $R(x)$ si possible et l'autre tel que $non(R(x))$ si possible.

Merci Foys pour ces explications.

Mais il y a toutefois un truc qui me chiffonne : dans ta théorie K il y a un axiome qui dit en substance que l'univers est en bijection avec les ordinaux (ce qu'on appelle aussi le principe du choix, ou l'axiome du choix global, que je noterai PC dans la suite).

Tu dis que K est une extension conservative de ZFC. OK. Mais il me semblait avoir compris que ZFC + PC a une consistency strength supérieure à celle de ZFC. Est-ce faux ?

Oui; ce n'est pas Gödel qui avait obtenu la consistance relative de V=L par rapport à ZF et avec ce résultat, cons(ZFC+HC) à partir de cons(ZFC)? (édité)

http://www.les-mathematiques.net/phorum/read.php?16,2202464,2202974#msg-2202974

Foys: je ne comprends pas ce que tu demandes (ou plutôt "veux") en fait.

Puisque tu connais, c'est juste la beta-reduction du lambda calcul. Ou (pour éviter les lettres (variables)) tu prends les combinateurs usuels (ou un jeu complet)

:-S

A moins que tu ne parles des axiomes, sinon, je ne vois pas.

Foys, Christophe: vous avez la même discussion à chaque fois, et à chaque fois vous ne parlez pas de la même chose :-D c'est un peu un dialogue de sourds. Je sais bien que Christophe n'est pas forcément super clair quand il parle de ce sujet (*), mais c'est évident, au moins après 3-4 répétitions (et il y en a eu plus) qu'il ne parle pas de la même chose.

(*): désolé Christophe ;-) si ça te rassure je te comprends de plus en plus, j'ai le projet d'essayer de clarifier ce que tu dis un de ces jours pour que tout le monde puisse te comprendre et qu'on puisse enfin avoir des discussions où toutes les parties parlent de la même chose.

@Foys, étant sur mon pc, je te donne quelques détails, puisque tu as exhibé une expertise en LC ça va être assez court. Je ne traite que la logique classique (enfin in some sense).

Comme tu sais tu as tout avec $W,K,C$ (je sais que tu préfères $S,K$ parfois, mais peu importe, je ne vais pas détailler et j'appelle $C$ le combinateur tel que $\forall u,v,t : Cuvt = v(ut)$

Par contre tu n'as ni l'égalité, ni le $\forall$, et, comme il est célèbre, l'un des deux amène l'autre, donc il suffit d'avoir disons $=$, que je vais noter $E$.

Reste à prendre la convention habituelle qui est que

$abc$ signifie $[if$ $a$ then $b$ else $c]$ quand $a$ est un booléen, faisant de $V:=K$ une représentation de vrai et de $F:=KJ$ une représentation de faux (tu peux prendre $J:=CKW$ ou l'éjouter, bref.

Ainsi, tu le sais, mais ça ne coute rien de l'écrire $Vxy=x$ et $Fxy=y$, on pourrait les appeler "gauche" et "droite" :-D mais ce serait faire de la pub à la gauche, ce qui n'est pas mon intention.

Je sais que tu sais implémenter $\mapsto$, donc dans la suite je l'utilise.

1/ tu as le combinateur quelque soit comme suit: $(\forall r ) := [Er(KK)]$

(je te laisse calculer $r\mapsto Er(KK)$

2/ Quand tu veux parler de $\{x\mid R(x)\}$, bin c'est juste $x\mapsto R(x)$ en fait,

3/ La négation $non$ est le combinateur $x\mapsto xFV$ (littéralement $x\mapsto [$ if $x$ then $faux$ else $vrai]$

4/ Ton "malaise" si j'ose dire c'est qu'il existe (facilement) $a$ tel que $a=non(a)$. Mais tant que tu focaliseras sur ça, tu risques de gaspiller de l'énergie à mon sens. On ne sait pas si l'arithmétique, ni même des formes plus faibles est / sont consistante(s). Alors tu pense bien que ZF.

5/ Je rappelle que l''axiome du choix est un axiome de compréhension parmi d'autre MODULO l'extensionalité, mais tu peux l'ajouter en dure avec une nouvelle lettre $L$ et l'axiome

$$ \forall (x\mapsto [\forall (y\mapsto [ x(Lx) (xy) K ])]) $$

par exemple (j'ai utilisé l'implication $(x\to y):=xyK$).

Etc, etc...

6/ J'ai toujours dit, mais j'en profite pour le redire qu'il n'y a pas de théorème, il n'y a que des preuves au sens où les habitudes un peu "arriérées" et provenant de notre passé (et hélas présent) bigot nous ont un peu trop conditionné à des "théories" qui n'ont en fait aucune importance autre que de raccourcir les listes d'admis D'UNE PREUVE (mais une preuve dans ZF n'utilise jamais une grande puissance de ZF par exemple)

Les contradictions connues donnent la taille des objets qui sont aussi gros que la logique est infaillible (aurtement dit donnent la taille de $\frac{1}{0}$)

Ainsi en va-t-il de $ON$ ou de $\{x\mid x\notin x\}$. Ca n'a rien de bien transcendantal, c'est juste une réécriture de

$$ \frac{1}{0} \times 0 = 1$$

mais c'est probablement intéressant pour un futur scientifique débarrassé de ses TOCS au sens où l'étude de "ces combats de titans" pourrait en être facilitée, même on ne voit pas bien ce qu'étudier la puissance de Dieu peut a priori apporter à un progrès des ingénieurs dans les usines de voitures et d'avions.