Logique des prédicats

Non, par exemple dans la formule $\forall x, x=x$, il n'y a pas d'occurrence libre de $x$, pourtant $x$ apparaît dans la formule.

waliddz écrivait:

---

> si F est une formule atomique dépendant d'une certaine variable x,
> alors dans la formule $\forall x F $, x apparait libre dans F.

Euh ... peux-tu formuler ça plus clairement ?

Cette propriété est un axiome (et pour info, c'est même quasiment le seul en plus de la partie propositionnelle des maths et de la science)

Sa bonne formulation est d'ailleurs une implication et non pas une équivalence:

$$ A \Rightarrow (\forall xA) $$

car la réciproque nécessite que l'univers soit non vide (qui est admis par tradition, mais n'a rien de "logique" a priori).

Attention: c'est un axiome officiel seulement quand $A$ ne contient pas d’occurrence libre de $x$

Pour la suite utilise le zoom de ton navigateur.

[small]Sinon, c'est un peu HS, mais je te donne une "leçon" extérieure un peu "philosophico-technique" qui permet de se décontaminer des ambiguités concernant les variables liées, via l'introduction de "combinateurs" qui le rendent inutiles (autrement dit, toutes les maths pourraient être écrites sans var liées grace à eux, mais la tradition ne les a pas privilégiés. Cependant, ils sont "pédagogiquement" très efficaces ici).

1/ Tout lieur de variables peut être vu comme une simple fonction (ou simple opérateur), de sorte qu'il n'y a qu'un seul "lieur" originel, qui se note $\mapsto$ et s'utilise comme suit (exemples):

$$[\forall xA] := [\forall (x\mapsto A)]$$

$$ [\int_A f(x)dx] := [int(A, (x\mapsto f(x)))]$$

2/ Du coup, je ne vais qu'éliminer l'usage de $\mapsto$ et ça suffira à TOUS les éliminer.

3/ En amont du langage tu ajoutes les symboles $K,S$ (on peut faire mieux et plus "doux", mais je te communique un principe et s'il te plait, je changerai le jeu de combinateurs) et décrètes avant toute autre chose, une bonne fois pour toute que : $\forall x,y,z: $

3.1/ $(Kx)y = x$
3.2/ $Sxyz=(xz)(yz)$

4/ Soit maintenant deux suites de symboles u,v et une lettre x, pour laquelle tu voudrais écrire sans l'utiliser l'objet grammatical :

$$ x\mapsto (uv)$$

Supposons que tu sois parvenu à prouver que

$$(x\mapsto u)=u'$$

et que

$$(x\mapsto v)=v'$$

Sans que la lettre $x$ n'apparaissent dans $u',v'$.

Alors tu auras que $[x\mapsto (uv)] = S(u')(v')$

Il suffit (par récurrence) de réussir à écrire $x\mapsto a$ quand $a$ est un symbole primitif (or c'est $Ka$) et de réussir à écrire $x\mapsto x$ (or et c'est très inélégant mais peu important) : exercice prouve que $SKK = [x\mapsto x]$

La "leçon" s'arrête là.

Exemple: tu veux exprimer $\forall x\exists y: x$ est amoureux de $y$ sans utiliser de variable liées. Et bien tu écris, en abrégeant "x est amoureux de y" par "(Ax)y":

$$ \forall (S (K \exists) (A))$$

qui veut très exactement dire la même chose. [/small]

Je t'ai dit la nuance. La tradition est de supposer l'univers non vide ce que fait le livre. Mais non seulement

1/ envisager le vide n'est pas un mal

2/ le plus important : aucune preuve n'a besoin de l'équivalence en dehors d'admettre EXPLICITEMENT la non vacuité. Autrement dit tu peux toujours enlever le mauvais sens articificiel de TOUTE preuve même quand tu parles d'univers non vides (dans ce cas tu peux ne l'utiliser qu'une fois à la fin)

En restant au premier ordre, en calcul des séquents (classique)

Un contexte est un ensemble fini de variables qui contient les variables libres des formules du séquent. Le contexte est indiqué en indice du $\vdash$. Une règle structurale de déduction permet d'augmenter le contexte :
$$\frac{\Gamma\vdash_V \Delta}{\Gamma\vdash_{V\cup\{x\}}\Delta}\;.$$
Règles d'introdution du $\forall$ :
$$\frac{\Gamma, A[t/x]\vdash_{V} \Delta}{\Gamma, \forall x\ A \vdash_V \Delta}\qquad \frac{\Gamma \vdash_{V\cup\{x\}} \Delta, A}{\Gamma \vdash_V \Delta,\forall x\ A}\;.
$$
Règles d'introdution du $\exists$ :
$$\frac{\Gamma, A \vdash_{V\cup\{x\}} \Delta}{\Gamma, \exists x\ A \vdash_V \Delta}
\qquad
\frac{\Gamma\vdash_{V} \Delta, A[t/x]}{\Gamma\vdash_V \Delta, \exists x\ A }\;.$$
Implicite : dans les règles $\forall$ gauche et $\exists$ droite, les variables du terme $t$ (de même type que $x$) sont dans $V$ ; dans les règles $\forall$ droite et $\exists$ gauche, les variables libres des formules de $\Gamma$ et $\Delta$ sont dans $V$.

Soit $V$ l'ensemble des variables libres de $A$ (par exemple $V=\emptyset$ si $A$ est un énoncé, c.-à-d. une formule close).
1) À partir de l'axiome $A\vdash_V A$, si $x\not\in V$, on démontre $A\vdash_V\forall x\ A$ et $\forall x\ A\vdash_{V\cup\{x\}}A$, mais pas a priori $\forall x\ A\vdash_{V}A$ (on peut le faire si on dispose d'un terme de même type que $x$ dont les variables sont dans $V$).
2) De manière analogue pour $\exists$, ...

Tu penses à un seul type de variables ?

Je ne vois pas ce que la parenthèse a à voir avec ma question.

Le calcul des séquents (intuitionniste) avec contexte est correct et complet pour la sémantique dans les topos.
Pour le calcul classique avec contexte, c'est correct et complet pour la sémantique dans les topos booléens.

De mon téléphone c'est un peu pénible à taper mais je rappelle que l'idée que forall veut dire pour tout est une vue de l'esprit non nécessaire.

On peut ne travailler qu'avec des énoncés clos (c'est plus sain) et THE règle du jeu (enfin axiome) importante est (en abrégeant forall par Q):

(Qx)=> ([QxU]=>[QxV])

Autrement dit l'impression d'illégitimité de cette étrange règle gratuite passant R(x) à QxR(x) sous certaines conditions peut être prise au sérieux sans mépris des objecteurs trop sémantiques (il faut ménager les gilets jaunes) et prouvée (et même de plus tout bêtement évitée: elle est utilisée QUE parce qu'on économise l'encre en n'écrivant pas les forall de gauche).