Formule bien formée - Well-formed formula

Dans la logique mathématique , la logique propositionnelle et la logique des prédicats , une formule bien formée , en abrégé WFF ou WFF , souvent simplement la formule , est une finie séquence de symboles d'une donnée alphabet qui fait partie d'un langage formel . Un langage formel peut être identifié avec l'ensemble de formules dans le langage.

Une formule est un objet syntaxique auquel on peut donner une signification sémantique au moyen d'une interprétation. Deux utilisations clés des formules sont la logique propositionnelle et la logique des prédicats.

introduction

Une utilisation clé des formules est dans la logique propositionnelle et la logique de prédicat telle que la logique du premier ordre . Dans ces contextes, une formule est une chaîne de symboles φ pour laquelle il est logique de demander "est φ vrai?", Une fois que toutes les variables libres de φ ont été instanciées. En logique formelle, les preuves peuvent être représentées par des séquences de formules avec certaines propriétés, et la formule finale de la séquence est ce qui est prouvé.

Bien que le terme «formule» puisse être utilisé pour des marques écrites (par exemple, sur un morceau de papier ou un tableau noir), il est plus précisément compris comme la séquence de symboles exprimée, les marques étant une instance symbolique de formule. Ainsi, la même formule peut être écrite plus d'une fois, et une formule peut en principe être si longue qu'elle ne peut pas être écrite du tout dans l'univers physique.

Les formules elles-mêmes sont des objets syntaxiques. On leur donne des significations 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. Une formule n'a cependant pas besoin d'être interprétée pour être considérée uniquement comme une formule.

Calcul propositionnel

Les formules du calcul propositionnel , également appelées formules propositionnelles , sont des expressions telles que . Leur définition commence par le choix arbitraire d'un ensemble V de variables propositionnelles . L'alphabet se compose des lettres en V ainsi que les symboles pour les conjonctions propositionnel et entre parenthèses « ( » 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 définies inductivement comme suit:

  • Chaque variable propositionnelle est, à elle seule, une formule.
  • Si φ est une formule, alors ¬φ est une formule.
  • Si φ et ψ sont des formules, et • est n'importe quel connecteur binaire, alors (φ • ψ) est une formule. Ici • pourrait être (mais sans s'y limiter) les opérateurs habituels ∨, ∧, → ou ↔.

Cette définition peut également être écrite sous forme de grammaire formelle sous forme de Backus – Naur , à condition que l'ensemble des variables soit fini:

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> | ¬<form> | (<form><form>) | (<form><form>) | (<form><form>) | (<form><form>)

En utilisant cette grammaire, la séquence de symboles

((( p q ) ∧ ( r s )) ∨ (¬ q ∧ ¬ s ))

est une formule, car elle est grammaticalement correcte. La séquence de symboles

(( p q ) → ( qq )) p ))

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

Une formule complexe peut être difficile à lire, en raison, par exemple, de la prolifération des parenthèses. Pour atténuer ce dernier phénomène, des règles de priorité (apparentées à l' ordre mathématique standard des opérations ) sont supposées parmi les opérateurs, rendant certains opérateurs plus contraignants que d'autres. Par exemple, en supposant la priorité (de la plus contraignante à la moins contraignante) 1. ¬ 2. → 3. ∧ 4. ∨. Puis la formule

((( p q ) ∧ ( r s )) ∨ (¬ q ∧ ¬ s ))

peut être abrégé en

p q r s ∨ ¬ q ∧ ¬ s

Il ne s'agit cependant que d'une convention utilisée pour simplifier la représentation écrite d'une formule. Si la priorité était supposée, par exemple, être associative gauche-droite, dans l'ordre suivant: 1. ¬ 2. ∧ 3. ∨ 4. →, alors la même formule ci-dessus (sans parenthèses) serait réécrite comme

( p → ( q r )) → ( s ∨ ((¬ q ) ∧ (¬ s )))

Prédis la logique

La définition d'une formule en logique du premier ordre est relative à la signature de la théorie en question. Cette signature spécifie les symboles constants, les symboles de prédicat et les symboles de fonction de la théorie en question, ainsi que les arités des symboles de fonction et de prédicat.

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

  1. Toute variable est un terme.
  2. Tout symbole constant de la signature est un terme
  3. une expression de la forme f ( t 1 ,…, t n ), où f est un symbole de fonction n -ary, et t 1 ,…, t n sont des termes, est à nouveau un terme.

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

  1. Si t 1 et t 2 sont des termes alors t 1 = t 2 est une formule atomique
  2. Si R est un symbole de prédicat n -ary, et t 1 ,…, t n sont des termes, alors R ( t 1 ,…, t n ) est une formule atomique

Enfin, l'ensemble de formules est défini comme étant le plus petit ensemble contenant l'ensemble de formules atomiques tel que ce qui suit est vrai:

  1. est une formule quand est une formule
  2. et sont des formules quand et sont des formules;
  3. est une formule quand est une variable et est une formule;
  4. est une formule lorsque est une variable et est une formule ( peut également être définie comme une abréviation pour ).

Si une formule n'a pas d'occurrences de ou , pour une variable , alors elle est appelée sans quantificateur . Une formule existentielle est une formule commençant par une séquence de quantification existentielle suivie d'une formule sans quantificateur.

Formules atomiques et ouvertes

Une formule atomique est une formule qui ne contient pas de connecteurs logiques ni de quantificateurs , ou de manière équivalente une formule qui n'a pas de sous-formules strictes. La forme précise des formules atomiques dépend du système formel considéré; pour la logique propositionnelle , par exemple, les formules atomiques sont les variables propositionnelles . Pour la logique des prédicats , les atomes sont des symboles de prédicat avec leurs arguments, chaque argument étant un terme .

Selon une certaine terminologie, une formule ouverte est formée en combinant des formules atomiques en utilisant uniquement des connecteurs logiques, à l'exclusion des quantificateurs. Cela ne doit pas être confondu avec une formule qui n'est pas fermée.

Formules fermées

Une formule fermée , également formule ou phrase au sol , est une formule dans laquelle il n'y a pas d'occurrences libres d'une variable . Si A est une formule d'un langage du premier ordre dans lequel les variables v 1 , ..., v n ont occurrences libres, alors A précédée par v 1c n est une fermeture de A .

Propriétés applicables aux formules

  • Une formule A dans une langue est valide si elle est vraie pour chaque interprétation de .
  • Une formule A dans une langue est satisfiable si elle est vraie pour une interprétation de .
  • Une formule A du langage de l' arithmétique est décidable si elle représente un ensemble décidable , c'est-à-dire s'il existe une méthode efficace qui, étant donné une substitution des variables libres de A , dit que soit l'instance résultante de A est prouvable, soit sa négation est .

Utilisation de la terminologie

Dans les travaux antérieurs sur la logique mathématique (par exemple par Church ), les formules faisaient référence à toutes les chaînes de symboles et parmi ces chaînes, les formules bien formées étaient les chaînes qui suivaient les règles de formation des formules (correctes).

Plusieurs auteurs disent simplement formule. Les usages modernes (notamment dans le contexte de l'informatique avec des logiciels mathématiques tels que les vérificateurs de modèles , les prouveurs de théorèmes automatisés , les prouveurs de théorèmes interactifs ) tendent à ne retenir de la notion de formule que le concept algébrique et à laisser la question de la bonne formation , c'est -à- dire de la la représentation sous forme de chaîne concrète de formules (en utilisant tel ou tel symbole pour les connecteurs et les quantificateurs, en utilisant telle ou telle convention de parenthèse , en utilisant la notation polonaise ou infixe , etc.) comme un simple problème de notation.

Si l'expression formule bien formée est encore en usage, ces auteurs ne l'utilisent pas nécessairement par opposition à l'ancien sens de formule , qui n'est plus courant en logique mathématique.

L'expression «formules bien formées» (WFF) s'est également glissée dans la culture populaire. WFF fait partie d'un jeu de mots ésotérique utilisé au nom du jeu académique " WFF 'N PROOF : The Game of Modern Logic", par Layman Allen, développé alors qu'il était à la Yale Law School (il était plus tard professeur à l' Université de Michigan ). La suite de jeux est conçue pour enseigner les principes de la logique symbolique aux enfants (en notation polonaise ). Son nom est un écho de whiffenpoof , un mot absurde utilisé comme acclamation à l'Université de Yale rendu populaire dans The Whiffenpoof Song et The Whiffenpoofs .

Voir également

Remarques

Les références

Liens externes