Conjonction et forcing
Bonjour à tous,
Voilà mon problème : j'ai défini la relation de forcing par induction sur la complexité des formules en me servant uniquement des formules atomiques, de la négation, de la disjonction et du quantificateur existentiel (ce qui suffit).
J'ai donc à ma disposition le théorème fondamental du forcing.
Je sais aussi que $p$ force ($\phi$ et $\psi$) ssi $\forall q \leq p, \exists r \leq q$ tel que $r$ force $\phi$ et $r$ force $\psi$.
Comment en déduire (j'en ai besoin pour une utilisation ultérieure) que $p$ force ($\phi$ et $\psi$) ssi $p$ force $\phi$ et $p$ force $\psi$ ?
Merci d'avance.
P.S. : C'est quoi la syntaxe pour :
1) force
2) et
3) ou ?
Voilà mon problème : j'ai défini la relation de forcing par induction sur la complexité des formules en me servant uniquement des formules atomiques, de la négation, de la disjonction et du quantificateur existentiel (ce qui suffit).
J'ai donc à ma disposition le théorème fondamental du forcing.
Je sais aussi que $p$ force ($\phi$ et $\psi$) ssi $\forall q \leq p, \exists r \leq q$ tel que $r$ force $\phi$ et $r$ force $\psi$.
Comment en déduire (j'en ai besoin pour une utilisation ultérieure) que $p$ force ($\phi$ et $\psi$) ssi $p$ force $\phi$ et $p$ force $\psi$ ?
Merci d'avance.
P.S. : C'est quoi la syntaxe pour :
1) force
2) et
3) ou ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Ensuite pour ta question : t'es sûr que ça suffit d'utiliser ces connecteurs ? La logique du forcing est intuitionniste (en gros, bon j'exagère un peu mais tu vois l'idée), donc c'est pas clair à mes yeux que ça suffise...
Je sais plus comment c'est fait d'habitude
Et sinon, je ne sais pas si c'est Boban qui te l'a conseillé, mais comme dit max, il y a une vague illusion d'intuitionnisme qui émerge du forcing, qui a été immédiatement tuée, parce que son et leurs découvreurs n'en voulaient surtout pas.
Mais en gros, travailler avec les $p$ force machin-truc, ça s'appelle purement et simplement une punition pour les enfants de M2 qui bavardent et disperse le prof. Ca serait pertinent si tu voulais t'engager dans une voie qui mène aux topos, et encore mieux, mais pas encore rtès développée, je pense, à la théorie intuitionniste (la vraie) des ensembles (qui sauf erreur ne peut pas exister vue la preuve de l'article que j'ai promis à alesha et qui est sur le (ah mince j'ai oublié le mot "établi"?, non ça sonne mal) juste après Syracuse
Mais sinon, oublie. Si tu veux juste "comprendre" les consistances d'énoncés comme l'axoime de Martin, l'existence d'ultrafiltres de Ramsey, ou la consistance de $ZF + AC_{den} + non(CD)$ ou de $ZF + AxiomeUltrafiltre + non(AC)$, si tu t'embarques dans l'analyse des non bons ouverts d'un espace topologique, tu risque fort de ne jamais arriver à tes fins.
Dis-toi qu'un poset, c'est voué à fournir un espace topologique dont [large]LES BONS OUVERTS[/large] fourniront les valeurs de vérité.
Les posets donnent naturellement un espace topologique, mais il est assez rare que les ouverts soient tous BONS.
"bon ouvert" est une abréviation de "intérieur de son adhérence".
Travailler avec les $p$ force Truc, c'est analyser TOUS les ouverts et non pas seulement les bons. Donc t'imagines: tu veux (exemple, forcing d'ajout d'un réel de Cohen) étudier les bons ouverts de IR, tu oublies "bon" et te voilà parti à explorer tous les ouverts denses de IR, et bé t'as pas fini, puisque toute la théorie descriptive y est déjà depuis 50ans :-D pour en faire "autre chose.
La définition des relations (en général, sans même la commutativité, ni la moindre hypothèse) des garantissages est la suivante:
1/ $p$ force $A\to B$ veut dire pour tout $q: $ si $q$ force $A$ alors $p*q$ force $B$
2/ $p$ force $\forall x R(x)$ veut dire $p$ force tous les $R(a)$
Dans le cas très particulier du forcing, il se trouve que $p*q:=inf(p,q)$, et quand il n'y a pas de inf, on y trouve un substitut.
Dans le cas TRES PARTICULIER encore du forcing, il se trouve qu'il y a des génériques.
Le choix $\exists, \vee$ me parait donc un choix qui a été élaboré et ne tombe pas par hasard, d'autant que GBZM évoque souvent dans son domaine, et sauf erreur de ma part le fait que ce serait "la quantification de la géométrie".
Christophe, je t'explique la philosophie du cours de Boban, qui sort un peu des sentiers battus.
Il est parti d'un article d'un Brésilien qui s'appelle Rodrigo A. Freire, et qui propose une approche axiomatique du forcing.
En gros, on part de 9 axiomes (je pourrai développer si ça t'intéresse), qui décrivent ce que l'on veut faire : partir d'un ground model transitif dénombrable $M$, mettre un ordre partiel $P$ dessus, avec $P \in M$, puis montrer l'existence d'un générique $G$ inclus dans $P$ tel que $M[G] \models ZFC$. Les axiomes contiennent exactement ce qu'on souhaite, y compris le théorème fondamental du forcing. Ensuite, il reste à définir la relation de force, la seule difficulté étant qu'il faut "éliminer" le générique dans les définitions pour pouvoir tout contrôler de l'intérieur.
Je suppose que c'est pour ça qu'il a choisi $\neg, \lor, \exists$.
Ensuite on a vérifié que cette définition permettait bien de récupérer les axiomes 1 à 9, puis on a vérifié que $M[G] \models ZFC$ et on a poursuivi le cours de façon classique.
Mais à un moment donné on a utilisé l'équivalence $p \Vdash (\phi \land \psi)$ ssi $p \Vdash \phi \land p \Vdash \psi$ sans la démontrer.
Je sais qu'il y a un argument de densité là-dessous mais je n'y arrive pas.
Quelqu'un peut-il développer un peu ?
Boban acquiesçait, mais ne cherchait pas à développer (c'est vrai que c'était hors sujet).
Je m'étais toujours dit qu'un jour je demanderais à l'étudiant où diable il avait étudié ces questions, mais je ne l'ai jamais revu "en live" pour des raisons que tu devines.
Je pense que tout cela est affaire de goût.
Du coup, tu as évidemment des gens qui vont s'amuser avec ça. C'est une forme de cloture pratique.
Une manière d'obtenir la logique classique dans un monde a priori intuitionniste est de rajouter
$$ \forall X\exists Y: X = non(Y)$$
Du coup, je ne suis pas à ton cours, mais il est possible que le gars ait trouvé sympa de définir ce que signifie
$$ p\Vdash non(A)$$
avant toute chose.
Dans ce cas, quand $p$ ne force pas $A$ et que l'ensemble de ses minorants qui forcent $A$ est dense sous lui, tu auras probablement une contradiction avec le fait que, par densité
$$[r \Vdash non(A)]\iff [\forall s\leq r: non(s\Vdash A)]$$
Mais comme je ne connais pas tes définitions.
En tout cas, retiens bien que LE BUT est classique.
Un réel de Cohen appartient TOUS les ouverts denses de $[0,1] \cap \R_{vieux}$. Si tu ajoutes plein de Cphen, il en ira de même de tous.
Si tu ajoutes $k$ Cohen avec $k$ cardinal extendible par exemple, chacun d'eux sera ainsi. Et $\omega_1$ restera un ordinal dénombrable (donc non(HC) sera gagnée) non pas parce que $\R$ est $CCC$, mais parce qu'il existera un $n$ entier non nul tel que ils seront séparés par des intervalles de LARGEUR $1/n$ (or il n'y a qu'un nombre FINI) à pouvoir être 2 à 2 disjoints (le dénombrable ne suffirait pas car tu peux tout rendre dénombrable, vu que les choses se passe A l'EXTERIEUR de l'univers.
Du coup, tu vois ce qui t'attend si tu veux profiter de ça pour te cultiver en intuitionnisme. Ca s'appelle changer ses vacances entre montagne et mer :-D
Pour Boban, tout ceci est l'équivalent de la table de multiplication. Pour des gens "pas tout jeune" (pardon, je sais ce que ça fait de vouloir progresser en ski à 35ans, j'ai essayé et me suis pêté bien des membres), c'est tout de même réconfortant de savoir que tu n'as pas besoin du générique et que tu calculs de "bêtes" valeurs dans une algèbre de Boole.
Après c'est sûr que tout le monde se réfère au générique et par psychologie se demande si le machin est vrai dans $M[G]$, au lieu d'avoir conscience de se demander si c'est vrai dans $\prod_{Generiques} M[G]$.
Je ne veux pas contrarier les conseils qu'ils te donnent, mais manipuler des $p\Vdash A$ est une affaire pour jeunes qui veulent tout faire pêter, arrivé sans aucun effort 2" à ulm, et espérant décorcher un des 5 postes de théorie des ensembles à pourvoir dans le monde (l'infinistime et les gouvernements ont du mal à s'aimer)
Donc à toi de voir. Je peux juste te dire que ça fait mal à la tête.
Je suis d'accord avec Christophe qu'en fait, tu as peut-être défini ce qui est traditionnellement noté $p\Vdash \neg \neg \phi$ au lieu de $p\Vdash \phi$; et que dans ce cas-là, peut-être (à nouveau c'est des détails que j'ai vus il y a longtemps) - faudrait qu'on voie ta définition pour te dire mieux.
Ça c'est sûr.
@Max : oui tu as raison.
Je vais découper un bout de mon fichier et vous l'envoyer.
Tu verras, tureviendras toujours à ça.
Et deux espaces topologiques homéomorphes donnent le "même" forcing (ou si tu préfères "effet-forcingant" :-D )
Par exemple, prenons le forcing de chez bête consistant à rendre $\omega_1$ pas plus gros que $\omega_1$ en prenant comme conditions les fonctions de domaines inclus dans $\omega_1$ dénombrables de $\omega_1$ dans lui-même.
C'est sûr que stricto sensu, il semble différent du forcing, qui lui sert à quelque chose, consistant à faire de même, mais avec les fonctions de domaine dénombrable inclus dans $\omega_1$ à valeurs dans IR (il force HC celui-ci.
Bin, en fait comme lis sont "essentiellement" équivalents (à prouver certes), le premier, tout en accomplissant l'inutile labeur de faire de tous les éléments de $\omega_1$ des ordinaux dénombrables (ce qui ne sert à rien, ils l'étaient déjà), a le bon gout "en passant" de surjecter $\omega_1$ sur IR.
Evidemment les numéros des définitions, lemmes etc ne correspondent plus, il faut enlever 169 pour que ça corresponde. (Exemple : quand je parle de la proposition 171, en fait c'est la proposition 2).
Merci d'avance, les gars !
Et ensuite, pour définir $p \Vdash (a=b)$, on se sert de la négation de "a différent de b", ce qui semble utiliser le tiers exclu.
Et là, il y a contradiction avec ce que dit Max.
Là, ton texte demande CLAIREMENT que $p\Vdash A$ veuille dire qu'il n'existe pas de $q\leq p$ tel que $q\Vdash non(A)$, autrement dit que l'ensemble des $r\leq p$ soit dense sous $p$.
Pour gagner l'extensionalité, OUI, il vaut mieux rendre non non ok dès les formules atomiques $\in$ et $=$, d'où cette ruse de leur demander dès le départ d'être les non de leur non.
Dans la vraie vie d'ailleurs, $a\neq b$ est reconnu par le peuple quand ils peuvent brandir un propriété de $a$ que $b$ n'a pas, je pense que tu as remarqué: "ah, nan, c'est lui qui était la bas, au fond de la salle car lui il".
Je reviens donc à ma question initiale : quelqu'un peut-il m'expliquer (dans l'optique du papier) pourquoi $p \Vdash (\phi \land \psi)$ ssi $p \Vdash \phi \land p \Vdash \psi$ ?
Hier soir j'étais dans le gaz, je ne palpais rien à cette simple phrase.
MERCI !!!