Axiomes de la logique intuitionniste
Bonjour à tous,
Dans un texte qui parle d'algèbres de Heyting on donne au passage les axiomes et règles de la LI (dans cette version-là il y en a une tétrachiée).
Parmi les axiomes il y en a un qui dit, je cite :
"$\forall x \varphi(x) \to \varphi(y)$ ($x$ free in $\varphi$ and $y$ free for $x$ in $\varphi$)".
Qu'est-ce que ça peut bien vouloir dire que $y$ est libre pour $x$ dans la formule $\varphi$ ?
Merci d'avance
Martial
Dans un texte qui parle d'algèbres de Heyting on donne au passage les axiomes et règles de la LI (dans cette version-là il y en a une tétrachiée).
Parmi les axiomes il y en a un qui dit, je cite :
"$\forall x \varphi(x) \to \varphi(y)$ ($x$ free in $\varphi$ and $y$ free for $x$ in $\varphi$)".
Qu'est-ce que ça peut bien vouloir dire que $y$ est libre pour $x$ dans la formule $\varphi$ ?
Merci d'avance
Martial
Réponses
-
Ce que tu imagines, à savoir que $y$ a été mis à la plce de toutes les occurrences libres et seulement elles de $x$ et que en plus, il n'apparait en occurrences liées qui vont capturer indûment la généralité exprimée :-D :-D :-D
autrement dit, ça ne veut rien dire en tant que phrase si courte. Ca veut dire "à la condition de faire attention" :-DAide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@Martial : je ne pense pas que ton interrogation porte sur un mécanisme substitutionnel propre à la LI. Voici deux extraits, l'un glané sur le web, l'autre extrait du livre excellentissime Introduction à la logique ; théorie de la démonstration de R. David, K. Nour et C. Raffalli, seconde édition de 2003 :Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
-
Lire également ceci.Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
-
Merci à tous 2, je vais potasser ça demain.
-
Je t'invite également à examiner les axiomes des quantificateurs, notamment le 2) c), page 230 du livre Logique mathématique, tome 1 de R. Cori et D. Lascar. Je pense que tu dois l'avoir.Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
-
@Thierry : tu as entièrement raison, je viens de vérifier, la 1ère définition que tu donnes est exactement la restriction imposée par Cori-Lascar. Je m'en doutais un peu, mais je voulais vérifier.
Et tu as également raison, ces restrictions ne sont pas propres à la LI.
Selon l'ouvrage que je suis en train de consulter, les axiomes et règles sont communs à la LI et à la LC, la seule différence étant qu'à la LI il faut rajouter la règle $\dfrac{\neg \neg \varphi}{\varphi}$ pour obtenir LC.
Tout ceci va bientôt figurer dans mon chap 20.
Grand merci ! -
@Martial : bonjour. J'espère que tu vas bien.Selon l'ouvrage que je suis en train de consulter (...)
De quel ouvrage parles-tu, s'il te plait ?
Il y a aussi le livre La logique, pas à pas, de Jacques Duparc, page 392, concernant la capture des variables.Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême). -
A l'occasion je vais me pencher là-dessus sérieusement, j'avoue que j'ai toujours eu du mal avec ces histoires de captures de variables. Je sais bien qu'il faut le faire un peu exprès pour tomber dans un piège, mais quand même...
-
Pas vraiment (je ne me sens pas complotiste ou préméditatif en écrivant:
$$ (\forall x\exists y: x\neq y)\to (\exists y: y\neq y)$$
:-D )Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@Christophe : oui, c'est précisément à ce contre-exemple que je pensais.
-
[large]Bonsoir Martial
Voici encore une précision issue du livre "Fundamentals of mathematical logic" de Peter G. Hinman, page 107 :[/large]Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême). -
Merci, Thierry, pour ces précisions.
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.1K Toutes les catégories
- 7 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 52 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 62 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 312 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 772 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 3
3 Invités