Langage ensembliste de base avec définitions. — Les-mathematiques.net The most powerful custom community solution in the world

Langage ensembliste de base avec définitions.

Modifié (27 Apr) dans Fondements et Logique
$\newcommand{\s}{\bullet}$
$\newcommand{\o}{\blacksquare}$
$\newcommand{\a}{\mathbf A}$
$\newcommand{\e}{\mathbf E}$
$\newcommand{\d}{\mathbf D}$
Préambule:
Ce fil a pour vocation à présenter une version implémentable (à quelques problèmes de complexité près qui peuvent être problématiques du point de vue de l'informatique mais négligeables du point de vue des fondements) et complète du langage de la théorie des ensembles formelle, avec un nombre de notions de base le plus petit possible.
Conformément à sa conception des mathématiques non comme une nouvelle doctrine (religion ?) à imposer mais comme un service dont les usagers peuvent employer les éléments comme ils le veulent, l'auteur refuse fermement toute forme de militantisme et, pour autant qu'il sache, livre des définitions compatibles avec la théorie des ensembles courante.
La totalité de ce qui est dit dans ce message concerne la logique classique (la seule à ma connaissance qui est vraiment utilisée en théorie des ensembles, les autres, intuitionniste, linéaire étant destinées à d'autres types de fondements -quoi qu'on dise, par exemple, COQ n'est pas une théorie des ensembles- ou bien de façon marginale).

#######################

Dans ce message il n'est question que de définitions de formules et d'éléments syntaxiques. Les systèmes de preuves seront discutés plus tard (des choses telles que "qu'est-ce qu'un théorème" etc, si j'ai le temps/la motivation ...)

######################
Dans ce qui suit, le mot "numéro" désigne exclusivement une suite de symboles destinée à enrichir l'alphabet.
Précisément, un numéro est:
-$\o$
-une suite de caractères constituée de $\s$ et d'un numéro placé à sa droite; la suite obtenue sera appelée "successeur" dudit numéro.
-étant donnés deux numéros $a,b$, si $a$ apparaît dans la liste des étapes de formations de $b$ on dira que "$a$ est inférieur à $b$" (on dira aussi "strictement inférieur à $b$" lorsque de plus $a$ et $b$ ne sont pas identiques).

Si $n$ est un numéro, la notation "$n+1$" pourra également être utilisée pour désigner le successeur $\s n$ de $n$.
De même des notations "familières" telles que "$0$" pour $\o$, "$1$" pour $\s \o$, "$2$" pour $\s \s \o$ pourront être employées.

Exemples: $\o$, $\s \o$, $\s \s \s \o$ sont des numéros (notés habituellement "$0,1,3$").

Dans la suite, le mot "lettre" désignera des lettres de l'alphabet, à l'exclusion de $\a,\d,\e$ qui sont des constantes réservées à un usage ultérieur, ou bien des assemblages syntaxiques de la forme $a_{k}$ où $a$ est une lettre et $k$ un numéro (appelé souvent "indice").

Etant donné un numéro $n$, les $n$-formules sont des suites de caractères obtenues à l'aide des règles suivantes:

1°) si $\bf x,y$ sont des lettres ou bien des numéros strictement inférieurs à $n$, $\e \bf x y$ est une $n$-formule
2°) si $\Psi,\Theta$ sont des $n$-formules, $\d \Psi \Theta$ est une $n$-formule.
3°) si $\Phi$ est une $n+1$-formule, $\a \Phi$ est une $n$-formule.

[size=x-small](NB: apartés techniques
(i) cette manière d'implémenter les variables liées s'appelle "indices de Bruijn". Voyez un moteur de recherche
(ii) toutes les formules dont nous parlons sont donc en notation polonaise. Mais nous introduirons rapidement des notations parenthésées. Il n'y a pas lieu d'écrire les formules sans abréviation -c'est même matériellement impossible au vu des éléments premiers que nous avons choisis ici pour fonder le langage formel tant le nombre de caractères nécessaire pour écrire la moindre formule non triviale serait grand-, mais l'intérêt de faire ce genre de présentation est de dire vraiment au moins une fois ce que sont les objets de base des mathématiques).[/size]

-Certaines simplifications syntaxiques seront utilisées dans la suite. Par exemple lorsque $\bf a$ et $\bf b$ sont des numéros ou des lettres on notera "$(\bf a \in b)$" ou même "$\bf a \in b$" au lieu de $\e \mathbf a \mathbf b$. Cette formule se lit "$\bf a$ appartient à $\bf b$".

-Soit $\Phi$ une $0$-formule et $\mathbf x$ une lettre.
On note $\{\mathbf x:\Phi\}$ la $1$-formule obtenue en remplaçant dans $\Phi$ tous les numéros par leurs successeurs, et toutes les occurrences de $\mathbf x$ par $\o$.
On désigne par $\forall x\Phi$ la formule $\a \{\mathbf x : \Phi\}$. Cette formule se lit "pour tout $\mathbf x,\Phi$".

IMPORTANT: Noter que $\{\mathbf x : \Phi\}$ et $\forall \mathbf x \Phi$ sont des suites de caractères (lorsque toutes les abréviations sont retirées) où la lettre $\mathbf x$ ne figure pas.

- Les $0$-formules (i.e. les $\o$-formules) seront simplement appelées "formules".

-Etant donné deux formules $P,Q$, la formule $\mathbf DPQ$ est destinée à signifier intuitivement que $P$ et $Q$ ne sont pas toutes les deux vraies; $\d$ se note "Nand" dans un contexte informatique.
On emploiera les notations (abréviations) suivantes pour toutes formules $\Psi,\Theta$ et toutes lettres $\bf z,w,v$:
"$(\Psi|\Theta)$" pour $\d \Psi \Theta$
"$\Psi \Rightarrow \Theta$" pour $(\Psi|(\Theta|\Theta))$ (on dit "$\Psi$ implique $\Theta$")
"$\neg \Psi$" pour $(\Psi|\Psi)$ (on dit "non $\Psi$")
"$\Psi \vee \Theta$" pour $(\neg \Psi) \Rightarrow \Theta$ (on dit "$\Psi$ ou $\Theta$")
"$\Psi \wedge \Theta$" pour $\neg (\Psi | \Theta)$ (on dit "$\Psi$ et $\Theta$")
"$\Psi \Leftrightarrow \Theta$" pour $(\Psi \Rightarrow \Theta) \wedge (\Theta \Rightarrow \Psi)$ (on dit "$\Psi$ équivaut à $\Theta$").
"$\exists \mathbf z \Psi$" pour $\neg (\forall \mathbf z (\neg \Psi))$
"$\mathbf v \notin \mathbf w$" pour $\neg (\mathbf v \in \mathbf w)$.

Exemples: les formules
(1) $\forall x ((x \in a \wedge x \in b) \Rightarrow x \in c)$
(2) $\forall y \neg (y \in x)$
(3) $\exists y \forall x \neg(y \in x)$ (qui signifient respectivement intuitivement que "$c$ contient l'intersection de $a$ et de $b$", "$x$ est vide", "il existe un ensemble vide") sont en fait sous forme non abrégée, les formules suivantes:

$$\a \d \d \d \e \o a \e \o b \d \e \o a \e \o b \d \e \o c \e \o c \tag 1$$
$$\a \d \e \o x \e \o x \tag 2$$
$$\d \a \d \a \d \e \s \o \o \e \s \o \o \a \d \e \s \o \o \e \s \o \o \a \d \a \d \e \s \o \o \e \s \o \o \a \d \e \s \o \o \e \s \o \o \tag 3$$

Remarque: la formule (2) est identique à la formule $\forall t \neg (t \in x)$. La lettre $x$ est la seule qui figure dans cette formule. De même la formule (3) ne contient aucune lettre (à nouveau $\a,\d$ et $\e$ ne sont pas considérées comme des lettres mais sont des constantes du langage) et cette formule est identique, une fois les abréviations enlevées, à $\exists v \forall w \neg (w \in v)$.
Une formule ne "parle" que des lettres qui apparaissent dans elle (!!!).

Autres définitions:

Substitution de variables:
Si $n$ est un numéro, $\Psi$ une $n$-formule et $\bf x,t$ deux lettres, on désigne par $(\Psi [\mathbf x:= \mathbf t])$ (parenthèses facultatives si aucune confusion n'est à craindre) la formule obtenue en remplaçant dans $\Psi$, chaque occurrence de $\mathbf x$ par $\mathbf t$.

-Une classe est une 1-formule.

-Si $\Phi$ est une classe et $\mathbf y$ une lettre, $(\Phi(\mathbf y))$ (ou $\Phi(\mathbf y)$ ou même $\mathbf y \in \Phi$ si aucune confusion n'est à craindre) est la formule obtenue en remplaçant dans $\Phi$, chaque numéro par son prédeceseur s'il est non nul, et par $\mathbf y$ s'il est nul. Le prédecesseur du numéro $\s n$ n'est rien d'autre que $n$.

NB: Si $\Gamma$ est une formule et $\bf t,u$ des lettres, $\{\mathbf t : \Gamma\}(\mathbf u)$ est l'énoncé$ \Gamma[\mathbf t:= \mathbf u]$

###############################

Autres abréviations courantes des maths:

A1) Soit $\Phi$ une classe et $\mathbf x$ une lettre.
On abrège par "$ens (\Phi,\mathbf x)$" l'énoncé "$\a \left (\Phi \Leftrightarrow (\o \in \mathbf x) \right )$". Cet énoncé se lit "$\Phi$ est l'ensemble $\mathbf x$".
On voit donc que lorsque $\mathbf z$ est une lettre différente de $\mathbf x$ et ne figurant pas dans $\Phi$ , l'énoncé $ens(\Phi,\mathbf x)$ se réecrit $\forall \mathbf z \left ( \Phi(\mathbf z) \Leftrightarrow \mathbf z \in \mathbf x\right )$
Dans le cas particulier où $\Phi$ est introduite sous la forme $\{\mathbf t : \Gamma\}$ avec $\mathbf t$ une lettre différente de $\mathbf x$ (NB: on peut toujours se ramener à cette situation puisque si $\mathbf s$ est une lettre ne figurant pas dans $\Gamma$ et différente de $\mathbf s$, les classes $\{\mathbf t:\Gamma\}$ et $\{\mathbf s :\Gamma[\mathbf t := \mathbf s]\}$ sont identiques), on voit avec les conventions précédentes que $ens (\mathbf x, \{\mathbf t : \Gamma\})$ est l'énoncé $\forall \mathbf t \left (\Gamma \Leftrightarrow \mathbf t \in \mathbf x\right )$.

A2) On note pour toute classe $\Phi$, $Ens(\Phi)$ l'énoncé $\exists x, ens(\mathbf x,\Phi)$ où $\mathbf x$ est une lettre ne figurant pas dans $\Phi$ (cet énoncé se lit "$\Phi$ est un ensemble").

Un célèbre théorème de logique dû à Russell dit que $\{x : x \notin x\}$ n'est pas un ensemble.

A3): Soit $\Phi$ une classe et $A$ une lettre ou une classe.
On pose $\Phi \in A:=\exists \mathbf z\left (ens(\mathbf z,\Phi) \wedge \mathbf z \in A\right )$ (cf notation bleue plus haut quand $A$ est une classe). Ainsi on a défini $A\in B$ quand $A$ et $B$ sont des lettres ou des classes et on a étendu le langage de la théorie des ensembles. On pourra consulter "Introduction to axiomatic set theory" de Takeuti et Zaring pour un exposé détaillé de cette approche.

A4) si $A$ est une classe, $\Phi$ une formule et $\mathbf x$ une lettre,
$\forall \mathbf x\in A,\Phi$ abrège $\forall \mathbf x, (\mathbf x \in A \Rightarrow \Phi)$ et
$\exists \mathbf x\in A,\Phi$ abrège $\exists \mathbf x, (\mathbf x \in A \wedge \Phi)$.

A5) Soient $A,B$ des lettres ou des classes. (":=" veut dire "on définit ...").
On définit donc:
$A\subseteq B:= \forall x (x \in A \Rightarrow x \in B )$
$A=B:= A \subseteq B \wedge B \subseteq A$
$\{A,B\}:= \{x: x = A \vee x = B\}$
$(A,B):= \{\{A\},\{A,B\}\}$
$\mathcal P(A):= \{x : x \subseteq A\}$
$\bigcup A := \{x : \exists y, y \in A \wedge x \in y\}$
$A \cap B:= \{x: x \in A \wedge x \in B\}$
$A \cup B:= \{x: x \in A \vee x \in B\}$
$A \backslash B:= \{x : x \in A \wedge x \notin B\}$
$\{x\in A\mid \Phi\}:= \{x : x \in A \wedge \Phi\}$ où $\Phi$ est une $0$-formule.
$dom(A):= \{x: \exists y, (x,y) \in A\}$
$im(A):=\{y: \exists x, (x,y) \in A\}$
$Graphe(A):=\forall c \in A, \exists x \exists y, (x,y)=c)$ (NB: en fait par construction, les lettres qui suivent les quantificateurs ne peuvent pas désigner autre chose que des ensembles).
$Fonction\_ensembliste (A):=Graphe(A) \wedge \forall x \forall y \forall z, \left ((x,y) \in A \wedge (x,z)\in A\right) \Rightarrow y = z$.
$A \times B:= \{c:\exists x \in A, \exists y \in B, c=(x,y)\}$
$B^A:= \{f:Fonction\_ensembliste(f) \wedge dom(f)=A \wedge im(f) \subseteq B\}$
$x \in A \mapsto B := \{u: \exists x \exists y(u=(x,y) \wedge x \in A \wedge y = B )\}$ ($x,y,u$ étant distinctes, $x$ ne figurant pas dans $A$, $y$ ne figurant ni dans $A$, ni dans $B$, $u$ ne figurant ni dans $A$, ni dans $B$).

Réponses

  • Ta générosité me sidère.

    Mais ne crois-tu pas que tu devrais (et tu ferais des économies !!!) la version contradictoire (toute collection est un ensemble) et en plus sans variable (les combinateurs).

    Si je m'embarquais dans une volonté de partager comme la tienne, c'est ce que je ferais.

    C'est BEAUCOUP PLUS SIMPLE, même si long, on peut sauter des lignes et écrire directement des formules sans lâcher personne et la fin, tu rattrapes tout ce qui est contradictoire "en une seule fois" (les "grosses collections sont aussi fortes que Dieu et cassent la logique").

    Parce que à mon avis, au final, la formalisation de "toute petite collection est un ensemble" (autrement dit ZF) restera ÉTERNELLEMENT + ou - illisible (autrement dit tu feras plaisir à des gens qui connaissent déjà).

    Je pense profondément que ce n'est pas pour rien que l'évitement du contradictoire complique GRANDEMENT les écritures, MÊME INTRODUCTIVES des théories : c'est exactement comme pour les pointeurs : c'est ultra simples, mais si tu veux implémenter des compilateurs qui n'acceptent que les sans boucle, c'est ultra galérien.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • C'est bien c'est très condensé en effet, c'est moins raide qu'il n'y parait d'un premier abord mais il faut bien s'accrocher - enfin j'ai sans doute bien plus de mal que les pros :-)

    Excuse mon ignorance Christophe, je ne comprends pas ton allusion à Dieu et aux grosses collections.
  • christophe c a écrit:
    Mais ne crois-tu pas que tu devrais (et tu ferais des économies !!!) la version contradictoire (toute collection est un ensemble)
    Je pense avoir répondu à cette objection (que j'avais anticipée :-D) dans mon préambule.
    En gros:
    1°) D'abord il n'est pas vrai que je peux faire apparaître des éléphants volants dans ma chambre en 3 secondes. Le vrai monde n'est pas contradictoire !!! Il exhibe à la marge des bizarreries (si tu veux parler de MQ faut-il rappeler que parmi ses modèles il y a celui unimonde de l'expérience vécue d'un individu) mais c'est tout.
    2°) Le texte vise explicitement à fournir un manuel de la théorie des ensembles telle qu'elle est pratiquée, c'est-à-dire ZF.
    -La "théorie cc" avec lambda calcul et "ensemble = prédicat" est contradictoire en 2 lignes.
    -La théorie des ensembles ZF n'a toujours pas été prouvée contradictoire après 90 ans d'existence et pourtant des tentatives dans ce sens. Ce ne sont pas les mêmes théories. Moi j'ai dit que je faisais la seconde et ce n'est pas la première.

    De plus le paradoxe de Russell n'est pas à proprement parler un théorème de théorie des ensembles, mais un théorème général de logique du premier ordre (et encore ...) valable dans toutes les situations où il y a au moins un symbole de relation à deux arguments $R$; il s'énonce: $\forall u \neg (\forall x (R(x,u) \Leftrightarrow \neg R(x,x)))$ et se démontre avec des moyens minimalistes (intuitionnistes voire en logique minimale si on insiste pour remplacer $\neg$ par un $(\_ )\Rightarrow P$).

    La logique du premier ordre est consistante (la construction de modèles concrets est un non-problème; $R(a,b)$ pourrait très bien désigner "le fichier $a$ appartient à la base de donnée (un cas particulier de fichiers) $b$" par exemple; une base de donnée des bases de données qui ne s'appartiennent pas elles-mêmes n'existe pas et ça ne va pas plus loin que ça).
    En fait ce théorème énonce une limitation irréductible du langage. Le schéma de compréhension non bridé est faux à jamais. On ne pourra jamais avoir "ensemble = propriété".
    christophe c a écrit:
    et en plus sans variable (les combinateurs).
    :-D Alors c'est la mort dans l'âme que j'ai dû renoncer à mon langage formel préféré (les combinateurs).
    Mais à nouveau le but du texte est d'introduire les outils de la théorie des ensembles courante et celle-ci est du premier ordre alors que le lambda calcul/les combinateurs ne le sont pas.
    La sémantique d'une théorie du premier ordre est essentiellement triviale (modèles ensemblistes avec symboles de relation) alors que celles des LC non typés a mis des décennies à être découverte (modèles de Scott; modèles de Plotkin etc) donc on peut se demander de quoi on parle avec les termes de ces théories.
    Après on pourrait se focaliser sur des solutions typées mais elles peuvent apparaître ad-hoc (on met 3 constantes $all$, $in$, $nand$ dans le langage et on dit que les formules sont le plus petit ensemble $F$ de lambda termes contenant $in(x)(y)$ pour toutes lettres $x,y$ et tel que pour tous $A,B\in F$ et toute lettre $x$, $nand(A)(B)$ et $all (\lambda x.A)$. Il y a peut-être quelques justifications à faire pour établir le bien fondé du truc: confluence, les termes sont typables et donc fortement normlisants etc. Sauf que va manipuler ça dans un programme informatique; sans même parler de prouveur).

    De toute façon il y a deux rôles pour les langages en tout genre:
    1°) pour donner des ordres: on parle de langage de programmation et la récursivité estt souhaitable (et encore pas toujours: les programmeurs de la NASA n'ont pas le droit à la Turing complétude pour les logiciels d'appareils à plusieurs milllions de dollars qu'on envoie dans l'espace: un bug et c'est la cata).
    2°) pour décrire le monde (de façon fiable, par exemple dans un cadre scientifique): à nouveau le vrai monde n'est pas contradictoire. Donc la récursivité c'est niet et bridage/types sont absolument la norme: ce n'est pas parce qu'on peut parler de comment on peut soulever la tour Eiffel avec une seule main que ceci peut arriver dans le monde réel.
  • Ci-dessous, un lien vers un programme coq implémentant la logique du premier ordre générale que j'avais rédigé il y a quelque temps, et dont le message initial de ce fil présente en fait un cas particulier.

    Le code compile avec COQ 8.9 (il y a des versions plus récentes mais avoir des programmes à jour sous debian est infernal; ça ne devrait pas poser de problèmes en principe).

    https://pastebin.com/KfCCrVhd

    Au menu:
    -définition des formules du premier ordre sur une signature donnée
    -déduction naturelle classique
    -interprétation dans un modèle (théorème de correction).
  • @foys, je t'ai bien lu, ne t'inquiète pas, je te fournirai une réponse détaillée. Merci pour ta réponse.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Foys, je vais rtès vite car ne peux faire autement et j'utilise le fait que tu es très intelligent pour te prier de déplier le caractère provocateur et parodique que je vais utiliser pour diviser par 10 la longueur du propos.

    D'abord il n'est pas vrai que je peux faire apparaître des éléphants volants

    Il n'est pas non plus vrai que tu tires du th de Gales Stewart une méthode pour être invincible aux échecs ou que tu perçois VRAIMENT la finitude de $U(99,99)$ avec la $U:=AckermannFuntion$. Ce n'est pas du tout un argument. On fait des maths pour étudier ce que sont les paysages de Gattaca à l'avance, ou le paradis quand on ira y vivre.
    telle qu'elle est pratiquée, c'est-à-dire ZF.

    Justement, ce que je te propose c'est bien ce qui est pratiqué, en un sens très profond.
    La "théorie cc" avec lambda calcul et "ensemble = prédicat" est contradictoire en 2 lignes.

    Ce qui est bien avec toi, c'est que le contradictoire est une vraie phobie idéologique, et en fait, tu serais Superman, quand on te connait si tu n'avais pas quelques blocages idéologiques très gratuits.

    Je te rappelle que les maths recensent DES CHEMINS et que ceux qui mènent du paradis vers ce que tu veux ne constituent pas des problèmes, ni ne semblent interférer avec ceux qui mènent au paradis. Qu'on sache aller au paradis en 2 lignes avec un téléporteur qui n'est fabriqué qu'au paradis n'est pas un problème. La philosophie ZF est très exactement "la bonne" en terme de simplicité puisqu'elle identifie l'incassabilité logique avec la taille des collections qui permettent de prouver que $0=1$ (ie d'aller au paradis. -

    Le schéma de compréhension non bridé est faux à jamais. On ne pourra jamais avoir "ensemble = propriété".

    C'est un ensemble d'axiomes, et oui "à jamais" dedans il y en a qui mènent au paradis. Merci d'avouer la non relativité de la force des maths.
    Alors c'est la mort dans l'âme que j'ai dû renoncer à mon langage formel préféré

    Mais justement, normal, tu refuses le contradictoire, donc ce qu'on fait depuis toujours qui est un cas particulier DEPUIS TOUJOURS d'un principe, tu le reconnais, qui est contradictoire. Ton refus d'aller au paradis te fait ressentir insconciemment le gout désagréable qu'a le fait de se tirer volontairement une balle dans le pied.
    le lambda calcul/les combinateurs ne le sont pas.

    Si si bien sûr, ce n'est pas académique, mais si on l'instituait, c'est même une théorie très simple qui ramène tout au calcul
    a mis des décennies à être découverte

    Pas du tout. On le pratique depuis toujours et on a mis des millénaires à avoir des psychanalystes, ça n'a rien à voir. Toutes nos définitions depuis la nuit des temps sont des "lambda x: blabla"
    à nouveau le vrai monde n'est pas contradictoire. Donc la récursivité c'est niet

    Et après tu dors mal.

    1/ Le vrai monde mène ou ne mène pas au paradis, on n'en trop rien, mais s'il y mène il est contradictoire (une contradiction n'étant rien d'autre qu'un itinéraire pour aller d'un endroit au paradis)

    2/ Prétendre que le vrai monde ne mène pas au paradis me prait présomptueux et spéculalitf

    3/ Au fond de toi, alors même que tu l'as étudiée et mieux comprise que bcp de chercheurs dont c'est le métier, la CCH (au sens général) est traitée par toi comme une personne qui aurait acheté une lampe d'Aladin et refuse avec beaucoup d'autoritarisme de la frotter "je la pose là, n'y touchez pas".


    Voilà, pardon de ne pas être plus "sérieux" dans ma réponse, je pense t'avoir mis tout ce qui permet de DEVINER après traduction ma réponse. Je reviendrai détailler si je dégage un peu de dispo. Et même définir la théorie complète en quelques lignes dont je parle pour éviter le vague.

    Attention, pour toi-même ne tombe pas dans le piège des TRES NOMBREUX défauts supplémentaires de cette forme de réponse condensée pour construire des objections artificielles.

    J'attire ton attention sur le fait qu'il faut traiter TES DEUX PARTIES de post CONJOINTEMENT. Il y a un "marché" : on accepte "le contradictoire" en paiement "d'un service rendu par le tout combinateur simplifiant"
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • @foys, je m'adresse toujours à toi (autrement dit, en sachant que tu connais ces choses), mais précise un peu plus formellement ce que tu pourrais faire si tu te "libérais" de ton envie de rester dans le spéculé-non-contradictoire.

    1/ Comme tu sais, on fait tout le langage avec $W,C,K$. Mais on ne réalise pas le platonisme.

    2/ Je rajoute donc un signe, que je note $P$ tel qu'on veut que $Pab$ signifie $b\subset a$

    3/ L'égalité est définie par $(a=b) := ((et) (Pab)(Pba))$, le combinateur "et" étant facile à décrire avant

    4/ Tu as alors le combinateur $\forall$, sous la forme $\forall :=(u\mapsto Univers \subset u)$, autrement dit $\lambda u: Pu(KK)$

    5/ etc.

    6/ Toutes les preuves deviennent alors de simples calculs, et comme tu le sais il est facile de voir quand est-ce qu'on utilise un "outil trop puissant" dans une preuve (au même titre qu'une preuve dans le schéma $\forall R\exists a: ([x\in a]\iff [R(x)])$ ne peut jamais cacher l'éventuelle utilisation de collections trop grosses.

    7/ Toi, tu le sais, mais je rappelle les bases booléennes:

    7.1/ Le vrai est défini par $V:=K$

    7.2/ Le faux est défini par $F:=(KJ)$

    7.3/ L'implication $a\to b$ est définie par $abV$

    7.4.1/ La conjonction $a$ et $b$ est définie par $abF$

    7.4.1/ La disjonction $a$ ou $b$ est définie par $aVb$

    7.5/ La négation $non(a)$ par $aFV$

    7.6/ Dans le contexte booléen, $abc$ se lit "if $a$ then $b$ else $c$" (on n'est jamais déçu)

    7.7/ Dans le contexte général, $ab$ se lit $b\in a$

    7.8/ Ca tombe bien car $Pa$ est l'ensemble des parties de $a$

    7.9/ J'ai déjà parlé de $\forall$

    7.10/ Tu n'as aucun axiome de compréhension à ajouter, puisque le calcul fait tout tout seul, par contre, tu as des axiomes de gestions, ainsi que l'extensionalité.

    8/ Pour les lecteurs autres que foys, je vous donne la définition de $x\mapsto blabla$ :

    8.1/ Elle est récursive et se calcule comme suit:

    8.2/ $[x\mapsto ((u)(v))] := [W(C(u')(C(v')))]$ avec $(u',v') := ([x\mapsto u],[x\mapsto v])$

    8.3/ Quand la lettre $x$ ne figure pas dans $u$, on peut directement écrire $[x\mapsto u] := Ku$

    8.4 $[x\mapsto x] := J := (WK)$ (par exemple, mais on peut rajouter "en dur" un combinateur $(Jx:=x)$)

    9.1/ Sur le rôle des parenthèses : j'ai respecté un principe de confort, mais en toute rigueur, il faudrait utiliser l'écriture polonaise et ajouter la lettre Majuscule "A", et comprendre $uv$ comme $Auv$.

    9.2/ l'écriture polonaise a en effet l'avantage que TOUTE SUITE DE CARACTERES est parsable avec ajout de conventions ultrasimples (mettre ou enlever des "A" à gauche, rien de plus). Tandis qu'avec les parenthèses c'est "relou" (exemple la suite $)at(((Kd$ bof bof)

    10/ Ce message était essentiellement pour Foys qui connait le sujet, mais il est paradoxalement plus long que si je voulais tout faire partir de $0$, car il contient une part de clins d'oeil et d'arguments.

    11/ Le slogan à retenir est que toutes les maths s'écrivent avec $A,C,K,P,W$ avec seulement deux signes "platoniciens" : $A,P$, le "A" étant l'habituelle $\in$ de la version classique. De plus le $\{x\mid blabla\}$, qui n'est rien d'autres qu'une présentation poétique de $x\mapsto blabla$ est obtenu au point 8.

    12/ Je fais un item avec les règles de calcul de $C,W,K$ : pour tous $a,b,c$

    12.1/ $Cabc = b(ac)$
    12.2/ $Wab=abb$
    12.3/ $Kab=a$
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Merci d'avoir précisé le système que tu avais en tête Christophe. Il s'agit de la "logique combinatoire illative" introduite par Curry (lui aussi notait "P" l'inclusion inverse)... et presque immédiatement abandonnée par lui puisqu'inconsistante (mais il y a eu des sauvetages plus tard en introduisant du typage, cette notion qui te fait poster des messages indignés de 500 lignes pour expliquer à quel point le monde entier est bête) (on pose $U:= \lambda x \lambda y. y(xxy)$ de sorte que pour tout $f$, $UUf = f(UUf)$; on applique à $f:=\lambda x (x\Rightarrow \perp)$). Ceci est provoqué par le langage lui-même, non par des "collections trop grosses".
    La logique du premier ordre ne contient pas ça.
    La logique du premier ordre avec un seul symbole de relation binaire (et axiome d'extensionnalité) admet des modèles tels que des ensembles ordonnés finis. Ce langage est donc consistant. Les problèmes d'inconsistance ultérieurs éventuels seront donc dûs a des axiomes rajoutés.
    Ces langages ne sont pas les mêmes.
    J'ai dit que je traitais le second, non le premier, de plus si j'avais voulu parler de lambda calcul j'aurais intitulé le post "lambda calcul" ou quelque chose comme ça.

    En plus tu es bien placé pour savoir que les résultats de ZF (ceux techniques, la moitié de tes messages techniques doit leur être consacrés) font REFERENCE SANS ARRET, DE MANIERE CRUCIALE, PRECISE ET INCONTOURNABLE A LA FACON DONT CETTE MEME THEORIE DES ENSEMBLES S'EXPRIME FORMELLEMENT EN LOGIQUE DU PREMIER ORDRE!!!

    ZF n'arrête pas de parler de l'ensemble des formules, de faire des distinctions très fines entre elles, les hiérarchies de formules alternances de quantificateurs, les formules à quantification bornée absolues pour les modèles transitifs,
    le forcing (à un moment il faut donner la définition de choses comme "$p \Vdash F$" et il y a une induction sur la taille de $F$), il y a même "l'ensemble des formules" et des outils sémantiques pour les interpréter.

    Rien de tout ceci n'est possible avec cette chose dont tu sembles vouloir imposer l'usage à la place.
    Ou alors il faudrait donner une traduction algorithmique complète et dûment documentée (alors que remplacer les formules avec $nand$, $\forall$, $\in$ par celles avec le jeu complet de connecteurs logique et vice-versa est trivial et connu de tout le monde).
  • Ah et aussi dorénavant je ne lirai plus les messages prétendant agressivement l'inconsistance d'un système donné et traitant au passage d'imbéciles ou de peureux les sceptiques, sauf dans le cas où le message en question contient une démonstration formelle complète (et juste) de l'inconsistance du système en question.
  • De mon téléphone.

    Je n'ai traité personne d'imbécile. Surtout pas toi comme tu te doutes.

    Mais par contre je ne comprends pas pourquoi tu parles de gens qui déclarent contradictoires des systèmes qui ne le sont a priori pas car je n'en ai pas vu récemment.

    Et non je ne te parlais pas du système de Curry. C'était bien plus simple ce que je te disais : qu'il est inutile de se placer solennellement dans un sous système bridé quand on sait qu'en maths les preuves montrent TOUT ce qu'elles utilisent.

    Les contradictions connues actuellement utilisent TOUTES de manière visible au moins une grosse collection.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Si j'ai un peu de temps demain, je te répondai, car je te trouve un peu "irascible intellectuellement" dans ta réaction, mais n'ai pas le temps de me relire (et surtout pas la vue, je vois tout flou).

    Il me semble qu'il y a un malentendu, je te répondais vraiment dans TON CONTEXTE de fil, à savoir dire à un noéphyte tout le début.

    De ce fait, je te disais que la consistance n'avait pas d'importence et que les combinateurs ne gommaient en rien la distinction entre ZF (n'utiliser que des petites collections dans des preuves) et la TDE non brédée.

    De ce fait, on ne perd rien à présenter même ZF en mode combinateurs.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • @CC, il me semble t'avoir entendu dire à plusieurs reprises que $x \in y$ pourrait être considéré comme une abréviation de $y(x)$.
    Il est clair que l'introduction d'une relation $x \in y$ à part entière entre directement en conflit avec un schéma de compréhension général, d'où les restrictions de ZF.
    Mais après tout, c'est vrai, pourquoi aurait-on impérativement besoin de cette relation pour faire une théorie des ensembles ?

    On pourrait partir d'un domaine d'objets non spécifiés (des sortes d'"urelements") et de relations qui seraient considérées elles-mêmes comme des objets, et dont les arguments dénoteraient des objets de base ou des relations. Les quantifications porteraient aussi sur les relations.
    Les relations s'appeleraient aussi des ensembles. Il semblerait qu'on pourrait alors faire l'impasse des axiomes extra-logiques.
    Par exemple :

    Plus de schéma de compréhension, de remplacement.

    Plus d'extensionalité : a = b, c'est l'énoncé $\forall x $ $ (a(x) \Leftrightarrow b(x)) $

    La paire {a, b}, c'est l'ensemble q(x) : $x = a \vee x = b $

    Le couple (a, b), c'est l'ensemble c(x, y) : $ x=a \wedge y=b$

    Le produit cartésien A x B, c'est l'ensemble C(x, y) : $ A(x) \wedge B(y) $

    L'ensemble des parties de A, c'est l'ensemble p(x) : $ \forall y $ $ (x(y) \Leftrightarrow \forall z $ $ (y(z) \Rightarrow A(z))) $

    L'union de A, c'est l'ensemble u(x) : $ \exists y $ $ (y(x) \wedge A(y)) $

    Etc.


    Ce n'est bien sûr qu'une idée, une suggestion, et je ne sais pas si elle viable et si elle a un rapport avec ce que tu as en tête.
  • @GG, certes, on peut algébriser ZF aussi comme tu commences à le faire, mais c'est tout autant usine à gaz.

    Le malentendu avec Foys vient de son titre, qui annonce une introduction au langage. Et non un débat sur la consistance.

    Ce que je lui ai dit est que les deux ne provoquent pas de mélange puisque ZF n'est qu'un cas particulier de la TDE contradictoire, ie axiomes

    $$ << \forall R>> \exists a\forall x: ([x\in a]\iff [R(a)]) $$

    que je vais abréger pour la suite en TDENB pour "TDE non bridée", qui elle-même n'exprime QUE des axiomes implicitement induit par le langage et que tout ça, c'est totalement formel.

    Il a posté un truc un peu "en colère", mais je ne me suis toujours pas relu pour voir si j'avais été maladroit éventuellement, dans lequel la consistance a l'air importante pour lui.

    Or je le répète, il n'y a pas de "solubilité" : les preuves de $0=1$ ou de n'importe quoi d'autres EXPLICITENT TOUJOURS les instances de

    $$ \{x\mid R(x)\} $$

    qui sont utilisées.

    A un moment il écrit
    Foys a écrit:
    de plus si j'avais voulu parler de lambda calcul j'aurais intitulé le post "lambda calcul" ou quelque chose comme ça.

    qui résume le mieux notre désaccord. On peut toujours dire que "c'est du lambda calcul" si on veut, juste parce que ce mot a été réimporté dans une spécialité qui a d'autres objectifs que ZFéfiriser, MAIS, non je persiste et signe à dire que C' EST LA MEME CHOSE et bien plus fluide.

    Même si ce n'est pas l'usage, ça s'apprendrait très vite et ça présente l'avantage qu'il n'y ni variables, ni parenthèses, ni quantificateurs au sens propre, puisqu'il s'intègrent tous naturellement au process.

    On n'est ps sur "de la recherche de pointe", mais sur "ds choix de posts et de fils pour donner au grand public, c'était comme ça que j'avais compris son intention. On n'atteindra de "grand public" avec la complexité et la patience qu'il faut pour ingérer du Bourbaki, alors que sur le principe, ce que je signale relève d'un simple jeu de calcul "presque" accessible en sixième

    J'ajoute pour finir, que le jour à où un gamin vient te voir en te prouvant $0=1$ à coup d'exploitations diagonales, c'est un bon (ce n'est pas un échec enseignemental invitant à remettre en cause le langage). Bien avant "cette utilisation du chèque repas pour acheter un Paquebot", crois-moi, il y a des fautes autrement plus grave à corriger chez les débutants.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • OK, CC, mais tu n'as pas véritablement répondu à mon interrogation : est-ce que la démarche que j'ai esquissée est viable (i.e. est-ce qu'elle ne conduit pas rapidement à des contradictions rédhibitoires ?) et est-ce qu'elle permet de se dispenser des axiomes de ZF, ce qui serait en soi très intéressant, non ?
  • christophe c a écrit:
    MAIS, non je persiste et signe à dire que C' EST LA MEME CHOSE et bien plus fluide.
    Cette affirmation n'est pas prouvée.
    De toute façon rien n'est jamais égal à rien, il y a des traductions entre systèmes à fournir.
  • Je vais être en transit quelques temps. Mais je pensais que tu sais de quoi je parle. Je te trouve de mauvaise humeur dans ton style. Y a-t-il un truc technique auquel tu penses qu'on pense tacitementqui expliquerait ça ou c'est juste comme ça?

    De mon téléphone
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c a écrit:
    Je vais être en transit quelques temps.
    Pareil pour moi, je risque de n'être pas trop disponible les prochains jours.
  • Bonjour.

    Moi je trouve que c'est une bonne chose car je vais aussi être en transit quelques temps, je ne raterais donc rien.

    À bientôt.

    Cherche livres et objets du domaine mathématique :

    Intégraphes, règles log et calculateurs électromécaniques.

  • christophe c a écrit:
    Je vais être en transit quelques temps. Mais je pensais que tu sais de quoi je parle. Je te trouve de mauvaise humeur dans ton style.
    Je ne suis pas sûr de ce dont tu parles, ce n'est pas clair.
    christophe c a écrit:
    Y a-t-il un truc technique auquel tu penses qu'on pense tacitement qui expliquerait ça ou c'est juste comme ça?
    Tout se passe comme si tu essayais d'inciter à utiliser des fondements alternatifs pour bousculer les gens dans leur apprentissage de base et les amener à penser que 0=1. Ca a été un de tes projets sauf erreur (prouver la non consistance de ZF). Il n'y a rien de mal à ça (les garanties du contraire de pouvant exister) mais j'ai dit que je présentais le langage mathématique usuel dans lequel il n'y a pas ça (la logique du premier ordre sans axiomes supplémentaires est consistante) et il est hors de question pour moi d'embrigader, peut-être à leur insu, des lecteurs potentiels dans un projet spéculatif quelconque.

    D'autre part le système que tu esquisses est contradictoire au niveau du langage (puisqu'il permet d'écrire des combinateurs de point fixe) alors qu'à nouveau la logique du premier ordre ne l'est pas (modèles à un élément; modèles à deux éléments + extensionnalité pour mettons une signature avec $(\in, =)$: $\{0,1\}$ muni de son ordre habituel: dans la théorie des ensembles usuelle, les problèmes de consistance éventuels sont provoqués par les axiomes, une fois les règles de démonstrations introduites). Dans mes réponses plus haut, quand j'insiste sur la consistance c'est avant tout pour pointer cette différence.
  • Je comprends mieux ton approche morale. Mais je pense que tu te trompes sur l'aspect trompeur. Qu'on le veuille ou non la notation

    {x / blabla}

    continue de parler au delà de la consistance sans que je trouve légitime de parler d'arnaque. Je préfère dire que les gros objets provoquent l'égalité entre 0 et 1 sans qu'il n'y ait lieu de s'en étonner outre mesure.

    Rien à voir, je n'aurai pas internet avant longtemps ds ma cambrousse paradisiaque donc peu de possibilités d'intervenir (téléphone bof bof pour taper des maths). Si un modérateur voyait ce présent msg accepterait-il de cacher mon fil "viré" pour évite risque de desanonymisation de "m'y New life"? Merci par avance et à bientôt..

    [C'est fait. Poirot]
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • La bonne nouvelle du jour c'est que christophe c is still alive. Salut Christophe ! Bonne rentrée et bonne installation dans ta cambrousse paradisiaque.
  • Bonjour Christophe! Je suis heureux de de te revoir (t'as déménagé dans le sud? Les profs demandent tous leur mutation là-bas).
  • Grand merci à Poirot!!

    Oui, je suis pile poil au carrefour des plus beaux paysages du pays. C'est assez incroyable, je ne réalise pas encore. Seul prix à payer: la technologie internet y parvient assez difficilement :-D Mais la 3D mode réel c'est inestimable.

    Bonne rentrée à tous.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Bonjour CC

    J'espère que tu vas bien. Serais-tu proche du 04 ? ;-)

    Amitiés

    Titi
Connectez-vous ou Inscrivez-vous pour répondre.
Success message!