Remplacement
Axiome de remplacement:
$\forall f \forall a\exists b\forall z(z\in b\leftrightarrow \exists c(c\in a\wedge z=fc))$
Ici, $f$ est une variable fonctionnelle d'arité 1, les autres variables étant des variables fonctionnelles d'arité 0.
Le schéma d'axiomes de remplacement est une théorie du premier ordre qui est équivalente à la formule du second ordre que j'ai écrite plus haut. Pourquoi ça a l'air beaucoup plus naturel le second ordre ?
$\forall f \forall a\exists b\forall z(z\in b\leftrightarrow \exists c(c\in a\wedge z=fc))$
Ici, $f$ est une variable fonctionnelle d'arité 1, les autres variables étant des variables fonctionnelles d'arité 0.
Le schéma d'axiomes de remplacement est une théorie du premier ordre qui est équivalente à la formule du second ordre que j'ai écrite plus haut. Pourquoi ça a l'air beaucoup plus naturel le second ordre ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Votre question n'est pas mathématique et concerne votre ressenti, comment pourrions-nous répondre ?
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Ah bon ? C'est passer un peu vite sur les travaux de J-Y. Girard, par exemple : https://fr.wikipedia.org/wiki/Syst%C3%A8me_F
Alors 1) cette théorie n'a pas de modèle plein (évident, $\{c_n, n\in\mathbb N\}$ n'a pas de minimum); 2) il n'y a pas de contradiction qui puisse s'obtenir en un nombre fini d'étapes (preuve : une telle contradiction n'utilise qu'un nombre fini de constantes $c_n$, mais alors la théorie a plein de modèles si on se restreint à ces constantes).
Un élément essentiel de ce contre-exemple est la finitude des preuves, mais aussi du nombre d'axiomes utilisé par étape de la preuve. Le premier me semble essentiel à la notion de preuve (quoique ça a certainement été étudié), mais dans des logiques plus bizarres on peut imaginer des preuves où une étape est $\bigvee_{i\in I}\varphi_i$, $\varphi_i$ des axiomes ou théorèmes, $I$ non nécessairement fini (je ne sais pas comment faire un gros $\land$ donc je m'en tiens à $\vee$ mais vous voyez ce que je veux dire) - typiquement en $L_{\kappa,\lambda}$, même si ça je n'y connais rien.