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
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
autrement dit, ça ne veut rien dire en tant que phrase si courte. Ca veut dire "à la condition de faire attention" :-D
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 !
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.
Il s'agit du livre de John Bell : "Set Theory - Boolean valued models and independence proofs".
Merci pour la référence de la page 392
$$ (\forall x\exists y: x\neq y)\to (\exists y: y\neq y)$$
:-D )
Voici encore une précision issue du livre "Fundamentals of mathematical logic" de Peter G. Hinman, page 107 :[/large]