Des excuses sont peut-être justifiées pour avoir posé une autre question sur les conditions préalables, mais j'étais confus quant aux points de départ. Je suis tombé sur divers termes tels que "Logique modale", "Logique temporelle", "Logique du premier ordre", "Logique du second ordre" et "Logique de l'ordre supérieur".

Que veut dire "logique" dans ce contexte? Comment définissons-nous rigoureusement le mot "logique"?

Après avoir parcouru les pages de début de quelques livres, je peux en conclure que "la logique est un moyen de décider de ce qui suit et est importante dans la conception de langages de programmation car elle dicte et facilite la conception de programmes pour raisonner et comprendre automatiquement les programmes. Je veux comprendre le deuxième point de manière un peu élaborée.

J'en viens maintenant à ces logiques.

Toutes ces logiques, "Logique temporelle", "Logique modale", "Logique du premier ordre", "Logique de l'ordre supérieur", sont-elles indépendantes les unes des autres ou avons-nous besoin de comprendre quelques unes de ces logiques pour comprendre quelques-unes de ce groupe? En un mot, quels seront les préalables pour eux? (Ce sera formidable si je peux également obtenir des suggestions sur certains matériaux.)

PS: Merci beaucoup pour votre gentillesse

Fondamentalement, une logique consiste en deux choses.

• La syntaxe est un ensemble de règles qui déterminent ce qui est ou non une formule.
• La sémantique est un ensemble de règles qui déterminent quelles formules sont "vraies" et quelles sont "fausses". Pour un théoricien du modèle , cela s'exprime en rapportant des formules aux structures mathématiques dans lesquelles elles sont vraies; pour un théoricien de la preuve , la vérité correspond à la prouvabilité à partir d'un ensemble choisi d'axiomes avec un ensemble choisi de règles de preuve (techniques).

La différence entre des logiques différentes réside le plus simplement dans le choix de la syntaxe et de la sémantique. La plupart des logiques sont des extensions de la logique propositionnelle ou du premier ordre . En un sens, vous pouvez voir ces extensions comme "ajoutant plus de fonctionnalités" à la logique. Par exemple, les logiques temporelles traitent de vérités qui peuvent varier dans le temps.

En général, ces caractéristiques pourraient être exprimées dans une logique plus simple, au prix de devoir écrire des formules plus longues. Par exemple, le concept temporel "  est vrai à partir de ce moment-là pour l'éternité" peut être exprimé dans le premier ordre en ajoutant un paramètre de temps à toutes vos propositions et en disant "Pour tous les temps  , si  est supérieur ou égal à à l'heure actuelle, alors  est vrai à l'instant  . " En un sens, vous pouvez considérer ces logiques comme l'ajout de bibliothèques à un langage de programmation de base afin de pouvoir dire des choses plus facilement.$\varphi$$t$$t$$\varphi$$t$

Étant donné que presque toutes les logiques sont basées sur des logiques propositionnelles et de premier ordre, je vous conseillerais de vous familiariser d'abord avec celles-ci.

Bien que des domaines tels que l'informatique, les mathématiques et la physique soient relativement bien organisés, Logic a une histoire chaotique. Son organisation est vraiment déroutante et je pense qu'il est important de lire un peu d'histoire pour comprendre la structure dense du domaine.

Le chemin que vous devez choisir dépendra de votre arrière - plan et objectifs .

Qu'est-ce qu'une logique?

1. Selon le point de vue traditionnel, une logique est un système formel avec un langage formel (syntaxe), une sémantique (sens externe, penser aux interprètes de programmes) et un ensemble de règles permettant de déduire des déclarations d’autres (pensez aux règles de réductions de programmes). Une logique est purement considérée comme un simple objet mathématique.

2. Le point de vue moderne, dit, à travers le célèbre isomorphisme de Curry-Howard, qu’une logique est un système de types cohérent (les preuves sont des programmes et les types sont des formules). Plus précisément: un système de règles d'inférences bénéficiant du théorème d'élimination de coupe et du théorème de Church-Rosser / théorème de confluence impliquant que le système de programmation sous-jacent se comportera bien.

3. Concernant les ordres, la logique propositionnelle peut être vue comme un système d'ordre 0 (supposons que les variables des propositions soient notées ). Ils se comportent comme des fonctions sans arguments (constantes).$p, q$

   • Lorsque nous passons à la logique du premier ordre, les variables des propositions deviennent les variables des prédicats et prennent un objet comme argument , . Ils se comportent comme des fonctions prenant des objets (paires, entier, chaîne) sont des arguments. Pensez à la langue C.P ( x 1 , . . . , X n ) Q ( x 1 , . . . , X n$P, Q$$P(x_1, ..., x_n)$$Q(x_1, ..., x_n)$
   • Dans la logique du second ordre, la variable des prédicats devient une sorte de fonction prenant celle du premier ordre. Ils se comportent comme des fonctions prenant comme argument des fonctions du premier ordre. Par exemple, nous pouvons avoir des prédicats et une quantification par rapport aux prédicats.
   • Même raisonnement pour le troisième ordre, etc. Les logiques d'ordre supérieur acceptent n'importe quel ordre. Pensez à Haskell et OCaml qui ont des fonctions prenant des fonctions de fonctions de fonctions, etc. en argument.

4. En général, il n'y a pas de consensus sur ce qu'est une logique. Certains philosophes utilisent des systèmes qui ne disposent pas d'un système de programmation sous-jacent cohérent. En fait, je dirais que chaque domaine utilisant Logic a sa propre conception de la logique. Et la plupart des mathématiciens ne se soucient probablement pas de ce qu'est une logique.

La structure du terrain

L’historique de la logique est trop volumineux, je vais donc vous donner la structure du champ. Le domaine de la logique formelle est scindé en deux catégories: utilisation philosophique, mathématique et informatique. La logique formelle commence au 19-20e siècle.

• Vous devez d’abord étudier la logique propositionnelle et la logique du premier ordre . Ce sont les plus standards. Ils ont été créés pour donner un compte formel / mathématique à l'ancienne logique de l'époque de la Grèce antique.

  • Théorie des modèles (sémantique), étude des structures mathématiques du point de vue de la logique
  • La théorie de la preuve (syntaxe), indépendamment, étudie les preuves en tant qu'objet mathématique.

• La logique du second ordre est une extension de la logique du premier ordre qui est une extension de la logique propositionnelle. Il est particulièrement intéressant car les arithmétiques "vivent" au second ordre (prédicats sur les prédicats avec induction). De même, la topologie vit dans le "troisième ordre" (prédicats sur des ensembles qui peuvent être vus comme prédicats eux-mêmes).

• Puis vint LEJ Brouwer qui divisa la logique en deux:

  • La logique classique est la logique habituelle telle que définie auparavant. En particulier, pour tout , tient pas (exclu milieu).A ∨ ¬ $A$$A \lor \lnot A$
  • La logique intuitionniste est une sorte de logique rejetant le tiers exclu et toutes les lois équivalentes (pour des raisons techniques et philosophiques, je ne l'expliquerai pas ici).

• Dans un autre contexte, les philosophes se sont intéressés à la logique formelle et ont pensé qu’elle pouvait répondre à des questions philosophiques (philosophie analytique). Ils ont créé leurs propres systèmes logiques indépendants (logiques paraconsistantes, logiques de pertinence et modales telles que les logiques déontiques, les logiques temporelles, les logiques épistémiques, ...). La logique modale ne fonctionne pas avec la vérité, mais avec des modalités telles que la possibilité, la nécessité, le temps, la connaissance. Ils sont tous indépendants des logiques ci-dessus.

• La correspondance de Curry-Howard donne une correspondance formelle (isomorphisme) entre les preuves et les programmes. Maintenant, beaucoup de logiques peuvent être considérées comme des systèmes de programmation et inversement. La logique intuitionniste qui était un peu ignorée est maintenant considérée comme un système de programmation fonctionnel ( -calculus). Cela mène à l'étude de la théorie des types . C'est un sujet de recherche actuellement actif.$\lambda$

• Les informaticiens voulaient vérifier et prouver la soudaineté des systèmes de manière formelle et il semble que les logiques modales soient pertinentes. Aujourd'hui, ils utilisent des logiques temporelles et modales pour raisonner sur des systèmes (voir: méthodes formelles, vérification de modèle). Les systèmes sont modélisés via la théorie des automates (par exemple) et sont vérifiés à l'aide d'outils logiques. Cela a conduit à la logique temporelle linéaire (LTL) et à la logique d'arbre informatique (CTL) .

• Dans la même motivation, les informaticiens voulaient vérifier la validité et prouver les propriétés des programmes. Nous avons donc inventé la logique de Hoare pour les programmes impératifs et plus généralement, la logique de séparation .

• En étudiant l'isomorphisme de Curry-Howard, une nouvelle logique est apparue: la logique linéaire qui restreint les règles structurelles (affaiblissement et contraction) considérées comme l'effacement et la duplication opérant dans les preuves et les programmes. L'infinité potentielle de la vérité est expliquée. Il semble que cette logique soit une généralisation de la logique classique et de la logique intuitionniste et donne une toute nouvelle conception de la logique basée sur le calcul et un paradigme procédural. Il est principalement étudié par des informaticiens.

• La logique linéaire provient également de ce que nous appelons la logique sous- structurelle rejetant les règles structurelles de la logique. La logique pertinente et la logique affine sont des exemples de tels systèmes.

Résumé et sélection du chemin

• Toute logique peut être: logique propositionnelle, ordre du premier ordre, ordre du deuxième ordre, ordre du troisième ordre, ..., ordre supérieur (chacune étant la précédente).

• Nous pouvons ajouter ou supprimer des règles pour créer des variantes des systèmes existants:

  • Supprimer les tiers exclus: logique intuitionniste
  • Ajouter des modalités: logiques modales
  • Limiter la contradiction et l’affaiblissement: logique linéaire
  • Supprimer la contraction: logique affine
  • Supprimer l'affaiblissement: logique pertinente
  • Traiter la négation différemment: logique paraconsistante

• Apprenez d'abord la logique propositionnelle et de premier ordre et:

  • théorie des modèles, deuxième ordre, ordre supérieur si vous êtes intéressé par les mathématiques
  • théorie de la preuve, logique intuitionniste, second ordre, logique linéaire si vous êtes intéressé par les fondements de l'informatique
  • logiques modales, logiques hoare, logiques de séparation si la vérification des systèmes et des programmes vous intéresse
  • logiques modales, logiques non classiques en général si la philosophie vous intéresse

Références (livres)

Je recommande personnellement de mélanger des références, si possible.

• Mathematical Logic (Chiswell & Hodges) : Livre très concis et simple pour commencer.
• Un premier cours en logique (Hedman) : un peu comme le précédent mais donnez plus de détails et prenez en compte la calculabilité.
• Manuel de logique pratique et de raisonnement automatisé (Harrison) : Si vous souhaitez comprendre comment certains concepts liés à la logique sont mis en œuvre dans la pratique. Plus orienté vers le raisonnement automatisé.
• Logique en informatique (Huth & Ryan) : très clair et orienté vers les informaticiens (vérification de programmes et de systèmes, logique de Hoare, utilisation pratique de la logique modale, logique temporelle, vérification de modèle).
• Introduction à la théorie de la preuve (Buss) : introduction à la théorie de la preuve. Il serait préférable de lire ceci après une logique générale.

Références (Wikipedia)

• https://en.wikipedia.org/wiki/Philosophical_logic
• https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
• https://en.wikipedia.org/wiki/Non-classical_logic
• https://en.wikipedia.org/wiki/Intuitionistic_logic
• https://en.wikipedia.org/wiki/Modal_logic
• https://en.wikipedia.org/wiki/Model_theory
• https://en.wikipedia.org/wiki/Proof_theory
• https://en.wikipedia.org/wiki/Linear_temporal_logic
• https://en.wikipedia.org/wiki/Computation_tree_logic
• https://en.wikipedia.org/wiki/Separation_logic
• https://en.wikipedia.org/wiki/Hoare_logic
• https://en.wikipedia.org/wiki/Linear_logic
• https://en.wikipedia.org/wiki/Substructural_logic

Toutes ces logiques se retrouvent sous la logique mathématique .

La logique mathématique est souvent divisée en domaines de la théorie des ensembles, de la théorie des modèles, de la théorie de la récursivité et de la théorie de la preuve. Ces domaines partagent des résultats de base sur la logique, en particulier la logique du premier ordre, et la définissabilité. En informatique (en particulier dans la classification ACM), la logique mathématique englobe des sujets supplémentaires qui ne sont pas détaillés dans cet article; voir Logique en informatique pour ceux-là.

De plus, si vous voulez connaître la logique en termes généraux, cet article pourrait être utile.

La logique, qui signifiait à l'origine "le mot" ou "ce qui est dit", mais qui en vient à signifier "pensée" ou "raison", est un sujet qui concerne les lois les plus générales de la vérité et qui est généralement considérée comme une étude systématique. de la forme d'inférence valide. Une inférence valide en est une où il existe une relation spécifique de support logique entre les hypothèses de l'inférence et sa conclusion.