[LOGI] Logique du premier ordre (4)

Langages du premier ordre (Relationnels)

Nouveaux connecteurs logiques

Partie specifique : On note la donnee de symboles dits specifiques

Ou nb d’arguments = Meta-variables et fonctions = symboles

Vocabulaire:

Si R est une relation d’arite verifiant est valide y est unique On dira alors que R est fonctionnelle

Notation: On ecrira alors au lieu de

Toute fonction peut etre vue comme une relation (syntaxiquement)

Construction inductive de

(Formules du premier ordre du langage )

Exemples: } (0, 0, f 2, f 2, f 1, rel 2)

Termes : (ok)

NB: polonais

Algo de verif de construction de termes de

Entree : ( : symbole)

Process :

Accept: ssi

Exemple

1 1 -1 -1 -1
1 2 1 0 -1

Formules

Atomes : sont des formules pour chaque d’arite sont des termes de alors est une formule atomique

Construction : [connections logiques de ] si formules de alors sont encore des formules de

Arret

Exemple(Ari) : En polonais

Statuts des variables

Ocurrence : apparition d’un symbole donne

et admet ??? n’admet pas

Ocurrences libres : Hors champ de quantification

[hors champ] [champ de quanditication de “x”]

En polonais:

Symbole de var quantifie : chaque occ dams le champ de quandification Symbole de var lie

Formule close : tous les symboles de variables qui admettent une occurrence sont entierement quantifies ()

Exemple:

Demonstration avec Regles du calcul des sequants des LK1 Autres regles LK1 (pas LK0): gestion des quantifs

Notation : signifie que x a occurences libres dans