Discussion:Théorie des modèles

Définition élémentaire

C'est dommage qu'il n'y ait pas, au début de l'article, une définition de ce qu'est un modèle pour un ensemble d'axiomes (un ensemble muni d'une relation binaire qu'on interprète comme l'appartenance), assortie d'exemple (au moins le modèle d'Ackermann). Quelqu'un qui ne connait rien à la logique ne peut pas lire cet article...

Bonjour... en effet je suis curieux par rapport aux mathématiques et m'intéressant à la logique mathématique en tant que novice, j'ai commencé à lire cet article, et j'ai eu beaucoup de mal à le comprendre jusqu'à l'exemple sur la loi de Pierce qui m'a enfin permis de comprendre ce qu’était un modèle: si j'ai bien compris c'est d'une part l'ensemble des variables propositionnelles atomiques à qui on associe à chacune soit la valeur vrai, soit la valeur fausse, et d'autre part l'association à cet ensemble de variables d'une formule qui est elle aussi vrai ou fausse. Ne maîtrisant pas la définition de modèle mathématique je ne me risquerai pas à le rédiger, mais je trouverai interessant qu'elle soit rajouter dès le début... Cependant si quelqu'un me donne une définition précise dans cette discussion je pourrai l'aider à la rajouter sur l'article.--Nicobzz (d) 2 novembre 2010 à 13:39 (CET)

Je trouve qu'il faudrait revoir la rédaction du paragraphe présentation de la théorie des modèles car il me paraît un peu verbeux et limité. Il n'envisage que le calcul des prédicats du premier ordre en logique classique, alors qu'il serait souhaitable d'introduire en préambule une théorie des modèles plus générale (calcul propositionnel, calcul des prédicats, logique intuitionniste) quitte à renvoyer vers d'autres articles (en particulier pour les modèles en logique intuitionniste qui devraient avoir un article à eux tous seuls). Il faudrait aussi un paragraphe sur le fait qu'un modèle d'une théorie peut, sous une autre interprétation, servir de modèle à une autre théorie (je pense au modèle de la géométrie non euclidienne en réinterprétant des objets de la géométrie euclidienne). Enfin une phrase telle que Tout être rationnel dispose d’un tel pouvoir divin me paraît totalement déplacée dans un article scientifique. Theon 22 février 2006 à 18:40 (CET)

Nom de l'article

Il est malheureux que cet article s'appelle théorie des modèles, et pas "sémantique de ...", cet article ne parle pas de la théorie des modèles, qui est un domaine de la logique mathématique, dont on n'a aucune idée en lisant cet article. Il faut séparer logique classique et intuitionniste, probablement calcul propositionnel classique, et calcul des prédicats classique. Le problème c'est que comme la définition de la sémantique de la logique classique est basique, il y a déjà beaucoup d'articles qui pointent sur celui-ci, et ça ne peut que croître ... Peut-on encore modifier ? Proz 12 mai 2006 à 02:41 (CEST)

Prouvabilité

Peut-être faudrait-il dire « démontrabilité »? Mais que ce soit « prouvabilité  » ou « démontrabilité » cela a un sens précis. Une proposition est « démontrable » ou « prouvable » si elle peut être « démontrée » ou « prouvée » dans le système logique considéré. Je pense que syntaxique ne veut rien dire, car la syntaxe d'un système logique ça n'est pas la partie démonstration et nous avons le devoir d'être à la fois précis et didactique. Pierre de Lyon 5 mai 2007 à 20:20 (CEST)

Oui tu a raison, c'est la phrase qui m'avait choqué. Par contre j'ai un doute est-ce le même concept que «Décidabilité» ou il y a une nuance ? Outs 6 mai 2007 à 11:00 (CEST)

Le problème est que « décidable » et surtout sa négation « indécidable »est polysémique en logique. On emploie souvent « indécidable » pour dire « indémontrable », tandis qu'« indécidable » signifie aussi qui ne peut pas être « tranché » par algorithme. Quant à « décidable », il signifie presque toujours qui peut être accepté ou refuté par algorithme. J'affirmerais donc que le concept de « décidabilité » est différent de celui de « démontrabilité ».

Évidement ça ne pouvait pas être simple ... :-)

Est-ce que la nouvelle formulation te va? Pierre de Lyon 7 mai 2007 à 14:52 (CEST)

Oui cela me parait beaucoup plus clair.

En passant, puisque tu a l'air de t'y connaitre, aurait-tu quelque part dans tes cartons quelques textes ou article que l'on pourrait rajouter en source. Cela me parais indispensable pour un article de ce genre. Mais je sais aussi que ce n'est pas facile de trouver des bonnes sources. (Si tout les articles étaient sourcés cela permettrait à des rédacteurs d'un niveau intermédiaire, genre moi, de corriger ou d'améliorer) Outs 8 mai 2007 à 09:48 (CEST)

Mon domaine étant plutôt la théorie de la démonstration, je ne sais pas quel est le meilleur livre à recommander en théorie des modèles. Je constate que l'article en anglais donne des références récentes, (:-) en anglais hélas ou bien sûr! Pierre de Lyon 8 mai 2007 à 17:37 (CEST)

Je ne suis pas non plus théoricien des modèles, mais vu le contenu actuel de l'article, le Cori-Lascar Tome I suffit. Il y a un chapitre introductif à la théorie des modèles proprement dite ch 8 du Tome II. L'article anglais parle (ou souhaiterait parler, puisqu'il est en construction) "vraiment" de théorie des modèles compte aller plus loin. Il me semble toujours qu'il faudrait réorganiser. En attendant la section reprise par Pierre pourrait s'appeler "Notion de modèle" plutôt que "Présentation de la théorie des modèles". Proz 8 mai 2007 à 19:08 (CEST)

Je pense qu'en fait il y a trois parties dans cette section:

1. une définition succincte,
2. un survol historique,
3. une description (succincte elle aussi) des objectifs.

Faut-il créer des sous-sections? Pierre de Lyon 8 mai 2007 à 19:52 (CEST)

La section est une introduction à la notion de modèle, qui est déjà satisfaisante (on pourrait peut-être préciser que les preuves de cohérence sont relatives), mais la théorie des modèles c'est autre chose, à la frontière entre algèbre et logique, avec des méthodes spécifiques (voir le plan, ambitieux, de la version anglaise). La réorganisation, désolé de ne pas avoir été précis, c'est une référence à mon message de 2006 au dessus. Je pensais : faire un article à part pour la logique intuitionniste modèle de Kripke (mais il y a la logique modale), ou plutôt modèle de la logique intutionniste (on peut mettre deux mots sur les modèles de Beth), renommer celui-ci par exemple modèle de la logique classique, ou "sémantique de la logique classique", et espérer quelqu'un de compétent pour théorie des modèles (je peux quand même faire une ébauche, l'article anglais est pris en main par une spécialiste apparemment mais qui a l'air très occupée, c'est prématuré de le traduire). Proz 8 mai 2007 à 22:32 (CEST)

différence entre une théorie consistante (cohérente) et non-contradictoire ?

L'article dit: Il n'est pas toujours facile ou possible de montrer qu'une théorie est consistante. Il est parfois plus facile de montrer qu'elle est non contradictoire. Quelle est la différence entre une théorie consistante (cohérente) et une théorie non-contradictoire ? Ce n'est pas très clair, puisque je lis ailleurs:

• cohérence : (non contradiction), en mathématique, la cohérence est la propriété logique d'une théorie absente de contradiction ; http://fr.wikipedia.org/wiki/Coh%C3%A9rence
• consistance: On dira qu'une théorie est consistante (ou cohérente) si elle ne permet pas de prouver à la fois une formule et sa négation. http://fr.wikipedia.org/wiki/Th%C3%A9orie_des_mod%C3%A8les
• consistency: In mathematical logic, a formal system is consistent if it does not contain a contradiction, or, more precisely, for no proposition φ are both φ and ¬φ provable. http://en.wikipedia.org/wiki/Consistency_proof

Merci de vos éclaircissements. Eric 29 novembre 2007 à 16:18 (CET)

Les définitions précises sont dans l'article, qui a tort çà mon avis de présenter celles-ci comme si elles étaient universelles (on peut tout aussi bien inverser). Il y a deux définitions équivalente de la cohérence ou consistance, l'une sémantique -- il existe un modèle, l'autre syntaxique -- il existe une formule qui n'est pas démontrable (d'où incohérence : pas de modèle, toutes les formules sont démontrables). Je précise que démontrer une contradiction ça a pour conséquence de démontrer toutes les formules. L'équivalence de ces deux définitions (en logique classique) c'est le théorème de complétude de Gödel. Pour des raisons pédagogiques, on donne souvent des noms différents à chacun des énoncés avant de montrer ce théorème. Il est normal de trouver des variations dans la littérature, à la fin ce sera la même chose. Il vaudrait mieux que l'article dise : pour montrer la cohérence ou consistance d'une théorie il est souvent plus facile d'en déterminer un modèle que de montrer qu'on ne peut dériver de contradiction. Mais les preuves de cohérences sont forcément relatives, à la cohérence d'une autre théorie. Les preuves de cohérence syntaxiques peuvent donner des résultats plus fins. Proz (d) 30 novembre 2007 à 00:01 (CET)

On impose U non vide, vraiment ?

Il est vrai que si on autorise U vide (ce qui bien sûr n'est possible que pour les langages sans constantes), l'exemple 1 ne marche que pour les langages avec constantes. Mais justement, je demande à voir comment la formule

$\exists x\;\forall y\;(R(x)\to R(y))$

pourrait "également être prouvée au moyen d'un système de déduction" dans un langage sans constantes.Anne Bauval (d) 20 juillet 2010 à 23:37 (CEST)

1/ Ta formule ci-dessus est équivalente à : all x R(x) --> all y R(y) ; moyen mnémotechnique pour se rappeler comment déplacer les quantificateurs lorsqu'il y a une implication : le quantificateur se conserve sur le conséquent et s'inverse sur l'antécédent de l'implication (il faut bien sûr faire attention à ne pas capter une variable libre quant on fait le déplacement).

2/ Sinon une structure d'interprétation est tjs définie en effet sur un ensemble non vide et on a donc comme formule valide du calcul des prédicats : all x Px --> exists x Px. Pour le démontrer il faut partir des règles d'inférence qui peuvent varier selon les présentations.

A ma connaissance, cette restriction de la logique à un domaine non vide d'objet n'est pas nécessaire (on peut l'étendre, mais bon si c'est pour parler de rien ;-) ) mais facilite la présentation. Cette règle à mon souvenir (pas biographique, mais de lectures anciennes, hein :-) ) n'existait pas avant Frege et il me semble que la logique de Port Royal du 17è (qui est restée à un catalogue de "syllogismes" très simple) ne l'avait pas pour exemple.

--Epsilon0 ε₀ 21 juillet 2010 à 12:05 (CEST)

Je n'avais aucun scrupule à remplacer de mon propre chef (de proche en proche)

$\exists x~\forall y~(R(x)\to R(y))$

par

$[\forall x~R(x)]\to [\exists x~\forall y~R(y))]$

mais c'est ce $\exists x$ que je n'osais pas gommer, sans trouver quelque part une règle d'inférence qui m'y autoriserait (et de même, ta règle $\forall \to \exists$ me choque a priori). Mais bon ... Anne Bauval (d) 21 juillet 2010 à 15:51 (CEST)

On peut toujours supprimer (biffer tout simplement !) un quantificateur (parasite) qui ne lie aucune variable. Sinon les règles du jeu sont cachées ici. --Epsilon0 ε₀ 21 juillet 2010 à 17:52 (CEST)

Ah ! merci pour le lien. Eh bin justement, avec ces règles, on ne peut démontrer ton $\forall \to \exists$ que dans un langage avec constante, et on ne peut pas "biffer" le $\exists x$ qui me gênait. Anne Bauval (d) 21 juillet 2010 à 18:06 (CEST)

Ah ? Euh ... je sens que je vais être obligé de réfléchir (et consulter du plus formel : Cori et Lascar par exemple). En gros je pense que le "a" de P[a/x] n'est pas une vraie constante, même que ça pourrait bien être une constante (ou variable !) métalinguistique de constante. En tout cas si on peut faire P[x/x], le tour est joué pour ton $\forall \to \exists$. Aussi me demande bien si dans la règle d'élimination du quantif existentiel ... on ne pourrait pas remplacer le "q" par "P", ce qui règlerait la question du biffage de $\exists x$. Je sens qu'on va rentrer dans du subtil, quand j'ai qqch (+ sources) je reviens. Le langage de la logique est simple sauf quand on commence à se poser des (très bonnes) questions (par ailleurs il y a une forte littérature de philo de la logique justement en ce qui concerne sont langage, mais je vais essayer de rester dans des bouquins de maths). Sinon il y a aussi Forme prénexe, mais qui ne fait qu'affirmer sans remonter aux règles d'inférences. --Epsilon0 ε₀ 21 juillet 2010 à 19:57 (CEST)

Sinon ta formule initiale est ce que Jean-Louis Krivine appelle « le plus trivial des thms non triviaux », je ne sais plus dans quel texte mais j’en trouve trace ici page 13.

Il n'y a pas besoin de constante. En déduction naturelle la règle de "Il existe x P" on déduit P quand x n'apparaît pas dans P et une instance de la règle d'élimination du quantificateur existentiel (la preuve "auxiliaire" est réduite à P, c'est peut-être ça qui surprend). Les règles usuelles du calcul des prédicats (systèmes à la Hilbert, calcul des séquents également) supposent tous que les supports des modèles sont non vides (pour de "bonnes" raisons, c'est plus simple, il faudrait un prédicat d'existence, en tenir compte dans les règles ...). Proz (d) 19 mai 2011 à 09:57 (CEST)

Notre problème n'était pas d'éliminer $\exists$ mais de l'introduire (quand on disait "biffer", c'était dans une preuve "à reculons"). Or dans la règle d'introduction, on utilise un a qui nécessite au moins une constante. Anne Bauval (d) 19 mai 2011 à 10:22 (CEST)

Ok j'ai lu trop vite, et effectivement pas de rapport entre élimination de l'existentiel, et domaine non vide. Pour l'introduction dan votre cas c'est aussi une instance de la règle d'introduction, le cas où le terme qui intervient dans la règle n'intervient pas dans la formule de départ. Dans ce cas le terme (qui n'intervient pas et que l'on explicite pas usuellement) est une variable libre. Le fait que le domaine soit non vide est lié au fait que pour le règles d'introduction de l'existentiel et d'élimination de l'universel on ne demande rien au terme en jeu : il peut contenir des variable libres (donc en être une), qui jouent le rôle de ce que tu appelles constante. Proz (d) 19 mai 2011 à 11:07 (CEST)

Merci ! tout est clair pour moi maintenant. Anne Bauval (d) 19 mai 2011 à 13:37 (CEST)

Poizat, dans son cours de théorie des modèles p. 22-23 de l'édition en anglais Springer 2000 autorise le modèle vide, en reconnaissant qu'il va contre l'usage et se justifiant assez longuement (et en précisant ce qui doit être modifié par rapport aux usages, of course). Je maîtrise trop mal pour faire plus de commentaires que donner ce pointeur vers une source. Touriste (d) 19 mai 2011 à 23:53 (CEST)

Poizat fait de la pure théorie des modèles et le revendique. Il ne s'intéresse pas aux systèmes de démonstration (donc ne dit pas ce qu'il faudrait modifier à ce sujet), le théorème de complétude n'apparaît pas dans son bouquin. Quand il s'en approche (méthode de Henkin chapitre 4) il doit ajouter un élément "bidon" à ces modèles et modifier les formules en conséquence (en gros ça reviendrait à un prédicat d'existence) pour pouvoir se ramener à des modèles non vides. Ca pourrait être mentionné (pas forcément indispensable) dans un "vrai" article théorie des modèles, mais il faudrait dire que ça ne fonctionne pas bien avec les systèmes de preuve. Dans l'état de l'article ça ne peut qu'introduire de la confusion, ama.

(précision au cas où : il est indispensable en logique du 1er ordre d'avoir des variables libres dans les règles précitées ou leurs équivalentes, c'est-à-dire de pouvoir parler d'un élément quelconque du modèle, ceux-ci n'ayant pas forcément de "nom"). Proz (d) 20 mai 2011 à 19:33 (CEST)

Tautologie

Il y a une erreur sur la définition d'une tautologie; On appelle une formule vrai dans tout modèle une formule universellement valide et non une tautologie. Une tautologie se définie à partir de l'évaluation d'une formule logique. Il faut et il suffit que pour toute valeurs de vérité des variable propositionnelles, la proposition globale soit vrai par exemple, A ou (non A); (A => B) <=> (Non A => Non B)... Cependant on a trivialement le fait qu'une tautologie est universellement valide --Fougeroc (d) 8 novembre 2010 à 23:45 (CET)

Les 2 notions de tautologie et de validité (dans tout modèle) sont équivalentes. Sinon "tautologie" s'emploie peu pour le calcul des prédicats, on l'utilise surtout en calcul propositionnel.

Sinon, vérifiez que : (A => B) <=> (Non B => Non A) et non ce que vous avez écrit. --Epsilon0 ε₀ 9 novembre 2010 à 19:17 (CET)

Le modèle classique du calcul des propositions est le modèle {vrai,faux}, donc les concepts de formule valide et de tautologie coïncident. Et comme le dit Epsilon0 ε₀ le substantif tautologie est peu utilisé en calcul des prédicats, mais il l'est parfois comme synonyme de formule valide. Je crains que nous soyons en train de couper des cheveux en quatre. --Pierre de Lyon (d) 11 novembre 2010 à 15:24 (CET)

Je suppose que Fougeroc veut dire "en calcul des prédicats" auquel cas je connais la même définition que lui pour tautologie du calcul des prédicats (qui est aussi celle du Cori-Lascar et étymologiquement compréhensible). On ne parle pas trop de modèle d'habitude pour le calcul propositionnel (plutôt de valuation), donc je ne vois pas bien l'implication ici (j'ai mis quelque chose sur tautologie, mais l'article est assez hors sujet à mon avis, cf. version anglaise, le contenu correspondrait plutôt à Modèle (logique) (?), et plus renvoyer sur d'autres articles (calcul propositionnel). Proz (d) 19 mai 2011 à 10:15 (CEST)

Satisfiabilité (logique mathématique)

Bonjour, je viens de rédiger l'article Satisfiabilité (logique mathématique)... Je souhaitais invité l'un d'entre vous à la vérifier, j'ai fait une partie de la traduction de l'article anglais.

Merci. --Nicobzz (d) 10 juillet 2011 à 18:25 (CEST)

Théorie des modèles et écritures rigoureuses

Boujour, je me demandais quelque chose:

On peut par exemple prouver des théorèmes mathématiques par exemple en logique du premier ordre en utilisant par exemple la déduction naturelle et ses règles d'inférences, ainsi on crée un texte bien rigoureusement formaté pour prouver ce théorème.

En utilisant la théorie des modèles pour prouver un théorème, existe il aussi une manière bien rigoureuse de prouver ce théorème?

Merci. --Nicobzz (d) 1 septembre 2011 à 22:45 (CEST)

Ah! en relisant mieux l'article il me semble que c'est expliqué dedans, n'est ce pas?

--Nicobzz (d) 1 septembre 2011 à 22:47 (CEST)

La théorie des modèles n'est pas une syntaxe pour développer les preuves. On peut développer des preuves dans une théorie en justifiant les règles utilisées par la th. des modèles, mais les théorèmes de théorie des modèles sont plutôt des résultats "au niveau au dessus", par exemple qui permettent de fabriquer de nouveaux modèles ayant certaines propriétés (théorème de compacité, théorème de Löwenheim-Skolem ...). Lire plutôt la version en: pour savoir ce qu'est la théorie des modèles. Proz (d) 2 septembre 2011 à 08:16 (CEST)

Merci.--Nicobzz (d) 2 septembre 2011 à 13:45 (CEST)

Vérité mathématique

Je suis très gêné par la phrase de la section Présentation de la théorie des modèles : « Il [Tarski] a compris que cette vérité élémentaire pouvait le conduire à apporter une réponse générale, puissante et satisfaisante au problème plusieurs fois millénaire de la nature de la vérité mathématique ». Je ne sais pas si vraiment Tarski a compris cela, en tout cas je connais le théorème de Tarski qui dit grosso modo le contraire de ce que prétend cette phrase. C'est pourquoi je me propose de supprimer cette phrase et sa précédente (l'exemple de la neige pour expliquer la théorie des modèles a peut-être une valeur historique s'il fut donné par Tarski lui-même, mais pas très pédagogique). Alternativement, si vraiment il y a des signes que Tarski pensait cela mais alors il faut une référence, on peut glisser cette phrase dans une section historique, mais elle ne me semble pas à sa place là où elle est présentement.

Laurent de Marseille (discuter) 7 octobre 2016 à 13:37 (CEST)

bonsoir Laurent, je précise que la logique mathématique n'est pas mon domaine de base, mais que tout de même j'ai beaucoup lu dessus car je fais de la recherche dessus sur mon temps libre. Je ne pourrais pas confirmer que l'exemple de la neige a été cité par tarski ou non, mais il me parait être un bon exemple pour expliquer ce qu'est l'implication dans la théorie des modèles, et pour moi ça veut dire cela:

le théorème : "(il neige) => (il neige)" peut se vérifier dans la théorie des modèles car on peut voir que dans l'ensemble des modèles où il neige, il neige. Je vais détailler le principe: on considère deux types de modèles, ceux qui vérifient le fait qu'il neige, et ceux qui vérifient le fait qu'il ne neige pas.

On va d'abord prouver que tout les modèles satisfont l'énoncé "(il neige) => (il neige)" et à partir de cela on pourra prouver que le théorème est vrai car tout théorème est vrai si et seulement si il vérifie tout les modèles.

Allons y: pour les modèles où il neige, on a "(il neige) => (il neige)" égale à "Vrai => Vrai" car on remplace la valeur (il neige) par Vrai, hors si l'on regarde le tableau de vérité de l'implication "Vrai => Vrai" renvoie "Vrai", donc on vient de prouver que "(il neige) => (il neige)" satisfait les modèles où il neige est vrai, plus simplement on pourrait dire l'énoncé est vrai dans les modèles où il neige (bien qu'on préfère le terme satisfait les modèles où il neige)

pour les modèles où il ne neige pas, on a "(il neige) => (il neige)" égale à "Faux => Faux" car on remplace la valeur (il neige) par Faux (sa valeur dans le modèle étudié), hors si l'on regarde le tableau de vérité de l'implication "Faux => Faux" renvoie "Vrai", donc on vient de prouver que "(il neige) => (il neige)" satisfait les modèles où il ne neige pas, plus simplement on pourrait dire l'énoncé est vrai dans les modèles où il ne neige pas.

l'énoncé "(il neige) => (il neige)" satisfait tout les modèles (ceux où il neige et ceux où il ne neige pas), donc l'énoncé est un théorème (l'énoncé est dit je crois universellement valide, du moins en logique du premier ordre)

malheureusement cette explication n'a pas été donnée dans l'article alors qu'elle le méritrait je trouve, elle est longue et pas évidente à comprendre, il m'a fallu pas mal de temps pour comprendre pourquoi l'implication avait un tel tableau de vérité.

Voila pour le principe de la théorie des modèles, pour le détails il faut voir ce qu'est réellement un modèle pour la logique du premier ordre par exemple, car en fait les faits, vérités, sont contenues dans les modèles sous forme d'ensemble de prédicats et de fonctions qui s'appliquent à un ensemble nommé Domaine.

--Nicobzz (discuter) 9 octobre 2016 à 21:13 (CEST)

Excuses moi, je viens de lire ta page de discussion et me rend compte que tu es professeur en logique mathématique, donc surement je ne t'apprends pas grand chose, même si je pense que mon interprétation de la phrase de Tarski est bien la bonne, c'est juste que tu n'as pas du saisir son sens.--Nicobzz (discuter) 9 octobre 2016 à 21:26 (CEST)

En effet cela ne répond pas à mon objection qui est que je doute que Tarski ait vu dans sa définition « une réponse générale, puissante et satisfaisante au problème de la nature de la vérité en mathématique » puisque, en tant que définition de la vérité il s'agit d'une tautologie, comme le montre très bien ta discussion ci-dessus : la formule « il neige » est vraie dans un modèle si... dans ce modèle il neige. Attention je ne dis pas que cette définition n'a aucun sens, elle en a beaucoup puisqu'elle fonde la théorie des modèles en distinguant clairement la formule et son interprétation ; je dis juste que je doute que Tarski y ait vu ce qui est prétendu de façon un peu grandiloquente ici, d'autant plus que le même Tarski a démontré que l'on ne pouvait pas définir mathématiquement la vérité en mathématique.

Cela étant tu m'as convaincu qu'il fallait garder l'exemple de la neige, non pas pour comprendre ce qu'est la vérité en mathématique mais pour la distinction syntaxe/sémantique entre la phrase « il neige » et le fait qu'il neige dans le monde, ce qui est sans doute ce que Tarski avait en tête. Il faudrait une citation précise pour ça, mais je n'en ai pas.

Laurent de Marseille (discuter) 10 octobre 2016 à 14:29 (CEST)

J'ai enfin pu jeter un oeil au papier de Tarski « Le concept de vérité dans les langages formalisés », comme je le supposais l'affirmation sus-citée est absolument fausse, bien au contraire, Tarski explique dès l'introduction de l'article que la réponse qu'il apporte au problème de la vérité est négative pour le langage naturel (coloquial language), négative pour le système formel en vigueur à son époque (Calcul des classes avec une infinité de classes), négative également pour un langage qui je crois correspond à ce que l'on appelle aujourd'hui calcul des prédicats du premier ordre, et finalement positive seulement pour un fragment du système de classes comportant seulement un nombre fini de classe. Je n'ai pas eu le temps de comprendre pleinement ce que sont tous ces systèmes et à quoi ils correspondent dans le langage moderne mais il semble clair que cette phrase est ridiculement exagée, je l'ai donc enlevée. --Laurent de Marseille (discuter) 1 novembre 2016 à 16:58 (CET)

rajout de deux lignes

Comme je disais au chapitre précédent, la logique mathématique n'est pas mon domaine de base, j'ai rajouté les 2 lignes: "Pour qu'un énoncé utilisant un ensemble de symbole définit par un langage ${\mathcal {L}}$ soit considéré comme vrai, c'est à dire qu'on puisse dire qu'il soit un théorème, il faut et il suffit que toutes les ${\mathcal {L}}$-structures satisfassent l'énoncé."

n'hésitez à les corriger si besoin, a mon avis si erreur il y a, il s'agit de vocabulaire mal choisi et non du sens de la phrase.--Nicobzz (discuter) 9 octobre 2016 à 21:45 (CEST)

Et Skolem dans tout cela?

L'article sur Skolem dit « C'est un pionner de la théorie des modèles ». Il prend la suite de Leopold Löwenheim qui en 1915 démontre un théorème en théorie des modèles. Est-ce qu'attribuer tant de paternité à Tarski n'est pas exagéré? --Pierre de Lyon (discuter) 23 janvier 2017 à 14:13 (CET)

À relire

Je suis tombé un peu par hasard, pour corriger un détail de formulation, sur un fatras d'énormités basiques dans la section Catégoricité. Je les ai retirées, mais je m'aperçois en consultant l'historique que la même IP a ajouté un paragraphe sur la omega-stabilité, sujet que je ne connais quasiment pas, donc il me faudrait du temps pour vérifier, mais il y a de quoi être inquiet.

Après lecture en diagonale il y a pas mal de choses bizarres, du vocabulaire non standard, qui résultent principalement d'interventions sous IP de janvier 2017. Des références ont disparu à l'occasion. Proz (discuter) 14 janvier 2020 à 00:07 (CET)

Je ne suis pas tropqualifié sur ce sujet, mais je continue à suivre l'article et donc tes améliorations. --Pierre de Lyon (discuter) 14 janvier 2020 à 09:09 (CET)

Satifaisabilité ??? Pourquoi pas plutôt Réalité ou Vérifiabilité que ce néologisme bancal ?

Bonjour,
Je n'ai rien contre les néologismes pourvu qu'ils soient rendus nécessaires (pour réduire la longueur des discours ou introduire un nouveau concept, à titres d'exemple) en l'absence d'une préexistant et bien construits (je serai hors sujet à être complet et précis).
Satisfaisabilité ne me semble ni répondre à la première condition ni à la seconde.

• Vérifiabilité semble pouvoir convenir (sauf si c'est déjà pris pour exprimer un autre concept) car dans la langue française courante, même s'il peut y avoir des abus de langage (comme dans toute langue naturelle), c'est bien en "allant voir le réel" qu'on vérifie l'absence d'erreur de calcul, la présence d'un objet, l'existence d'un évènement, etc.
• Réalité serait une alternative excellente (ma préférée) s'il n'y avait pas autant de flou dans la langue vulgaire. La réalité d'une chose c'est la capacité de vérification qu'elle appartient bien au réel.
• Le simple fait de devoir écrire « Par exemple, il distingue la proposition "il neige" de l'observation du fait qu'il neige effectivement dans le monde réel. Pour cela, Tarski introduit le concept de satisfaisabilité, au sens que la proposition "il neige" est satisfaite par la réalité », pour éclairer le sens à donner au néologisme, suffit à démontrer en quelque sorte sa bancalité d'une part et le lien nécessaire de référence au réel d'autre part (qui permet de le distinguer de l'idéalité ou de l'illusion, ce dernier point problématique étant évacuée en silence par l'exemple de la neige qui tombe, ceci dit en passant).
• Satisfaire est un peu trop passe-partout on satisfait aux attentes d'une personne, à une opinion, à une condition implicite ou explicite, etc. que ce soit nécessairement réel vu qu'il suffit que l'illusion soit crédible.

En guise de conclusion réalité est le plus approprié (à mon humble avis) quitte à préciser (bien qu'en mathématique on soit habitué à s'en dispenser, la définition faisant foi) que c'est précisément en relation au réel définit comme effectif (effectivavilité ??? pas terrible) et non illusoire.

Pour une fois qu'un article mathématique fait un peu de pédagogie et de vulgarisation (ça existe mais ce sont des exceptions) plutôt que de se jeter le plus rapidement possible dans des notations mathématiques (c'est comme l'orthographe ça parait constant mais ça n'a jamais cessé d'évoluer) que seuls des mathématiciens patentés ou de jeunes encore dans les études scientifiques ou fraichement sortis de celles-ci (moins de 40 ans assurément) peuvent lire sans problème, ce serait vraiment dommage de tout gâcher par un néologisme mal né.
Cordialement.--Overkilled ^[discuter] 24 octobre 2020 à 21:51 (CEST)

Après avoir lu l'article satisfaisabilité (que c'est moche mais bon) je m'interroge. S'agit-il ici exactement du même concept ? Si oui, alors l'exemple pédagogique du "il neige" est probablement à récrire pour mieux cibler le concept et gommer le surplus de possibles. Ne serait-ce qu'en précisant qu'il faut et suffit de trouver un endroit où il neige pour que la satisfaisabilité soit effective (ou vraie). Sauf que je n'ai pas les compétences pour le déterminer par moi-même, ça reste donc une suggestion sous condition que...--Overkilled ^[discuter] 25 octobre 2020 à 01:17 (CEST)

C'est la transcription de "satisfiability" en anglais, dans le même sens que pour le problème SAT (qui en est une exemple élémentaire vec des valeurs booléennes binaires). On peut l'utiliser pour un système d'équation par exemple : "x est un nombre entier, est-ce qu'il existe une valeur pour laquelle x*x=-1 ?" est un problème de satisfaisabilité, non satisfaisable en l'occurrence, on ne peut pas trouver d'entier de carré négatif). On dit aussi "réalisabilité" parfois mais c'est un truc légèrement différent on dirait. "Vérité" renverrait à une tautologie (logique), ou un théorème (par exemple si à la place de "x*x=-1" on prends "x>0" c'est vrai quelle que soit la valeur de x), dans le langage de la théorie des modèle ce serait quelque chose de vrai dans tout modèle. C'est toujours un peu casse figure de nommer certaines notions pointues, il y a des nuances parfois subtiles qui poussent à des néologismes et pas nécessairement de norme ultra finalisée. — TomT0m ^[bla] 25 octobre 2020 à 17:21 (CET)

(Tu me donnes des souvenirs d'un prof de logique Russe qui lui ne s'embarrassait pas et disait "satisfiabilité" qui ne me choquerait du coup même pas :) ) — TomT0m ^[bla] 25 octobre 2020 à 17:48 (CET)

Il me reste quelques restes de mathématique et je n'ai donc jamais été étonné que des termes d'usage courant puissent avoir un sens très réduit et précis en mathématique (sinon ça ne serait pas des maths sinon une varinate floue, je l'avais bien compris). J'avais également deviné que c'était probablement un anglicisme (que je puisse le trouver malheureux n'est pas mathématique non plus). Ce qui m'a vraiment embarrassé (et me chagrine toujours) c'est l'analogie pédagogique du "il neige". Dans sa rédaction actuelle, pour un candide tel que moi-même j'ai l'impression que ça conduit à trop de possibilités autres que celle qu'il conviendrait de retenir pour appréhender (s'initier) correctement à ce concept mathématique de faisabilité. L'exemple laisse entendre qu'il suffirait qu'il neige (quelque part) pour que la faisabilité soit vraie. Or j'ai plutôt l'impression désormais après les exemples que tu m'as fourni que c'est en fait bien plus proche de la notion de "faisabilité/possibilité réalisable" du langage courant, transposé dans la rigueur des mathématiques évidemment.--Overkilled ^[discuter] 25 octobre 2020 à 20:02 (CET)

Satisfaisabilité est un terme technique utilisé en logique mathématique (pour le fait qu'une formule soit satisfaisable), construit sur satisfaisable comme l'anglais satisfiability sur satisfiable (ça ne veut pas dire que c'est un anglicisme). On ne va pas le remettre en cause sur wikipedia ! La réalisabilité est effectivement autre chose (on interprète par des programmes en gros). L'image donnée vaut ce qu'elle vaut (elle n'est pas à développer en tout cas, sous peine d'encore plus obscurcir), je ne sais pas d'où elle sort, mais le commentaire me laisse penser qu'elle n'est pas si mauvaise (ce que l'exemple laisse entendre est effectivement ce qui est attendu). La satisfaisabilité n'a pas le sens de faisabilité. C'est dérivé du sens de satisfaire au sens de satisfaire des conditions par exemple. Proz (discuter) 25 octobre 2020 à 20:56 (CET)

Merci pour toutes ces précisions. Le jargon ne se discute pas, surtout en mathématique et c'est à moi-même qu'il revient de comprendre ce que ça recouvre. Maintenant il faut croire que ce concept est relativement nouveau vu que satisfaisable et satisfiable n'existent pas encore en français hors du domaine des mathématiques. Ce qui autorise à dire que ce n'est encore à ce jour qu'un néologisme calqué sur l'anglais (probablement emprunté au franco-normand) et donc bel et bien un anglicisme jusqu'à preuve du contraire. C'est pas un jugement de valeur, c'est factuel. Mais c'est également hors sujet ici. En tout cas merci d'avoir apporté un peu de lumière à ma lanterne de curieux d'apprendre.--Overkilled ^[discuter] 26 octobre 2020 à 00:31 (CET)

Satisfaisable existe déjà au XIXe https://www.cnrtl.fr/definition/satisfaisable (satisfiable est a priori directement emprunté à l'anglais, satisfaisabilité est forgé sur satisfaisable, selon une construction commune). Proz (discuter) 26 octobre 2020 à 09:52 (CET)

Une seule occurrence citée (Goncourt,Ch. Demailly,1860, p. 165), c'est suffisant à en prouver l'existence mais très insuffisant (faible) pour en prouver l'usage commun. L'avenir nous dira quelle place il prendra ou ne prendra pas à côté de possible ou facile.--Overkilled ^[discuter] 26 octobre 2020 à 11:54 (CET)

Et pourquoi pas sémantiquement consistant que je ne conaissais pas et que je découvre dans La Grande encyclopédie. 13, Marconi-mouvement / Larousse de 1975, en faisant un recherche sur Gallica ? --Pierre de Lyon (discuter) 26 octobre 2020 à 18:30 (CET)