Implication vs. conséquence logique

La logique (comprise comme étude du raisonnement comme un objet) gère deux sortes de choses:

-Un ensemble $E$ qu'on va appeler "ensemble des énoncés formels" (ce sont littéralement des suites de symboles).
-Des affirmations portant sur $E$, sur ses sous-parties et sur ses éléments.

1°) L'implication $\to$ est un symbole typographique. On a donc simplement, étant donné deux éléments $x,y\in E$, un troisième élément $x\to y \in E$ qui est une construction typographique.

2°) Une partie $\frak C$ (qu'on va appeler "relation de conséquence (*) ") de $\mathcal P (E) \times E$. Les éléments de $\frak C$ sont donc des couples $(S,x)$ où $x$ est un énoncé formel (i.e. un élément de $E$ et $S$ un ensemble d'énoncés formels.

Lorsque $(S,x)$ appartient à $\frak C$, on va dire que $x$ est conséquence de $S$ au sens de $\frak C$.

Les logiciens utilisent essentiellement comme types de relations de conséquence:

-la démontrabilité: (la notation la plus fréquente est $S \vdash x$ au lieu de $(S,x) \in \mathfrak C$): $x$ est obtenu à partir d'une suite de manipulations syntaxiques avec au départ des éléments de $S$ appelés axiomes ou hypothèses (dans la démonstration correspondante seulement: aucun énoncé logique n'est intrinsèquement un axiome).
- la validité au sens de la théorie des modèles: la notation la plus fréquente est $S\vDash x$ au lieu de $(S,x) \in \mathfrak C$.
Ce qui veut dire "si pour une interpétation quelconque tous les éléments de $S$ sont vrais alors $x$ est vrai aussi pour cette interprétation" (la notion d'interprétation doit être définie séparément sans quoi un énoncé formel ne veut rien dire et en particulier n'est pas susceptible d'être vrai ou faux).

Contrairement à ce qui se passe en 2°), j'insiste sur le fait que dans 1 il n'y a aucune référence à une quelconque vérité ou prouvabilité de $y$ et de $x$ quand on écrit $x \to y$.


#########

(*) Dans les situations habituelles une relation de conséquence $\mathfrak C$ va vérifier les propriétés suivantes
(je vais désormais utiliser la notation $T \Vdash u$ à la place de $(T,u) \in \mathfrak C$, $a_1,...,a_m \Vdash b$ à la place de $\{a_1,...,a_m\} \Vdash b$ et $S,p_1,...,p_n \Vdash q$ à la place de $S \cup \{p_1,...,p_n\} \Vdash p$.

i) Pour tout $x\in A$, $A \Vdash x$ (lapalissade: si tous les éléments de $A$ sont vrais,alors tous les éléments de $A$ sont vrais ...)

ii) Pour tous $A,B \subseteq E$ et tout $x\in E$, si $A \Vdash x$ et $A\subseteq B$ alors $B \Vdash x$ (intuitivement: si $A$ entraîne $x$ et tous les énoncés de $A$ appartiennent à $B$, alors a fortiori $B \Vdash x$).

iii) Pour tous $x\in E$, $A,B\subseteq E$, si pour tout $y$ dans $B$, $A\Vdash y$ et si $B \Vdash x$ alors $A \Vdash x$ (intuitivement: si $x$ est conséquence d'énoncés tous eux-mêmes conséquences de $A$, alors $x$ est conséquence de $A$)

iv) Si $A$ est une partie de $E$ et $x\in E$, $A \Vdash x$ si et seulement si il existe une partie finie $\{a_1,...,a_n\}$ de $A$ telle que $a_1,...,a_n \Vdash x$.
Cette propriété est évidente lorsque $\Vdash$ est la démontrabilité (une démonstration n'étant qu'une suite finie de symboles obéissant à des règles syntaxiques, elle ne peut faire intervenir qu'un nombre fini d'axiomes).
De manière surprenante elle est également vraie pour la validité de la théorie des modèles: c'est l'objet des résultats appelés théorèmes de compacité.

-Lorsque le symbole $\to$ est utilisé:

v) (modus ponens) Pour tous $A\subseteq E$, $x,y \in E$, si $A \Vdash x$ et $A \Vdash x \to y$ alors $A \Vdash y$.
vi) (règle de déduction) Pour tous $A \subseteq E$ $x,y\in E$, si $A,x \Vdash y$ alors $A \Vdash x \to y$ (intuitivement: si $y$ est conséquence de l'ensemble obtenu en ajoutant $x$ à $A$, alors le fait que "$x$ implique $y$" est conséquence de $A$ seul. C'est exactement ce qu'on fait lorsqu'on dit "qu'on suppose $x$ pour en déduire $y$" sous les hypothèses $A$).

-Lorsque le symbole $\wedge$ est utilisé:

vii) Pour tous $A\subseteq E$, $x,y \in E$, $A \Vdash x \wedge y$ si et seulement si $A \Vdash x$ et $A \Vdash y$

exo: deviner le cahier des charges satisfait par le symbole "ou" $\vee$.

Non, pas du tout, c'est bien plus simple. C'est juste que tu t'es trompé quand tu as écrit:

et je crois avoir compris ce que signifie l'implication : sois deux formules .... Je l'interprète comme suis : pour toutes les possibilités des symboles

L'implication, au même titre que "et" ; "ou"; $+$; $\times $ ; etc est une "banale" opération. Elle n'a pas de statut spécial.

Et oui, tu peux considérer que sa définition est donnée pour tout $a,b$ par $(a\to b):= ((non(a))\vee b)$, en attendant d'arriver à étudier plus précisément la logique, ça ne te trompera jamais.

Ce sont les deux autres symboles $\vdash$ et $\models$ qui sont un peu plus "savants".

Si tu précises ton niveau, je te donnerai une explication adaptée, car plusieurs sont possibles, avec des exemples différents. Par exemple, je veux savoir avant de taper si je peux te parler d'anneaux.