Discussion:Système formel

"Vérité" ???

A la fin du chapitre L’énumérabilité des théories axiomatiques, il est question de 'proposition vraie', mais nulle part n'est définie la notion de vérité?

Thibautlg (d) 8 janvier 2009 à 14:44 (CET)

Systèmes formels et informatique

Je considère que la partie langage informatique qui énonce que qu'un langage informatique dispose d'une sémantique opérationnelle est plutôt fausse. Un langage comme Haskell n'en définit pas, il ne définit qu'une sémantique dénotationnelle. Sedrikov (d)

Je maintiens : tout langage informatique a une sémantique opérationnelle, y compris Haskell. Peut-être devrais-je relativiser et ajouter tout langage informatique implémenté sur un ordinateur que ça soit sous forme d'interprète, de compilo, ou autre, l'implémentation étant la définition (très formelle il est vrai) de la sémantique opérationnelle du langage. C'est du reste ce qui est dit dans l'article : « La sémantique opérationnelle d'un langage est en général réalisée par un programme ». Laurent de Marseille (d) 9 mai 2012 à 22:48 (CEST)

Contradiction ? ce serait un comble !!!

 Sedrikov :,  Lregnier :,  Proz :. Je ne suis pas spécialiste en logique mathématique, juste un peu ingénieur... et je pense qu'il y a une erreur dans le § Cohérence. L'énoncé de la cohérence d'une théorie axiomatique ne me semble pas exact... Les exemples sont en contradiction avec l'énoncé... me semble-t-il !!! D'autre part il manque des sources à toutes les définitions, affirmations, développements, etc de cet article... A toutes fins utiles... Guy6631 (discuter) 20 juillet 2021 à 10:41 (CEST)

La formulation est bizarre, mais je ne pense pas qu’elle soit fausse. En fait, je pense qu’il est plus naturel de définir l’incohérence d’abord (toute formule est conséquence des axiomes, et en particulier, on peut prouver la formule "faux"). L’exemple "0=1" est une formule qu’on ne sait pas démontrer à partir des seuls axiomes de Peano (ou sinon, on est dans le caca !). Incohérent, c’est donc que tout est démontrable, y compris des énoncés contradictoires, Cohérent, c’est il existe quelque chose de non démontrable. Note que si deux énoncés contradictoires sont démontrables, alors tout énoncé est démontrable. Donc être cohérent implique ne pas contenir de contradiction.

Tout ça, c’est raconté avec les mains, car il y a des subtilités, par exemple la théorie (pas très intéressante) qui ne possède qu’une seule formule (disons "Vrai"), et qui a un axiome qui suppose "Vrai". Alors d’après cette définition, cette théorie serait incohérente. Ce n’est peut être qu’un problème de définition, et ce n’est sans doute pas très utile de s’attarder sur ce genre de cas plutôt dégénéré.

~~~ Sedrikov (discuter) 7 février 2024 à 16:02 (CET)