[Logique] pensée random

Supposons qu'on regarde le processus d'avoir de témoins de Henkin, càd que pour toute formule à une variable libre F on ajoute une constante c_F et l'axiome "(exists x, F(x)) -> F(c_F)". Maintenant au lieu de dire "exists x", on dit "il existe un unique x". Est-ce que notre nouvelle théorie avec témoins est une extension conservative ?

Wallah jai rien confruit igo

Parce que si c'est le cas, ça permet d'avoir un système de nommage "safe" : ajouter des noms à des objets définis de manière unique ne change aucun résultat prouvé.
Sans l'unicité j'ai peur qu'on puisse ajouter une sorte d'axiome du choix global, mais avec je dirais qu'on choisit juste de donner un nom à quelque chose de déjà défini correctement.

(Je sais pas si ça correspond à de l''extension par définition, dans mes souvenirs une telle extension associe une nouvelle définition à un terme, ce qui fait que typiquement pour ZFC on peut pas faire de def vu qu'il nous manque le moindre symbole de constante.)

Même question si on ajoute "pour tous x1,...,xn, il existe un unique blabla".
Typiquement pour pouvoir définir l'union de deux ensembles.

Non, la nouvelle théorie avec témoins ne sera pas nécessairement une extension conservative de la théorie initiale. Une extension est dite conservative si toute formule de la langue initiale qui est prouvable dans l'extension est déjà prouvable dans la théorie de départ.

Voici pourquoi le passage à des témoins pour des formules avec quantification existentielle unique pourrait ne pas être conservatif :

1. Ajout de nouveaux axiomes : Lorsque vous introduisez des témoins pour des formules de la forme "il existe un unique tel que ", vous ajoutez de nouvelles constantes ainsi que des axiomes du type :



(\exists! x \, F(x)) \to F(c_F),

(\exists x \, F(x)) \land (\forall y \, \forall z \, (F(y) \land F(z) \to y = z)).

2. Unicité et contradictions potentielles : En ajoutant des témoins pour des formules avec unicité, vous imposez implicitement une contrainte forte sur les modèles de votre théorie : si est vrai dans un modèle, alors il doit y avoir exactement un élément satisfaisant . Cela peut exclure certains modèles de la théorie initiale, rendant l'extension non conservative.


3. Conservativité : Pour que l'extension soit conservative, tout théorème de la langue initiale prouvable dans la théorie enrichie (avec témoins pour ) doit être prouvable dans la théorie originale. Cependant, les axiomes liés aux témoins d'unicité pourraient permettre de prouver des résultats supplémentaires qui ne sont pas prouvables dans la théorie initiale. Par exemple, si l'unicité implique une propriété structurelle forte qui n'était pas garantie dans la théorie de base, cela pourrait entraîner des divergences.



En résumé, l'ajout de témoins pour des formules avec unicité () impose des contraintes supplémentaires sur les modèles de la théorie, ce qui peut conduire à des résultats prouvables dans l'extension mais pas dans la théorie de départ. Par conséquent, la nouvelle théorie n'est pas nécessairement une extension conservative.

@Physics4fun qu'est-ce que tu en penses ?

J'ai C/c mais les symboles ne figurent pas tous.

C'est nul.

Truc intéressant : si on prouve que l'extension est conservative pour une seule couche d'ajouts de symboles, on en déduit que l'ajout d'une tour indicée sur N de couches de symboles sera aussi conservative, de la même manière que ça marche pour la préservation de cohérence dans le cas des témoins de Henkin.

Bonne digestion

Mais oui c'est clair

C'était quel piment au fait ?

Une personne de confiance sans aucun doute

Ok je viens de trouver une idée pour les constantes.

Si on a une formule G(cF) avec cF une constante introduite tq e | T |- G(cF), alors on prouve par induction sur les preuves que e, x | T, F(x) |- G(x). En particulier si G ne fait pas apparaître cF, on a e, x | T, F(x) |- G, d'où ensuite

e | T |- il existe x, F(x)
e, x | T, F(x) |- G
==================
e | T |- G