Logique du 1er ordre (théories logiqus)

[Grealishh]

Bonjour,
J'ai une question sur la logique du premier ordre, je ne comprends pas trop comment dois je y procéder.
Si quelqu'un peut m'aider s'il vous plaît, je vous remercie !

Voici l'énoncé et la question :

On se place dans cet exercice sur la signature LG
def = (∅, {E(2)
, =(2)}) et on commence par considérer l’en-
semble AG d’axiomes suivant :
(irréflexivité de E) ∀x. ¬E(x, x)
(symétrie de E) ∀x∀y. E(x, y) ⇒ E(y, x)
(réflexivité de =) ∀x. x = x
(symétrie de =) ∀x∀y. x = y ⇒ y = x
(transitivité de =) ∀x∀y∀z. (x = y ∧ y = z) ⇒ x = z
(E-congruence) ∀x1∀x2∀y1∀y2. (x1 = y1 ∧ x2 = y2) ⇒ (E(x1, x2) ⇒ E(y1, y2))
Les deux premiers axiomes imposent que l’interprétation du symbole E sera bien l’ensemble des arêtes d’un
graphe non-orienté (par symétrie) simple (par irréflexivité). On ajoute ensuite à AG une infinité d’axiomes
pour interdire les cycles de longueur impaire : pour tout n ∈ N avec n > 0, l’axiome suivant est ajouté :
¬∃x0∃y0∃x1∃y1 · · · ∃x2n∃y2n.
∧
0≤i≤2n
(xi = yi ∧ E(yi
, x(i+1) mod 2n))
(C2n+1 exclu)
par exemple, pour le cas n = 1, cela donne l’axiome
(C3 exclu) ¬∃x0∃y0∃x1∃y1∃x2∃y2. x0 = y0 ∧ E(y0, x1) ∧ x1 = y1 ∧ E(y1, x2) ∧ x2 = y2 ∧ E(y2, x0)
On note AB cette nouvelle axiomatisation ; Th(AB) est la théorie des graphes non-orientés sans cycles de lon-
gueur impaire.

**Montrer que la formule suivante appartient à Th(AB) :
"∀x∀y∀z.((E(x, y) ∧ E(y, z))⇒ ¬E(x, z)) "

[GaBuZoMeu]

Bonjour,

Je trouve que cet exercice ne porte pas tellement sur la logique du premier ordre. Cette formalisation ne fait qu'alourdir le problème.
Commence par voir en termes de graphes ce que veut dire la formule dont on te demande de montrer que c'est un théorème.

[Grealishh]

Bonjour,
Merci pour votre réponse,
Enfaite, on nous demande de montrer que cette formule appartient à la théorie de l'axiomatisation donnée.en terme de graphe la formule correspond à dire dans un graphe si on a une arête entre x et y et une arête entre y et z alors on n'a pas d'arête entre x et z (anti-transitivité). Mais pour montrer que cela appartient à la théorie de l'axiomatisation donnée, je ne sais pas comment procéder ...

[GaBuZoMeu]

Tu ne vois pas dans les axiomes quelque chose qui empêche qu'on ait une arête entre x et y, une entre y et z et une entre x et z ?

[tournesol]

Meilleurs voeux GaBuZoMeu

[Grealishh]

Merci pour la réponse,
Je ne comprends pas vraiment ce que tu veux dire, on a la transitivité de l'égalité et pas celle de E, donc je ne vois pas comment montrer cella si vous pouvez me détailler votre idée s'il vous plaît...

[tournesol]

Je me suis planté . Meilleurs voeux à toi aussi .

[GaBuZoMeu]

Meilleurs voeux Tournesol.

On a un graphe simple non orienté qui n'a pas de cycle de longueur impaire.
Grealishh, tu ne vois vraiment pas pourquoi, si on a une arête en x et y et une arête entre y et z, il ne peut pas y avoir d'arête entre x et z ? Fais un dessin, tu verras peut-être ?