Formule logique

L'utilisation clé de formules est en logique propositionnelle, telle que la logique du premier ordre. Dans ce contexte, une formule est une chaîne de symboles φ pour lesquels il faut se demander «est ce que φ vrai?», une fois que toutes les variables libres dans φ ont été instancié. En logique formelle, les démonstrations peuvent être représentées par des suites de formules munis de certaines propriétés, et la formule finale est ce qui est prouvé.

Les formules sont des objets syntaxiques. Elles sont donnés par des interprétations. Par exemple, dans une formule propositionnelle, chaque variable propositionnelle peut être interprétée comme une proposition concrète, de sorte que la formule globale exprime une relation entre ces propositions.

Les formules issues du calcul des propositions, aussi appelées formules propositionnelles[1], sont des expressions de la forme ${\displaystyle A\land (B\land C)}$ . Leur définition commence par le choix arbitraire d'un ensemble V de variables propositionnelles. L'alphabet se compose des lettres de V avec les symboles correspondants aux conjonctions et aux parenthèses propositionnelles « ( » et « ) », qui sont tous supposés ne pas être en V. Les formules seront certaines expressions (c'est-à-dire, des chaînes de symboles) sur cet alphabet. Les formules sont inductivement définies comme suit:

• Chaque variable propositionnelle est, en soi, une formule.
• Si φ est une formule, alors ${\displaystyle \lnot }$φ est une formule.
• Si φ et ψ sont des formules, et • est n'importe quelle connecteur binaire, alors ( φ • ψ) est une formule. Ici • pourrait être (mais sans y être limité) un des opérateurs usuels ∨, ∧, →, ou ↔.Cette définition peut aussi être écrite en grammaire formelle sous la forme de Backus-Naur, à condition que l'ensemble des variables est finie:

  <alpha set> ::= p | q | r | s | t | u | ... (ensemble fini arbitraire de variables propositionnelles)

  <form> ::= <alpha set> | ${\displaystyle \neg }$<form> | (<form>${\displaystyle \wedge }$<form>) | (<form>${\displaystyle \vee }$<form>) | (<form>${\displaystyle \rightarrow }$<form>) | (<form>${\displaystyle \leftrightarrow }$<form>)

En utilisant cette grammaire, la suite de symboles

(((p ${\displaystyle \rightarrow }$ q) ${\displaystyle \wedge }$ (r ${\displaystyle \rightarrow }$ s)) ${\displaystyle \vee }$ (${\displaystyle \neg }$q ${\displaystyle \wedge }$ ${\displaystyle \neg }$s)) est une formule, car elle est grammaticalement correcte. La suite de symboles

((p ${\displaystyle \rightarrow }$ q)${\displaystyle \rightarrow }$(qq))p))

n'est pas une formule, car elle ne se conforme pas à la grammaire.

Une formule complexe peut être difficile à lire, en raison, par exemple, de la prolifération des parenthèses. Pour remédier à ce problème, les règles de priorité (semblable à l'ordre mathématique standard des opérations) sont imposées entre les opérateurs, ce qui rend certains opérateurs plus contraignant que d'autres. Par exemple, en supposant que la priorité (du plus contraignant au moins contraignante) 1. ${\displaystyle \neg }$ 2. ${\displaystyle \rightarrow }$ 3. ${\displaystyle \wedge }$ 4. ${\displaystyle \vee }$. Ainsi, la formule

(((p ${\displaystyle \rightarrow }$ q) ${\displaystyle \wedge }$ (r ${\displaystyle \rightarrow }$ s)) ${\displaystyle \vee }$ (${\displaystyle \neg }$q ${\displaystyle \wedge }$ ${\displaystyle \neg }$s))peut être abrégé

p ${\displaystyle \rightarrow }$ q ${\displaystyle \wedge }$ r ${\displaystyle \rightarrow }$ s ${\displaystyle \vee }$ ${\displaystyle \neg }$q ${\displaystyle \wedge }$ ${\displaystyle \neg }$s

Ceci est, cependant, seule une convention utilisée pour simplifier la représentation d'une formule écrite.

La définition d'une formule dans la logique du premier ordre ${\displaystyle {\mathcal {QS}}}$ est relative à sa signature de la théorie en question. Cette signature spécifie les symboles constants, de relation, et les symboles de fonction de la théorie, ainsi que les arités des symboles de fonction et de relation.

La définition d'une formule vient en plusieurs parties. Tout d'abord, l'ensemble des termes est défini de manière récursive. Les termes, de façon informelle, sont des expressions qui représentent des objets du domaine du discours.

1. N'importe quelle variable est un terme.
2. Tout symbole constant de la signature est un terme
3. une expression de la forme f(t₁,...,t_n), où f est un symbole de fonction n-aire, et t₁,...,t_n sont des termes, est encore un terme.

L'étape suivante consiste à définir les formules atomiques.

1. Si t₁ et t₂ sont des termes, alors t₁=t₂ est une formule atomique.
2. Si R est un symbole de relation n-aire, et t₁,...,t_n sont des termes, alors R(t₁,...,t_n) est une formule atomique.

Enfin, l'ensemble des formules est défini comme étant le plus petit ensemble contenant l'ensemble des formules atomiques tel que :

1. ${\displaystyle \neg \phi }$ est une formule quand${\displaystyle \ \phi }$ est une formule
2. ${\displaystyle (\phi \land \psi )}$et ${\displaystyle (\phi \lor \psi )}$ sont des formules quand${\displaystyle \ \phi }$ et ${\displaystyle \ \psi }$ sont des formules;
3. ${\displaystyle \exists x\,\phi }$ est une formule quand${\displaystyle \ x}$ est une variable et${\displaystyle \ \phi }$ est une formule;
4. ${\displaystyle \forall x\,\phi }$ est une formule quand${\displaystyle \ x}$ est une variable et${\displaystyle \ \phi }$ est une formule (alternativement, ${\displaystyle \forall x\,\phi }$ peut être défini comme étant une abréviation de ${\displaystyle \neg \exists x\,\neg \phi }$).

Si une formule n'a aucune occurrence de ${\displaystyle \exists x}$ ou ${\displaystyle \forall x}$, pour toute variable ${\displaystyle \ x}$, elle est alors appelée sans-quantificateur. Une formule existentielle est constituée d'une suite de quantifications existentielles suivie par une formule sans-quantificateur.

Une formule atomique est une formule qui ne contient pas de connecteurs logiques ni de quantificateurs. La forme précise de formules atomiques dépend du système formel en question; pour la logique propositionnelle, par exemple, les formules atomiques sont des variables propositionnelles. Pour le calcul des prédicats, les formules atomiques sont des symboles de prédicat avec leurs arguments, chaque argument étant un terme.

Selon sa terminologie, une formule ouverte est formée en combinant des formules atomiques en utilisant uniquement des connecteurs logiques, excluant les quantificateurs[2]. Elle ne doit pas être confondue avec une formule qui n'est pas fermée.

• Une formule A dans un langage ${\displaystyle {\mathcal {Q}}}$ est valide si elle est vraie pour toute interprétation de ${\displaystyle {\mathcal {Q}}}$.
• Une formule A dans un langage ${\displaystyle {\mathcal {Q}}}$ est satisfaisable si elle est vraie pour quelques interprétations de ${\displaystyle {\mathcal {Q}}}$.
• Une formule A du langage de l'arithmétique est décidable si elle représente un ensemble décidable, à savoir s'il existe une méthode efficace qui, étant donné une substitution des variables libres de A, dit si A est prouvable ou si sa négation l'est.

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Well-formed forumla » (voir la liste des auteurs).

• Formule (logique mathématique)
• Formule propositionnelle
• Formes normales conjonctives et formes normales disjonctives
• Logique, logique classique, logique intuitionniste, logique minimale, logique linéaire, logique infinitaire
• Syllogisme
• Idéographie
• Lambda-calcul
• Logiques multi-valuées
• Logique de description

• René Cori, Daniel Lascar, Logique mathématique, tome 1 : Calcul propositionnel, algèbre de Boole, calcul des prédicats [détail des éditions]

• Terminologie et ontologie - Cairn.info
• La sémantique propositionnelle
• La nature des théories scientifiques
• (en) Well-Formed Formula for First Order Predicate Logic - inclut un court test en Java.
• (en) Well-Formed Formula at ProvenMath