47 lines
		
	
	
		
			1.8 KiB
		
	
	
	
		
			Markdown
		
	
	
	
	
	
			
		
		
	
	
			47 lines
		
	
	
		
			1.8 KiB
		
	
	
	
		
			Markdown
		
	
	
	
	
	
| up::[[axiomatique]]
 | |
| #s/maths
 | |
| 
 | |
| ---
 | |
| 
 | |
| # Axiomes de Peano
 | |
|  - $0 \in \mathbb{N}$
 | |
|  - si $x \in \mathbb{N}$ alors le successeur de $x$, noté $s(x)$ est dans $\mathbb{N}$ ($\forall x \in \mathbb{N}, s(x) \in \mathbb{N}$)
 | |
|  - $\forall (x, y) \in \mathbb{N}^{2}, \quad s(x) = s(y) \iff x = y$
 | |
|  - $\nexists x \in \mathbb{N}, \quad s(x) = 0$
 | |
|  - $P(0) \wedge \forall n \in \mathbb{N}, (P(n) \implies P(n+1)) \quad \implies \quad \forall n \in \mathbb{N}, P(n)$
 | |
|      - proposition de récurrence
 | |
|      - équivalent à dire que _tout sous-ensemble de $\mathbb{N}$ a un plus petit élément ($\mathbb{N}$ est bien ordonné)_
 | |
| 
 | |
| # Théorie des ensembles
 | |
| [[axiomes Zemerlo Frankel]]
 | |
| 
 | |
|  - $0 := \emptyset$
 | |
|  - $1 := 0 \cup \{ 0 \} = \{ 0 \}$
 | |
|  - $2 := 1 \cup \{ 1 \} = \{ 0 \} \cup \{ 1 \} = \{ 0,1 \}$
 | |
|  - $3 := 2 \cup \{ 2 \} = \{ 0, 1, 2 \}$
 | |
|  
 | |
| Le _sucesseur_ est défini comme $s(x) = x \cup \{ x \}$
 | |
| 
 | |
| On utilise l'[[axiome de l'infini]] pour définir $\mathbb{N}$ :
 | |
| 
 | |
| ![[axiome de l'infini#^definition]]
 | |
| 
 | |
| ![[classe héréditaire#^definition|ensemble héréditaire]]
 | |
| 
 | |
| De plus, on a une relation d'ordre totale et d'ordre strict totale : $x \geq y \iff x \subset y$ et $x < y \iff x \in y$
 | |
| 
 | |
| Avec cette définition, le [[principe de récurrence]] n'est plus un axiome, mais on le démontre : [[ZF démonstration du principe de récurrence]]
 | |
| 
 | |
| # Propriétés
 | |
| 
 | |
| > [!query] Sous-notes de `=this.file.link`
 | |
| > ```dataview
 | |
| > TABLE title, up as "Up", up.up as "2-Up", up.up.up as "3-Up", up.up.up.up as "4-Up"
 | |
| > FROM -#cours AND -#exercice AND -"daily" AND -#excalidraw AND -#MOC
 | |
| > WHERE econtains(list(up, up.up, up.up.up, up.up.up.up), this.file.link)
 | |
| > WHERE any(map([up, up.up, up.up.up, up.up.up.up], (x) => econtains(x, this.file.link)))
 | |
| > WHERE file.link != this.file.link
 | |
| > SORT up.up.up.up, up.up.up, up.up, up
 | |
| > ```
 | |
| 
 |