Le "et" intuitionniste
Bonjour,
je voulais avoir un point de vue assez global sur la logique et du coup j'ai voulu prendre un point de vue souvent raconté par Christophe sur le forum.
Désolé pour le post fleuve ! Il y a deux questions, à la fin.
Voici ce que j'ai fait :
Je pars d'un ensemble $V$ qui contient deux éléments différents $\top$ et $\bot$. Je considère le magma libre (c'est bien ça :-D ?) $F(V)$ sur $V$, c'est-à-dire que je considère l'ensemble des mots dans l'alphabet $V \cup \{ (,)\} \cup \{\rightarrow\}$ qui sont des expressions bien parenthésées, etc., enfin j'espère que vous voyez ce que je veux dire.
Une partie $A$ de $F(V)$ est dite stable par modus ponens si $\forall a \in F(V),\ \forall b \in F(V), \quad (a \in A \mbox{ et } a\rightarrow b \in A) \Rightarrow (b \in A)$.
Pour toute partie $A$ de $F(V)$, on note $\overline{A}$ l'intersection de toutes les sur-parties de $A$ de $F(V)$ qui sont stables par modus ponens et qui contiennent $\top$.
Je pose maintenant :
- $C_\top := \{a \rightarrow \top \ \vert \ a \in F(V)\}$ ;
- $C_\bot := \{\bot \rightarrow a \ \vert \ a \in F(V)\}$ ;
- $C_{ajout} := \{a \rightarrow (b \rightarrow a) \ \vert \ a,b \in F(V)\}$ ;
- $C_{permut} := \{(a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a\rightarrow c))\ \vert \ a,b,c \in F(V)\}$ ;
- $C_{oubli} := \{(a\rightarrow (a \rightarrow b))\rightarrow(a\rightarrow b)\ \vert \ a,b \in F(V)\}$ ;
- $C_{concl-hyp} := \{a\rightarrow a \ \vert \ a\in F(V)\}$ ;
- $C_{lem} := \{(q\rightarrow r)\rightarrow((p \rightarrow q)\rightarrow(p\rightarrow r))\ \vert \ p,q,r \in F(V)\}$ ;
- $C_{abs} := \{((p\rightarrow \bot)\rightarrow \bot)\rightarrow p \ \vert \ p \in F(V)\}$.
On appelle démonstration de longueur $n$ une suite finie (indexée par $\{1,...,n\}$) dont les termes sont des couples $(p,\{i_1,...,i_{n_p}\})$ où $p \in F(V)$, et $i_1,...,i_{n_p}$ sont des indices de termes de rang strictement inférieur.
Soit $D = ((p_1,h_1),(p_2,h_2),...,(p_n,h_n))$ une démonstration de longueur $n$. Soit $i \in \{1,...,n\}$. Si $h_i$ est vide, on dit que l'hypothèse faite au rang $i$ est $p_i$. Si $h_i$ est non vide et $h_i = \{i_1,...,i_{n_i}\}$, on dit que l'hypothèse faite au rang $i$ est $p_{i_1} \rightarrow(p_{i_2} \rightarrow (... \rightarrow (p_{i_{n-1}} \rightarrow p_i)...))$. On dit que $p_n$ est la conclusion de $D$.
Bon, si je ne me suis pas trompé, on a, pour toute $A \subset F(V)$, que $\overline{A}$ est l'ensemble des conclusions de démonstrations dont toutes les hypothèses sont dans $A$.
On appelle logique une réunion de trucs dans la liste des $C$ définis ci-dessus. Par exemple, on note $C_{int}$ la réunion de tous les $C$ sauf le dernier, et on note $C_{class}$ la réunion de tous les $C$.
Si $H$ est un ensemble possédant deux éléments $\top$ et $\bot$ et muni d'une opération binaire $\rightarrow$, alors toute application $\phi : V \rightarrow H$ qui envoie $\top$ sur $\top$, $\bot$ sur $\bot$ se prolonge de manière unique en une application $\overline{\phi} : F(V) \rightarrow H$ qui envoie toujours $\top$ sur $\top$, $\bot$ sur $\bot$, et qui, de plus est un morphisme pour $\rightarrow$.
On dit que la sémantique des algèbres de Heyting est complète pour la logique intuitionniste si pour toute partie $A \subset F(V)$ et tout $p \in F(V)$, $p \in \overline{A\cup C_{int}}$ si et seulement si (pour toute algèbre de Heyting $H$ et toute application $\psi : F(V) \rightarrow H$ envoyant $\top$ sur $\top$, $\bot$ sur $\bot$ et étant un morphisme pour $\rightarrow$, $\psi(A \cup C_{int}) = \{\top\} \Rightarrow \psi(p) = \top$).
On dit enfin que la sémantique des algèbres de Boole est complète pour la logique classique si la même chose que précédemment est vraie si on remplace algèbre de Heyting par algèbre de Boole, et si on remplace $C_{int}$ par $C_{class}$.
J'arrive à démontrer que la sémantique des algèbres de Boole est complète pour la logique classique, mais pas que la sémantique des algèbres de Heyting est complète pour la logique intuitionniste.
1) Est-ce vrai ?
2) Ma stratégie est de quotienter $F(V)$ par la relation $\leftrightarrow_A$ telle qu'on a $p\leftrightarrow_A q$ si $p\rightarrow q$ et $q \rightarrow p$ sont des éléments de $\overline{A\cup C_{int}}$.
J'arrive à démontrer que c'est une relation d'équivalence, et que $\rightarrow$ est compatible à gauche et à droite, et donc que cela induit une $\rightarrow$ sur le quotient. Je voulais alors construire un ordre sur $F(V)/\leftrightarrow_A$ qui en fasse une algèbre de Heyting et tel que $\rightarrow$ soit le $\rightarrow$ de cette algèbre de Heyting. Je me suis dit que si j'arrivais à fabriquer une opération binaire $\cap$ qui soit commutative, associative, et idempotente, je pourrais fabriquer un ordre en posant $a \leq b$ si $a = a\cap b$. Il fallait donc trouver un $\cap$. J'ai tenté de poser $p\cap q := (p \rightarrow(q \rightarrow \bot))\rightarrow \bot$, qui est bien commutative, mais qui n'est pas idempotente, a priori, car $p \cap p = (p \rightarrow (p\rightarrow \bot))\rightarrow \bot = (p\rightarrow \bot) \rightarrow \bot$ qui est différent de $p$ en général...
je voulais avoir un point de vue assez global sur la logique et du coup j'ai voulu prendre un point de vue souvent raconté par Christophe sur le forum.
Désolé pour le post fleuve ! Il y a deux questions, à la fin.
Voici ce que j'ai fait :
Je pars d'un ensemble $V$ qui contient deux éléments différents $\top$ et $\bot$. Je considère le magma libre (c'est bien ça :-D ?) $F(V)$ sur $V$, c'est-à-dire que je considère l'ensemble des mots dans l'alphabet $V \cup \{ (,)\} \cup \{\rightarrow\}$ qui sont des expressions bien parenthésées, etc., enfin j'espère que vous voyez ce que je veux dire.
Une partie $A$ de $F(V)$ est dite stable par modus ponens si $\forall a \in F(V),\ \forall b \in F(V), \quad (a \in A \mbox{ et } a\rightarrow b \in A) \Rightarrow (b \in A)$.
Pour toute partie $A$ de $F(V)$, on note $\overline{A}$ l'intersection de toutes les sur-parties de $A$ de $F(V)$ qui sont stables par modus ponens et qui contiennent $\top$.
Je pose maintenant :
- $C_\top := \{a \rightarrow \top \ \vert \ a \in F(V)\}$ ;
- $C_\bot := \{\bot \rightarrow a \ \vert \ a \in F(V)\}$ ;
- $C_{ajout} := \{a \rightarrow (b \rightarrow a) \ \vert \ a,b \in F(V)\}$ ;
- $C_{permut} := \{(a \rightarrow (b \rightarrow c)) \rightarrow (b \rightarrow (a\rightarrow c))\ \vert \ a,b,c \in F(V)\}$ ;
- $C_{oubli} := \{(a\rightarrow (a \rightarrow b))\rightarrow(a\rightarrow b)\ \vert \ a,b \in F(V)\}$ ;
- $C_{concl-hyp} := \{a\rightarrow a \ \vert \ a\in F(V)\}$ ;
- $C_{lem} := \{(q\rightarrow r)\rightarrow((p \rightarrow q)\rightarrow(p\rightarrow r))\ \vert \ p,q,r \in F(V)\}$ ;
- $C_{abs} := \{((p\rightarrow \bot)\rightarrow \bot)\rightarrow p \ \vert \ p \in F(V)\}$.
On appelle démonstration de longueur $n$ une suite finie (indexée par $\{1,...,n\}$) dont les termes sont des couples $(p,\{i_1,...,i_{n_p}\})$ où $p \in F(V)$, et $i_1,...,i_{n_p}$ sont des indices de termes de rang strictement inférieur.
Soit $D = ((p_1,h_1),(p_2,h_2),...,(p_n,h_n))$ une démonstration de longueur $n$. Soit $i \in \{1,...,n\}$. Si $h_i$ est vide, on dit que l'hypothèse faite au rang $i$ est $p_i$. Si $h_i$ est non vide et $h_i = \{i_1,...,i_{n_i}\}$, on dit que l'hypothèse faite au rang $i$ est $p_{i_1} \rightarrow(p_{i_2} \rightarrow (... \rightarrow (p_{i_{n-1}} \rightarrow p_i)...))$. On dit que $p_n$ est la conclusion de $D$.
Bon, si je ne me suis pas trompé, on a, pour toute $A \subset F(V)$, que $\overline{A}$ est l'ensemble des conclusions de démonstrations dont toutes les hypothèses sont dans $A$.
On appelle logique une réunion de trucs dans la liste des $C$ définis ci-dessus. Par exemple, on note $C_{int}$ la réunion de tous les $C$ sauf le dernier, et on note $C_{class}$ la réunion de tous les $C$.
Si $H$ est un ensemble possédant deux éléments $\top$ et $\bot$ et muni d'une opération binaire $\rightarrow$, alors toute application $\phi : V \rightarrow H$ qui envoie $\top$ sur $\top$, $\bot$ sur $\bot$ se prolonge de manière unique en une application $\overline{\phi} : F(V) \rightarrow H$ qui envoie toujours $\top$ sur $\top$, $\bot$ sur $\bot$, et qui, de plus est un morphisme pour $\rightarrow$.
On dit que la sémantique des algèbres de Heyting est complète pour la logique intuitionniste si pour toute partie $A \subset F(V)$ et tout $p \in F(V)$, $p \in \overline{A\cup C_{int}}$ si et seulement si (pour toute algèbre de Heyting $H$ et toute application $\psi : F(V) \rightarrow H$ envoyant $\top$ sur $\top$, $\bot$ sur $\bot$ et étant un morphisme pour $\rightarrow$, $\psi(A \cup C_{int}) = \{\top\} \Rightarrow \psi(p) = \top$).
On dit enfin que la sémantique des algèbres de Boole est complète pour la logique classique si la même chose que précédemment est vraie si on remplace algèbre de Heyting par algèbre de Boole, et si on remplace $C_{int}$ par $C_{class}$.
J'arrive à démontrer que la sémantique des algèbres de Boole est complète pour la logique classique, mais pas que la sémantique des algèbres de Heyting est complète pour la logique intuitionniste.
1) Est-ce vrai ?
2) Ma stratégie est de quotienter $F(V)$ par la relation $\leftrightarrow_A$ telle qu'on a $p\leftrightarrow_A q$ si $p\rightarrow q$ et $q \rightarrow p$ sont des éléments de $\overline{A\cup C_{int}}$.
J'arrive à démontrer que c'est une relation d'équivalence, et que $\rightarrow$ est compatible à gauche et à droite, et donc que cela induit une $\rightarrow$ sur le quotient. Je voulais alors construire un ordre sur $F(V)/\leftrightarrow_A$ qui en fasse une algèbre de Heyting et tel que $\rightarrow$ soit le $\rightarrow$ de cette algèbre de Heyting. Je me suis dit que si j'arrivais à fabriquer une opération binaire $\cap$ qui soit commutative, associative, et idempotente, je pourrais fabriquer un ordre en posant $a \leq b$ si $a = a\cap b$. Il fallait donc trouver un $\cap$. J'ai tenté de poser $p\cap q := (p \rightarrow(q \rightarrow \bot))\rightarrow \bot$, qui est bien commutative, mais qui n'est pas idempotente, a priori, car $p \cap p = (p \rightarrow (p\rightarrow \bot))\rightarrow \bot = (p\rightarrow \bot) \rightarrow \bot$ qui est différent de $p$ en général...
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
2) Pourquoi ne pas dire que $a\leq b$ si et seulement si $(a\to b) \leftrightarrow_A \top$ ? En effet on veut que $a\leq b$ si et seulement si $a\land\top \leq b$ si et seulement si $\top \leq a\to b$ ($\to$ est adjointe à droite de $\land$, c'est sa définition), si et seulement si $\top = a\to b$ (puisque $\top$ est le maximum de l'algèbre de Heyting en question).
A priori, si tu l'as bien fait, tes règles permettent de démontrer que c'est un préordre sur $F(V)$ compatible avec le reste, de relation d'équivalence associée telle qu'il induit un ordre sur $F(V)/\leftrightarrow_A$
Après je pense que le problème de Georges Abitbol est ici de prouver justement que c'est une algèbre de Heyting (cf. sa question 2))
Le "et" n'est définissable qu'au second ordre: A et B est une abréviation de pour tout X si si A alors si B alors X alors X. Peut être cette définition aidera t elle GA?
Je ne connais pas le mot "subdirectductible", c'est la première fois sue je le vois. Je "devine un peu" ce que tu entends par la mais si tu as une définition je serais ravi il est stylé ce mot lool
Merci d'avance. Bon de toute façon ce n'est que dur un PC que je pourrai éventuellement réagir plus sérieusement pardon d'avance si je n'ai pas été très "non HS"
Je pense que Georges a maintenant une idée de l'ordre à mettre sur $F(V)/\leftrightarrow_A$ ;-)
"subdirectement irréductible" est une notion en algèbre universelle: un produit subdirect des $(A_i)_{i\in I}$ est une algèbre $A$ munie d'un morphisme injectif $f:A\to \displaystyle\prod_{i\in I}A_i$ tel que pour tout $i$, $\pi_i\circ f$ soit surjectif. Une algèbre est dite subdirectement irréductible si elle ne peut pas s'écrire comme un produit subdirect non trivial (i.e. $|I| >1$ et pour tout $i$, $|A_i| > 1$). Il est facile de voir que ça revient à une condition sur les congruences de $A$. Un théorème classique d'algèbre universelle affirme que toute algèbre s'écrit comme un produit subdirect d'algèbres subdirectement irréductibles.
Dans le cas des algèbres de Boole, la seule algèbre de Boole subdirectement irréductible non triviale est $\{0,1\}$. Donc si on considère la construction de Georges Abitbol pour la logique classique on obtient une représentation $f:\mathfrak{B}_T \to \{0,1\}^I$, où $\mathfrak{B}_T$ est l'algèbre de Boole des propositions modulo l'équivalence (classique). Si $p$ est une formule qui n'est pas prouvable, alors $f(p) \neq (1)_{i\in I}$ par injectivité de $f$, et donc il existe $i$ tel que $\pi_i\circ f (p) =0$, de sorte que $\pi_i\circ f$ est une évaluation qui donne "faux" à $p$: ce qui n'est pas prouvable n'est pas universellement valide. Là où ça bugge pour les algèbres de Heyting et la logique intuitionniste c'est qu'il y a des algèbres de Heyting subdirectement irréductibles non réduites à $\{0,1\}$ (et pour savoir pourquoi c'est vrai il suffit de voir que le théorème que j'ai énoncé implique que la variété des algèbres de Boole est engendrée par $\{0,1\}$, et que la variété des algèbres de Heyting n'est pas égale à cette dernière; or elle est engendrée par ses membres subdirectement irréductibles)
Par contre, je ne sais pas si, muni de cet ordre, $F(V)/\leftrightarrow_A$ est une algèbre de Heyting dont le $\rightarrow$ est celui que l'on a déjà...
Bien sûr, un élément $c$ du quotient n'est digne d'être appelé $a\cap b$ que si $\forall x, \ c \rightarrow x = a \rightarrow (b \rightarrow x))$ dans le quotient, mais pourquoi y en aurait-il déjà un ?
Je pensais qu'il y avait une application binaire $\wedge : F(V)^2 \rightarrow F(V)$ "définie simplement" qui passerait au quotient et donnerait l'inf dans le quotient, mais Christophe, tu as l'air de dire que ça n'existe pas ?
Si ça, ça ne marche pas, je doute que quoi que ce soit marche (mais je t'avoue que je n'ai pas du tout vérifié - et il y a de grandes chances que ça ne marche pas puisqu'intuitionnistement ce que j'ai écrit revient à $\neg\neg (a\land b)$, ce qui a peu de chances d'être équivalent à $a\land b$).
Mais à tous les coups christophe me surprendra en me montrant qu'il y a une meilleure méthode de faire :-D (mais comme tu dis, il a l'air de dire que non)
Tout à l'heure, je me suis dit que mon quotient s'injecte peut-être dans un treillis libre engendré par lui, et que là, ça a une chance de marcher (c'est ce que la remarque de Christophe "possible qu'au second ordre" m'inspire).
- pour le sport ;
- en vue d'un exposé plus pédagogique de la notion de démonstration dans des petites classes (en L1, par exemple !) : je pense que ça vaudrait le coup de présenter ça comme je le fais dans mon premier post ;
- je suis un peu allergique aux présentations genre séquents, car j'ai souvent du mal à discerner les "niveaux" de lecture (par exemple, j'ai longtemps pensé que $\vdash$ était un nouveau symbole à ajouter dans le langage, et donc qu'un truc du style $A \vdash p$ pouvait être un prédicat, au même titre que $p$, ce qu'il n'est pas s j'ai bien compris), et je peine à trouver des références qui approchent tout ça du point de vue que j'ai choisi ci-dessus, donc je dois un peu improviser (en m'inspirant très fort de ce que tout ce que j'ai pu lire, bien entendu). Le fait de ne partir que de $\rightarrow$ me semble bien pour faire émerger "naturellement" tout le reste.
PS : Je pensais d'ailleurs que le "et" émergerait naturellement, et pour l'instant, c'est encore sous l'eau !
Mais d'ailleurs il me semble qu'une des caractéristiques voulues de la logique intuitionniste est que les connecteurs ne soient pas interdéfinissables, contrairement à la logique classique. Ce que tu essaies de faire est peut-être donc impossible par dessein.
Et en effet, $A\vdash p$ n'est pas au même niveau que $p$ (dans toutes les constructions que j'ai vues). Mais tu peux voir $\vdash$ comme essentiellement une relation d'ordre/préordre, c'est le choix que fait Alain Prouté dans son cours de logique catégorique par exemple. Le faire comme ça montre en quoi la logique dite structurelle est... structurelle
J'avais aussi une question terminologique : Christophe avait dit qu'à d'autres réunions de $C$ comme je les ai définies plus haut, on avait les logiques minimale, linéaire, et affine. Je n'arrive plus à retrouver sur le forum le post où il disait qui était quoi. Max, tu sais ? Ou Christophe, si tu passes par là ?
Non moi je ne connais pas les logiques minimales et linéaire. Pour autant, ça me paraîtrait bizarre que la logique linéaire puisse être définie avec seulement des $\to$ puisqu'elle a tout plein de connecteurs "bizarres" (deux "et", deux "ou", une exponentiation, ...) Je pense que quand Christophe dit ça, il s'autorise à quantifier sur les formules (comme ce qu'il a donné avant, $\forall x, (a\to (b\to x))\to x$); et alors c'est possible que ça marche.
Je reviendrai sur le reste d'un PC. J'étais débordé ces derniers jours.
En effet, tu définis la complétude avec (je caricature, ce n'est pas important): << pour tout P qui n'est pas théorème de blabla, il existe une algèbre de Heyting qui blabla (et algèbre de Boole pour la logique classique)>>
On ne peut rêver meilleur pari :-D avec pareille définition de la complétude:
l'algèbre de Heyting des énoncés avec $\leq$ défini comme étant l'implication intuitionnistiquement prouvable SUFFIT à t'assurer la Georges-complétude pour la LI et l'algèbre de Boole des énoncés avec $\leq$ défini comme étant l'implication classiquement prouvable SUFFIT à t'assurer la Georges-complétude pour la LC.
(Evidemment, il faut juste s'assurer qu'on n'a pas oublié d'axiomes, mais c'est routinier)
En fait, je pense que maxtimax n'a pas lu en détail et donc a anticipé dans sa réponse en supposant que tu avais accédé à la bonne notion de complétude. D'où ses réponses typiques.
Pour ma part, je vais te faire un aveu: je ne sais pas s'il y a une définition mathématique du mot "sémantique". Chacun la définit un peu comme il veut et appelle "théorème de complétude" un théorème qui lui semble "mériter légitimement cette appelation". L'exemple historique est celui de la logique classique où (propositionnellement) seule les théories complètes ont le droit de s'appeler "modèles" et donc, la complétude s'énonce par "toute théorie est incluse dans au moins une théorie complète", autrement dit, un genre de "Zorn-light" (ou se prouve si tout est fini).
En réalité c'est juste "tout idéal est inclus dans un idéal maximal. Les anneaux de Boole ont ceci de particulier que $A/P$ est toujours (iso à ) $F_2$ quand l'idéal $P$ est premier, ce qui a rendu historiquement marquant les théorèmes de complétude pour la LC, mais c'est en fait relativement "truismatique". (On veut une sorte d'intégrité et quand c'est associé à du Boole, on peut prouver qu'il n'y a plus que deux éléments)
Pour la LI (c'est GBZM qui me l'a appris, sur ce forum même, il y a quelques années), des candidats forts sympathiques pour la complétude sont les topologies munies de $\subseteq $ comme ordre. Par exemple, tu peux prouver que ton système LI défini par toi-même au premier post est "collection des topologies"-complet. (Tu as aussi les modèles de Krypke, mais c'est moin joussif)
Max connait tellement de choses qu'il a largement anticipé dans sa réponse, sur des choses semble-t-il savantes (il me démentira si je me trompe) dont j'essaie de te dire comment elles se situent par rapport aux considérations ci-dessus. J'ai écrit: << je vais te faire un aveu: je ne sais pas s'il y a une définition mathématique du mot "sémantique">>
Je pense que Max a tout simplement connaissance de réflexions et recherches qui contredisent mon aveu, c'est à dire qui tentent (ont réussi ou pas, je ne sais pas) de donner une sorte de définition automatique définitive à ce que veut dire EN GENERAL <<X est une sémantique de la logique/syntaxe Y>>. Pour l'instant je ne peux pas commenter car je suis ignorant sur les avancées de ça. Attention: je ne parle pas des posts où il t'aide pour ton "et".
J'ai crée une définition générale pour ce qu'est une logique. C'est un triplet $L:=(P, \to , \leq, 1)$ où $P$ est un ensemble appelé "espace de phrases", $\to$ va de $P^2$ dans $P$ est croissante à droite et décroissante à gauche et $1\in P$ est neutre à gauche ie $\forall x: [(1\to x)=x]$. On demande en outre que $\forall x,y: (x\leq y\iff (1\leq (x\to y)))$ et $\forall x,y,z: (x\to (y\to z))=(y\to (x\to z))$
Si on n'exige aucune propriété supplémentaire, tu es en logique linéaire dite "intuitionniste". Si tu ajoutes qu'il existe une involution décroissante, tu es en logique linéaire classique (qui diffère très peu de l'intuitionniste, car le simplement fait par exemple de se restreindre à $A_x\{y\in P\mid \exists z: y=(z\to x)\}$ permet de fabrique une classique (et même plein de classiques à partie de l'intuionniste de départ, ceci étant dû à l'involution $[((a\to k)\to k)\to k]\mapsto [a\to k]$ à $k$ fixé.
Tu récupères alors les autres logiques, ou bien en supposant "de l'extérieur" des propriétés supplémentaires, ou bien en supposant $(P,\leq)$ complet comme ordre (toute partie de $P$ a une inf) et en te demandant qui est $\geq $ cojonction des axiomes qui te plaisent (ces éléments étant appelés "théorèmes de la structure $L$ qui plaisent à Georges"
Quant au reste il est possible que j'aie anticipé, mais la référence que j'ai donnée a eu l'air de plaire à Georges donc on verra plus tard ce qu'il en est. C'est vrai que j'ai lu des trucs qui essayaient de généraliser cette notion de complétude, et elle est similaire à ce que tu proposes Christophe, quoiqu'un peu plus générale : c'est la logique algébrique (avec des qualificatifs "universelle" ou "abstraite" qui sont là pour enjoliver). En fait ça revient essentiellement à de l'algèbre universelle où on prétend que les opérations sont des connecteurs logiques, et où on se rajoute une relation $\vdash$; que l'on peut comparer (via ce qu'ils appellent des "matrices" qui correspondent à ce qu'on voudrait appeler des modèles, qui consistent en une algèbre pour le type considéré et un "filtre" sur cette algèbre, qui n'est rien de plus qu'une partie close pour $\vdash$ il me semble) à une relation $\models$. La variété d'algèbres choisie sera "complète" pour le "système logique" en question si $\vdash$ et $\models$ coïncident. Et donc c'est là-dedans qu'intervient l'algèbre universelle et ce dont j'ai parlé avec la subdirecte irréductibilité (qui revient à ce que tu as dit, Christophe, sur les idéaux premiers en gros, pour les algèbres de Boole : c'est le même phénomène qu'on observe sur la logique). Pour la logique classique on trouve les algèbres de Boole, dont la variété est engendrée par $\{0,1\}$ et ça donne le fameux théorème, et pour la LI on trouve les algèbres de Heyting, dont la variété est plus grosse donc a plus de membres subdirectement irréductibles
Ça c'est essentiellement pour la logique propositionnelle mais il parait (je n'ai jamais vraiment lu la preuve par contre, juste une idée) que ça peut marcher pour la logique du premier ordre. Mais pour une plus grande généralité et pour vraiment incorpoer naturellement les logiques d'ordre supérieur (ça prend en compte tout ce que j'ai pu rencontrer qui s'appelait "logique"), il y a la théorie des institutions, qui prend un point de vue totalement abstrait sur la question, en disant que les théories sont des trucs reliés par des flèches (une catégorie "synatxique") et qu'elles sont reliées via une relation $\models$ a des trucs (les modèles, une catégorie "sémantique") eux-mêmes reliés par des flèches, le tout satisfaisant certaines règles de cohérence qui font qu'on peut appeler toute institution un "système logique". Mais là je n'y connais rien (à part l'idee et quelques bribes de définitions - qui m'ont l'air naturelles puisque c'est des choses que j'avais trouvé en essayant de définir personnellement ce qu'etait un "système logique") donc je n'en dirai pas plus
Il y a ceci qui en parle aussi.
On fixe un ensemble $E$ bien fondé et tel que $E^2\subset E$ de sorte qu'on n'a pas de problème en définissant $x\to y$ par $(x,y)$. Etant donné une partie $X$ de $E$, je note $m(X)$ son stabilisé par modus ponens (ie l'intersection de toutes les parties $Y\subset E$ telles que $X\subset Y$ et $Y$ stable par modus ponens).
Il arrive très souvent, quand cette thématique est concernée que je jongle dans tous les sens avec des tas de parties $Z$ de $E$ que je déclare être telle que $m(Z)=LogiqueIntuitionniste^*$, au point qu'un lecteur qui a le courage de me suivre ou qui s'intéresse à ces questions doit se demander quelle mouche me pique et pourquoi je suis aussi instable dans mes différents $Z$.
Face à ça, on peut se demander si j'ai raison ou tort de prétendre que pour chacun de ces $Z$, il est vrai qu'en plus, il en va de même avec la lagoqie affine, la logique linéaire (je varie presque tout autant de $Z$ pour ces dernières).
Alors pour ça j'ai "un truc de prestidigitateur"**** que je suis tout à fait disposé à te décrire sur un post assez longs (ou plusieurs posts enchainés quand j'aurai le temps, mais je veux d'abord savoir si c'était ça ta demande)
Pour être concrets:
1/ exemples de $Z$ différents que je prétends souvent générer la logique linéaire:
$Z_1:= $ l'ensemble de toutes les formes $(a\to b)\to ((b\to c)\to (a\to c))$ + $a\to ((a\to b)\to b)$
$Z_2:= $ l'ensemble de toutes les formes $(a\to b)\to ((c\to a)\to (c\to b))$ + $a\to ((a\to b)\to b)$
$Z_3:= $ l'ensemble de toutes les formes $(a\to b)\to ((c\to a)\to (c\to b))$ + $(a\to (b\to c))\to (b\to (a\to c))$
$Z_4:= $ l'ensemble de toutes les formes $(a\to b)\to ((b\to c)\to (a\to c))$ + $(1\to a)\to a$ + $a\to (1\to a)$
etc, etc, j'en ai plein d'autres en magasin
2/ exemples de $Z$ différents que je prétends souvent générer la logique affine :
$Z_5:= $ l'ensemble de toutes les formes $(a\to b)\to ((b\to c)\to (a\to c))$ + $a\to ((a\to b)\to b)$ + $a\to (b\to a)$
$Z_6:= $ l'ensemble de toutes les formes $(a\to b)\to ((c\to a)\to (c\to b))$ + $a\to ((a\to b)\to b)$ + + $a\to (b\to a)$
$Z_7:= $ l'ensemble de toutes les formes $(a\to b)\to ((c\to a)\to (c\to b))$ + $(a\to (b\to c))\to (b\to (a\to c))$+ + $a\to (b\to a)$
etc, etc, j'en ai plein d'autres en magasin
3/ exemples de $Z$ différents que je prétends souvent générer la logique intuitionniste :
$Z_8:=$ Toutes celles qui précèdent quand on leur ajoute $(a\to (a\to b))\to (a\to b)$
$Z_9:=$ l'ensemble de toutes les formes $a\to (b\to a)$ + $(a\to (b\to c))\to ((a\to c)\to (b\to c))$ (c'est celle des manuels, loool la plus pourrie et la plus ancienne)
etc, etc, j'en ai plein d'autres en magasin
Bon je ne continue pas.
Bien évidemment, ce n'est pas très dur, en théorie un gars (ou une fille) n'a qu'à vérifier que $X\subset m(Y)$ pour s'assurer que $m(X)\subset m(Y)$, mais vu que s'amuser à écrire un interminables phrase avec que des $\to$ est une torture, tu t'imagines bien que je ne passe pas par là. Si c'est ça ta volonté (comment choisir des axiomes qui donnent telle ou telle logique et voir en 3 secondes qu'on ne s'est pas gourré), je te répondrai en détails.
C'est d'ailleurs exactement pour les mêmes raisons que je "sais vite" quels axiomes "toujours mettre à la base" permettent de rendre valide le théorème qui dit que pour tout théorème de maths $P$ il existe des $H_i$ qui sont tous des axiomes tels que $H_1 = (H_2\to (H_3\to ....\to (H_n\to P)...)$
C'est encore pour la même raison que je peux par exemple "conjecturer" (et peut-être parfois affirmer quand j'ai un coup dans le nez) que $Z:=$ l'ensemble des formes $(b\to c)\to (a\to ((a\to b)\to c))$ + $a\to (b\to a)$ + $(a\to (a\to b))\to (a\to b)$ ne permet pas d'obtenir la LI (je n'ai jamais cherché à le prouver, je sais juste prouver que si c'était vrai le père Noel existerait et je m'en contente).
* enfin logique minimale (ça ne change rien, la LM est la LI quand on se restreint aux théorèmes de LI qui sont écrits avec seulement le signe $\to$)
**** en fait, je pense que je n'ai rien inventé et que tous les CCH-istes sont encore bien plus forts que moi à ce petit jeu, mais le problème est que je n'en cotoie pas pour faire un concours de "qui va le plus vite", donc je ne sais pas. Sur le forum, on a GBZM qui est un gros expert, mais je n'ai pas l'impression qu'il soit spécialement orienté CCH, et il y a alesha qui semble très expert (entre autre en CCH?), mais qui ne s'est jamais manifesté sur ce jeu par exemple. Foys s'est intitié à la CCH ces dernières années si je ne me trompe pas, mais je pense qu'il a été content de rencontrer (il comprendra :-D le couple $(S,K$ et qu'il n'a pas forcément passé ses dimanches à collectionner les autres systèmes de générateurs). Pardon si j'oublie des gens: ces trois-là, tu pourras t'adresser à eux le cas échéant.
En tout cas, je ne vois que cette manière d'interpréter ta demande, parce que la notion de complétude est un peu trop vide comme je te l'ai dit (on peut très bien choisir de manière adhoc une sémantique qui convient après un geste capricieux qui impose des axiomes (pas trop fantaisistes non plus, puisqu'il faut que si $x\in m(Y\cup \{y\})$ alors $(y\to x)\in m(Y)$, mais ça s'obtient sans payer cher ça).
soit $(E,\to,1)$ un ensemble doté d'une application de $E^2$ dans $E$ telle que :
$$\forall x,y,z: [((1\to x)=x)\ et\ ((x\to (y\to z))=(y\to (x\to z)))]$$
En gros, c'est la base de chez base avec laquelle on perçoit les phrases (en particulier, si on les perçoit dessinées, il n'y a pas vraiment d'ordre dans lequel sont faites les hypothèses).
L'ensemble, que j'appellerais "ensemble des post-axiomes" est le plus petit ensemble $A$ qui contient tous les $x\to x$ et stable par l'opération suivante:
si $x\to x'$ et $y\to y'$ sont tous deux dans $A$ alors $(x'\to y)\to (x\to y')$ est aussi dans $A$
Il y a dans $A$ un petit peu plus que juste des axiomes "solennels". Les suites évoquées dans la suite peuvent être vides.
L'ensemble $L$ des théorèmes de la logique linéaire est l'ensemble des $x$ tels qu'il existe une suite finie $u_0,..,u_n$ telle que $[(u_0\to u_0)\to ((u_1\to u_1)\to ...\to ((u_n\to u_n)\to x)....)]\in A$
L'ensemble F des théorèmes de la logique affine est l'ensemble des $x$ tels qu'il existe une suite finie $u_0,..,u_n$ telle que $(u_0\to (u_1\to (...\to (u_n\to x)...)\in L$ où chaque $u_i$ est dans $K:=$ l'ensemble des éléments de la forme $x\to (y\to x)$
L'ensemble $Intu$ des théorèmes de la logique affine est l'ensemble des $x$ tels qu'il existe une suite finie $u_0,..,u_n$ telle que $(u_0\to (u_1\to (...\to (u_n\to x)...)\in F$ où chaque $u_i$ est dans $W:=$ l'ensemble des éléments de la forme $(x\to (x\to y))\to (x\to y)$
De la sorte, les axiomes sont assumés, l'espèce de "composition évidente" qui définit la règle (concernant des pointeurs, donc ne posant aucun problème!!) est mise au centre en début de construction.
L'ordre ne me semblait pas venir en premier, mais je ne saurai vraiment dire pourquoi. Par contre, je voulais que les deux éléments qui sont appelés à devenir plus grand et plus petit soient déjà là au départ, car je me disais que ça ne mangeait pas de pain, et que ça ne me paraît pas si dingue de demander que toute logique ait un "vrai" et un "faux".
L'application binaire $\to$, je la voulais également au départ.
Je me suis donc dit : définissons un "espace de phrases logiques" comme étant tout juste un quadruplet $(E,\to,\top,\bot)$ (qui n'est rien censé vérifier a priori), définissons les "démonstrations" dedans comme ci-dessus. Définissons les "morphismes" d'espaces de phrases logiques comme étant ce qu'on imagine. Ensuite, le jeu est de trouver des relations d'équivalence de plus en plus larges qui soient compatibles avec la structure d'espace de phrases logiques (i.e. telles que le quotient hérite naturellement d'une structure d'espace de phrases logiques et telle que la projection canonique soit un morphisme) et constater que plus on quotiente, plus il est possible d'étendre naturellement la structure pour se rapprocher d'une algèbre de Boole.
Mon problème est que quand je quotiente par la relation d'équivalence "$a$ et $b$ sont équivalents" si "$a\to b$ et $b\to a$ sont des théorèmes intuitionnistes", je n'ai pas l'impression d'obtenir tout de suite une algèbre de Heyting : je peux, certes, définir un ordre tout à fait naturel, de la façon suggérée par Max, mais il semble que ça n'en fait pas une algèbre de Heyting en général, parce que rien n'assure que les inf et sup existent déjà dans le quotient. Bien au contraire, l'idée que l'inf de $a$ et de $b$ pourrait être $((a \to (b \to \bot))\to \bot$ ne marche pas car l'opération n'est pas idempotente en général ; et ta remarque (qui pour l'instant, me semble mystérieuse), selon laquelle le "et" n'est définissable qu'au second ordre va dans ce sens aussi.
En tout cas, ma situation est que je joue avec des trucs, et en les manipulant, je constate que je m'attends à des choses qui n'arrivent pas. Ces choses, auxquelles je m'attends sont des "slogans" que j'ai extraits de choses que tu as dites sur le forum, et je ne sais pas si j'ai mal interprété ce que tu as dit, ou si j'ai oublié des choses.
Je suis désolé, je n'ai pas eu le temps de lire en détail les précédentes interventions, et j'ai rencontré des problèmes techniques pour poster. Mais je vais tout lire ! Merci pour toutes les informations !
En fait l'INF est à part et le vrai n'est la borne sup que des éléments jetables (ie vérifiant que pour tout y , y est plus petit que x=>y (on peut jeter x)).
Il faut un "acte de foi" pour ajouter les axiomes qui vont te donner les logiques traditionnelles (intuitionniste et classique) qui consiste en gros à demander que chaque phrase est idempotente. A savoir que la supposer deux fois ne diffère pas de la supposer une fois.
C'est pour ça que quelques poste plus hauts je t'ai donné la réalisation du programme que tu décris. Vérifie si ça te plait.
Déclarer que $H$ prouve $A\land B$ si et seulement si $H$ prouve $A$ et $H$ prouve $B$ semble à mes yeux ne pas relever de l'acte de foi mais plutôt de la définition de "et". Je comprends que tu as en tête la logique linéaire; et la question de "peut-on véritablement réutiliser les hypothèses ?" (comme par exemple dans "J'ai un gâteau au chocolat" $\vdash$ "Je le mange" qui n'entraîne pas qu'on puisse dupliquer le chocolat), mais il me semble (dis-moi si je me trompe !) que l'introduction de la logique linéaire n'a pas une visée "philosophique" (contrairement par exemple à ma "définition" du "et") mais plus "pratique", au sens où il est vrai par exemple qu'en informatique on ne puisse pas réutiliser les données et différents trucs. Enfin en gros je ne vois pas trop ce que tu entends par "a été remis à plat", ni par "erreur"
1) il voue aux gémonies la CCH (qu'il ne connait pas du tout), et encore plus probablement la CCH correcte, celle qui s'accorde avec la TDE (qu'il ne connait pas non plus (il s'en vante, il ne se contente pas de "l'avouer" :-D ))
2) Il a un but (ce n'est pas une erreur, un but n'est pas une erreur) extrêmement ambitieux qui est de trouver un moyen de réaliser que chaque théorème aurait une unique preuve. L'erreur est dans les moments où il croit avoir réalisé ce programme.
Dans presque les 2 cas, il n'ignore pas sa subjectivité, et c'est volontaire, rien à voir avec de l'ignorance.
On est très très loin de Georges!!! Qui, pour te donner un ordre d'idée, se demande s'il y a un chemin de nature essentiellement DEDUCTIVE qui voudrait que si $x\leq a$ et $x\leq b$ alors $(a\to (b\to c))\leq (x\to c)$.
Ce n'est pas une affaire de LL. Le fait que je la connaisse un peu me permet de répondre, mais elle n'y est pas pour grand -chose. Par exemple quand j'ai écrit mon article sur la logique annelée*** , c'était idem, la LL me permettait d'envisager" un petit topo de 3-4 pages, mais ensuite l'article s'est "écrit tout seul" sans que j'utilise ma culture de la LL.
AP, évidemment qu'il a choisi les outils qui lui permettent de s'épanouir (catégories cartésiennes fermées, topos), et qui donnent dans leur définition même la LI (les cat cartésiennes fermées sont tout aussi bien que les topos pour cette oeuvre d'ailleurs, les topos donnent juste un sens à $=$). Mais Georges (semble-t-il) ne demande pas "comment on force des définitions qui vont donner la LI". Il semble souhaiter plutôt justement comprendre comment on y arrive ou pas, selon les chemins qu'on prend. J'ai donc adapté ma réponse à ça.
D'une manière générale (même si je connais l'engouement et la militance actuelle de plein de gens), je ne pense pas que le paradigme catégorique permette de "bien aborder" ces problématiques (la preuve d'ailleurs, si tu arrives à "forcer" la LI (comme par exemple AP le fait), c'est que ça ne va pas, il y a des choses qui sont collapsées qui ne devraient pas l'être et de fait j'en ai trouvé pas mal qui le sont, mais ce n'est pas le sujet du fil)
Concernant la "fascination" de AP (je la comprends, c'est de l'art) pour le fait que les définitions suivantes:
$(a\wedge b) := ((a,b)=(vrai,vrai))$
$(a\to b) := ((a\wedge b) = a)$
$(\forall xR(x)) = ((x\mapsto R(x))=Constante(vraie))$
connues depuis je pense Leibniz (qui avait donné "la bonne" définition de $=$) semblent permettre de tout faire en partant de $=$, je la partage, mais ce n'est pas parce que quelqu'un fait un quadruple saut périlleux devant toi qu'il va t'indiquer correctement où se trouve la station "porte dorée". Ce sont deux choses différentes. De plus, vu qu'au fond, ce qu'il raconte en 400 pages, pourrait (à condition d'enlever un certain nombre de choses non nécessaires à l'information du lecteur qui veut juste savoir ce que signifie langage interne, etc, parce qu'il a entendu ça à la télé et que ça le fascine) pourraient l'être en 10 (je viens de le faire en 3 lignes bleues en exagérant un peu), on sent bien qu'il y a de la subjectivité dans l'air et une volonté d'avoir un produit d'appel pour ensuite faire visiter le magasin sur ses 10 étages.
*** Soit $A$ un anneau commutatif unitaire. Les phrases sont les idéaux de $A$. L'implication est $J\to K:=\{x\mid \forall y\in J: xy\in K\}$. L'adjoint de $\to$ est le produit des idéaux alors que la borne inf est l'intersection (l'ordre sur ces phrase est la simple inclusion). Dans le papier que j'ai écrit, il est prouvé (ce n'est pas très dur) que:
a) un anneau $\models $ la logique intuitionniste ssi tous ses éléments sont des multiples de leur carré
b) un anneau $\models $ la logique classique ssi il est isomorphe à un produit fini de corps
En outre, la logique annelée n'est pas TOTALEMENT incluse dans la logique intuitionniste, puisqu'au second ordre, la logique annelée considère comme un théorème que $buveur\to RPA$
Non, ce n'est pas trop ce que je voulais. Pour l'instant, je voudrais juste manipuler plusieurs groupes d'axiomes, me familiariser avec, constater que certains sont équivalents ou non, etc. Je suis en "phase découverte", même si j'aimerais bien un cadre général pas trop compliqué pour avoir des idées claires sur la logique (d'un niveau élémentaire, certes).
J'ai l'impression que je vois ce que tu veux dire, mais je ne considère pas ça comme très embêtant pour l'instant. Je pense que je serai satisfait quand j'aurai une réponse claire à cette question, d'ailleurs !
Ben, pour l'instant, comme je suis en mode découverte, je vais partir du point de vue selon lequel l'ordre des hypothèses importe, quitte à quotienter après, évidemment.
Ben ça me chagrine un peu parce qu'au début, je pensais qu'il n'y avait pas besoin de plonger dans un treillis. C'est ce que ton slogan (que je déforme sûrement) "on peut tout définir avec $\to$" m'avait inspiré, d'ailleurs !
C'est bien le genre de point de vue que je voulais adopter, et donc je pense que tes références et mots-clef vont bien m'aider !
Je n'aime pas trop le cours d'Alain Prouté. Je ne sais pas trop où il veut aller, et le fait qu'il n'y ait pas d'index et que parfois (à moins que j'aie vraiment craqué) des notations apparaissent avant d'avoir été définies rend la lecture assez difficile...
EDITS : Ca ne voulait rien dire car j'avais oublié des trucs.
Preuve: supposons que $a\to s$ et $(a\to b)\to s$. Alors $(s\to \bot)\to \bot$. Donc, si on te suit, il en découle $s$. Je viens de prouver que $Georges\to TiersExclus$, puisque moralement j'ai prouvé $a\vee(a\to b)$
Edit: je détaille, je ne pense pas que tu veuilles faire l'exo de chercher lool. Si $s\to \bot$, alors $s\to b$, donc $a\to b$, donc $s$. Conclusion $(s\to \bot)\to ((s\to \bot)\to \bot$, donc $(s\to \bot)\to \bot$.
joli^^
@GA: oui, mais plus, je voulais dire plussss, la LI est très bancale*** comme logique, car tout repose sur le fait que sa seule différence avec la LC est de NE PAS admettre que non(non(A)) => A où $non(A)$ est une abréviation de A=>Tout.
Il suit que dès lors que tu l'admets, c'est fini, adieu la LI, tu es en LC.
La (ou une) définition de la LI est que c'est l'ensemble des énoncés $P$ tels que $\emptyset \vdash P$ où $\vdash$ est le plus petit ensemble contenant
l'ensemble des $X\vdash A$ tel que $A\in X$
et tel que $\forall ...: $
si $X\vdash A$ et $Y\vdash (A\to $ alors $X\cup Y\vdash B$
si $X\cup \{A\}\vdash B$ alors $X\vdash (A\to $
Or pour obtenir la LC plus tôt que la LI, il suffit de remplacer l'assymétrie qui fait qu'à droite du $\vdash $ on ne peut avoir qu'nue phrase par la symétrie d'avoir, à droite, un ensemble.
Je te laisse réécrire la définition pour la logique classique.
Le fait de prendre des ensembles cache sous le tapis ce qui "répondait" à la remarque de maxtimax, mais il n'y a aucun moyen sauf à l'admettre comme axiome de prouver linéairement:
$$ (x\to a)\to ((x\to b)\to [(a\to (b\to c))\to (x\to c)] )$$
C'est le droit de "dupliquer" un $x$ qui le permet.