Arithmétique de Peano du premier ordre

[Médiat]

Une partie finie de l'ensemble des formules est vérifié par tout entier plus grand que ceux qui interviennent dans la partie en question
-----

[Merlin95]

Ha ok encore merci.

[Médiat]

Salut

Voilà une proposition de 1-types qui devrait permettre de trouver un minorant intéressant

On définit un nouveau symbole de prédicat lu ( divise ) (pas besoin d'axiome, puisqu'il est défini à l'aide d'élément du langage, et donc cela ne change pas la théorie)

Par la suite représentera les nombres premiers de , ce qui n'est pas un problème puisqu'on ne l'utilisera pas dans les formules mais pour construire les formules (définissable de toute façon, mais ce n'est pas le problème)


Soit , et soit l'ensemble de formules pour :





Soit le 1_type , par compacité ce 1-type est satisfiable dans AP et donc possède au moins un modèle.

Il faut

1) montrer que chaque partie finie de est satisfiable, par exemple en montrant qu'il y a un élément de IN qui vérifie cette partie finie
2) compter les 1_types
3) minorer le nombre de modèles

Bon courage (ce n'est pas très compliqué)