Ensembles finis collaboratifs

Je démarre un fil "simple", dont j'espère qu'on aura une construction collégiale. Il n'y a rien de bien inventif, il s'agit à plusieurs de faire avancer un peu le succès de la traduction de l'arithmétique dans les ensembles finis (qui sont gérés par ZFC non(infini) et n'ont pas besoin de récurrence, puisque l'a compréhension l'y met.

Je ne sais pas encore, mais il peut y avoir des avantages:

1/ La plupart des vérités des formules s'y calcule facilement, et c'est plus rapide qu'avec les entiers.

2/ On n'a que 2 opérations (singleton: unaire, union:binaire) et une constante $0$ qui est l'ensemble vide

3/ Les quantifications bornées passent toutes seules

4/ La programmation des maths aussi (qui sur le forum, sait "facilement" représenter les suites finies ou l'opération puissance avec les entiers? 3% des gens? Alors que là sait passer à l'ensemble des parties)

5/ Certains objets y ont définitions qualitatives: les puissances des premiers sont les cardinaux munissables d'une structure de corps par exemple

6/ Les opérations $+$ et $\times$ sont naturelles là où elles sont complètement artificielles dans Peano (même si amusantes)

7/ Leurs propriétés y sont naturelles et s'obtiennent sans effort

8/ Etc... Bref, il y a des avantages assez multiples. Sans compter qu'on retrouve les entiers et l'arithmétique sans fatigue et les coefficients binomiaux y sont définis naturellement et non pas des espèces de formules bizarres.


1/ Je propos de fixer une bonne fois pour toute $S(x):=\{x\}$ et $U(x,y):=x\cup y$. Ce seront les seules notations primitives (avec les quantificateurs non bornés non bornés évidemment).

2/ Définition (enfin axiomatisation) de $\in, \subset, =$:

$(x\in 0) := false$

$(0\subset x):=true$

$[x\in U(a,b)]:= [(x\in a)$ ou $(x\in b) ]$

$[S(x)\subset a] := [x\in a]$

$(U(x,y)\subset a) := ((x\subset a)$ et $(y\subset a))$

$[x=y]: = [(x\subset y)$ et $(y\subset x)]$

$(x\in P(y)):= x\subset y$

$Choix(0):=0$

$Choix(S(x)) = x$

$Choix(U(a,b)) : = [let$ $c:=Choix(a)$ in if $(c\in a)$ then $x$ else $Choix(b)]$

3/ Quelques remarques: j'ai ajouté du confort avec l'ensemble des parties et l'axiome du choix NON EXTENSIONNEL (ie on n'a pas de garantie que $a=b\to Choix(a)=Choix(b)$, cet axiome du choix est inoffensif, mais de toute façon, dans le cas fini, même l'axiome cu oihx extensionnel est un théorème).

4/ Le schéma de récurrence est que si une collection définissable contient $0$ et est stable par $S,U$ alors elle contient tout le monde.

5/ Les théorèmes de Ramsey permettent de tout ramener à de la quantification bornée sous l'oracle qui donne les parties infinies homogènes. De sorte que cette dernière disparaissant avec la fonction $Choix$ (qui n'est rien d'autres qu'une procédure de parcours de liste banale), Les oracles Ramseyiens renvoient à de simples formules écrites avec les fonctions précédentes (sans utiliser $P$).

Je rappelle ce qu'est un entier (ici):

6/ [$x$ est transitif] veut dire [$\forall y\in X: y\subset x$]

7/ [$x$ est un entier] veut dire [$x$ est l'ensemble de ses parties transitives à l'exception de lui-même]

8/ $(x,y)$ est une abréviation de $U(S(S(x)), S(P(P(y))) )$ (j'évite ainsi que $(x,x)$ ne contiennent qu'un seul élément).

9/ Je laisse les gens à qui ça peut plaire définir les bijections.

10/ Je rappelle qu'il n'y a absolument pas besoin de définir la notion de fonction de façon usine à gaz comme ça a été fait dans l'académisme. Les ensembles sont DEJA des fonctions à travers l'opération:

$$ a(b) := \{x\mid (b,x) \in a\} $$

11/ Après quoi, on pourra s'amuser à éliminer les quantifications bornées pour voir ce que ça donne pour les énoncés les plus célèbres.