Lors d'une conférence, Hintikka affirmait qu'on pouvait tenir les quantificateurs pour de simples abréviations des fonctions de Skolem...
Je conçois sans difficulté comment on peut supprimer soit les quantificateurs existentiels, soit les quantificateurs... mais je ne trouve aucun document expliquant comment remplacer TOUS les quntificateurs par des fonctions...
Quelqu'un peut m'aider ?
Salut,Envoyé par quantat
tu dis "soit les quantificateurs existentiels, soit les quantificateurs...", il faut lire "soit les quantificateurs existentiels, soit les quantificateurs universels" ?
A quel autre type de quantificateurs penses-tu en dehors de ceux-ci ?
Sinon, des explications de "skolemisation" pour divers cas (tous les cas ?), à partir de la fin de la page 16 de ce doc : http://ocw.mit.edu/NR/rdonlyres/Heal...10_logic2a.pdf
Bonjour ,
En langage de tous les jours ( et dans la logique d'aristote par ex. ) il y a d'autres quantificateurs , par exemple le quantificateur "quelques" ...
mais dés qu'il y a eu la théorie des ensembles seuls "il existe" et "tout" sont restés parce qu'ils sont devenus suffisants , par exemple :
"quelques X de l'ensemble E" voulant dire la meme chose que "tout X de l'ensemble P(E)" ( avec P(E) inclu dans E ) le quantificateurs quelques a par conséquent disparu ...
L'affirmation d' Hintikka est elle valable aussi pour "quelques" ?
Bonjour bardamu,
oui il s'agissait bien des quantificateurs universels (j'avais rédigé trop rapidement)...
Je vais consulter le texte que tu as eu l'amabilité de me communiquer. Merci.
Bonjour Matmat,
ta remarque me surprend un peu: j'avais toujours tenu "il existe" et "quelques" pour équivalents: as tu un exemple qui illustre la différence ?
bardamu, je pense avoir compris le procédé...
On élimine facilement les quantificateurs existentiels et, après avoir transformé la proposition en forme normale conjonctive ou disjonctive, on élimine les quantificateurs universels (qui restent tout de même implicites me semble t'il) en exprimant la liste des clauses, puis on "instancie" les variables... si la liste des clauses instanciées a un modèle, la formule initiale aussi...
Il s'agit donc bien d'une méthode de calcul sémantique.
J'avais cru, au départ, qu'il était possible d'exprimer exactement la même chose, qu'on pouvait donner une formule strictement équivalente à la formule initiale en remplaçant tous les quantificateurs par des fonctions...
Or, sauf erreur de ma part, la formule quantifiée initiale a un modèle si la formule skolémisée et "clausifiée" a un modèle, l'inverse n'etant pas forcément vrai...
Je ne suis pas sûr que l'inverse n'est pas forcément vrai.
Un cours qui me semble plus clair que le doc donné plus haut : http://www-lsr.imag.fr/Les.Personnes...05/sSkolem.pdf
Extrait p. 14 :
La transformation décrite est appelée la skolémisation. Elle vérifie :
1. Si G a un modèle alors G' en a un
2. Toute formule de G est conséquence de sa transformée dans G' et par suite tout modèle de G' est modèle de G.
Tu as raison ,
en fait je pensais que dans le langage courant "quelques" signifiait plusieurs ( au moins deux ) et que par conséquent cela le rendait donc différent du "il existe" qui signifie "au moins un" .
bonjour Bardamu,
j'été déjà tombé sur le document que tu as l'amabilité de me proposer.
La page 2 sur la skolémisation d'une formule existentielle précise que la forule skolémisée n'est pas équivalente à la formule initiale: si la transformée a un modèle, la formule initiale aussi, la réciproque n'étant pas nécessairement vraie.
Bonjour Matmat,
c'est là un des "pièges" dans lesquels on tombe souvent lors du passage du langage courant au langage formel
