Comment traduit-on "vacuously true" ?

Gebrane, pourquoi la 3 non ???
Il y a bien une quantification universelle portant sur l'ensemble vide.

Tu fais une faute : tu devrais écrire "Il N'existe aucun ... ", négation d'une quantification existentielle sur l'ensemble vide, kif kif quantification universelle sur l'ensemble vide ($\neg \exists x\;(x\in \emptyset \wedge A)$ équivaut logiquement à $\forall x\, (x\in \emptyset \implies \neg A)$).

@Foys " L'absence radicale de documentation accessible des règles de base de l'expression des mathématiques" dans les anciens manuels on en parle quand même un peu - je pense par exemple aux Aleph, mais on ne peut pas dire que la démarche soit d'une clarté extraordinnaire. Mais de nos jours il n'y a pas besoin d'aller bien loin pour voir apparaître des difficultés, dans $A \implies B$ par exemple je ne vois pas comment un élève puisse dire autre chose que il faut que A soit vrai pour que B le soit, le donc intuitif.

"A => B" n'est rien d'autre que "non(A et non " en logique classique.

Voici un exemple rédigé par George Tourlakis, où l'on s'attardera sur la démo du point 2 :

Voici un autre exemple de texte rédigé par David Bostock (lire à partir de 'Assume, for reductio, (...)') :

Ce n'est peut-être qu'une impression de ma part mais la majorité des logiciens n'utilisent pas les contextes et donc font comme si la sémantique de la logique classique du premier ordre n'est constituée que de modèles non vides. Cf "$(\forall x P) \Rightarrow (\exists x P)$" (qui est bien conséquence du calcul des séquents tel qu'il est présenté dans la plupart des manuels).

@GaBuZoMeu : et voici une partie du chapitre 3 où l'on s'attardera sur la définition (10) de l'auteur :

christophe c a écrit:

d'éventuelles "politisations" relevant d'hyper-spécialistes (mais je ne sais pas si la politisation va jusque là, j'ai déjà lu des diatribes colériques d'auteurs n'aimant pas

Les calculs des séquents sans et avec contexte sont équivalents pour des théories affirmant l'existence de quelque chose, ou dont le contexte est non vide. Aurtrement dit il n'y a de différence que pour des situations qui n'intéressent que certains puristes. Par contre lorsqu'on est en logique d'ordre supérieur on n'a pas de garantie que les types employés sont tous non vides et les contextes deviennent pertinents.

D'autre part il y a des arguments en faveur des deux approches je dirais.

Contextes:
1°) En fait c'est comme ça que les mathématiciens s'expriment: l'incantation "soient $x$ tel que $P$, $f$ telle que $Q$ et $E$ telle que $R$" signifie qu'on travaille dans le contexte $(x,f,E)$ sous les hypothèses $P,Q,R$.
2°) Les définitions de certains objets syntaxiques sont en fait simplifiées. Par exemple étant donné un contexte (en l'espèce une liste finie de lettres deux à deux distinctes) $\mathcal C$ une formule du 1er ordre sur le langage $\{\in\}$ et sur le contexte $\mathcal C$ est
-$x\in y$ où $x,y\in \mathcal C$
-$\neg P$ où $P$ est une formule du contexte $\mathcal C$
-$A \wedge B$ où $A$ et $B$ sont des formules du contexte $\mathcal C$
-$\exists z F$ où $z$ est une lettre ne figurant pas dans $\mathcal C$ et $F$ est une formule du contexte obtenu en ajoutant $z$ à $\mathcal C$

Les variables liées d'une formule $G$ du contexte $\mathcal D$ sont alors les lettres figurant dans $G$ mais non dans $\mathcal D$

3°) pour certaines sémantiques (relevant à nouveau de la logique d'ordre supérieure, catégories cartésiennes fermées etc) les contextes s'imposent naturellement, comme dans mon premier paragraphe.

Pas de contexte:
1°) définition des preuves plus simple.
2°) par exemple si $\theta$ est une lettre ne figurant pas dans les variables libres d'un ensemble d'énoncés $\Gamma$ et $P$ est un énoncé quelconque, $\Gamma \cup (\exists x P \Rightarrow P[x:=\theta])$ est une extension conservative de $\Gamma$. Ceci est faux en théorie de la démonstration avec contexte (sauf quand le contexte de base est non vide)
3°) un raffinement (edit: plutôt une réciproque un peu élaborée devrais-je dire, l'un n'entraîne pas l'autre) de 2°) est le résultat suivant (on l'énonce avec les connecteurs $\exists,\wedge,\neg$ pour faire vite mais l'adaptation à tout jeu complet de connecteurs est évidente): si $\Gamma$ est un ensemble fini d'énoncés, appelons suite régulière pour $\Gamma$ une suite finie $R_1,...,R_k$ d'énoncés tels que pour tout $i$, $R_i$ est de la forme $F[x:=t] \Rightarrow \exists x F$ ($t$ étant un terme du langage) ou bien de la forme $\exists y G \Rightarrow G[y:=\theta]$ avec $\theta$ non libre dans $\Gamma \cup \{R_1,R_2,...,R_{i-1}\}$; on dira plus bas que $\theta$ est une "lettre critique" de la suite $R$.
Le résultat en question est alors le suivant:
soit $\Gamma \vdash \Delta$ un séquent prouvable en calcul des séquents classique sans coupure et sans contexte. Il existe une suite $R$ régulière pour $\Gamma \cup \Delta$ telle que:
(i) $R \cup \Gamma \vdash \Delta$ est prouvable sans coupure et sans recours aux règles relatives aux quantificateurs (i.e. en pur calcul propositionnel)
(ii) si $F[x:=t] \Rightarrow \exists x F$ (resp. $\exists y G \Rightarrow G[y:=\theta]$ ) est l'une des formules de $R$, $\exists x F$ (resp. $\exists y G$) est une sous formule de $\Gamma \cup \Delta$ qui a une polarité inverse à la sienne dans le séquent.
La preuve est en fait facile (je pense que l'énoncé guide le lecteur sur ce qu'il faut faire): on prend une preuve sans coupure de $\Gamma \vdash \Delta$ et on transforme chaque introduction de quantificateur de sorte à faire apparaître l'élément de $R$ correspondant (quand deux sous-séquents sont mis à contribution dans l'introduction à droite de $\wedge$, on fusionne les suites régulières en remplaçant les lettres critiques pour avoir une liste régulière, il suffit de prouver que ce remplacement est faisable).
A nouveau ce résultat est faux pour des contextes vides.

Ne pas confondre finauds avec finaux !

@GaBuZoMeu: on peut mettre sous forme prénexe une formule en calcul des prédicats avec contexte?

-sans contexte, l'équivalence entre $\neg \left ( (\forall x A) \wedge B\right )$ et $\exists x \neg (A \wedge $ est prouvable lorsque $x$ n'est pas libre dans $A$
-dans tous les modèles vides, quand $x$ n'est pas libre dans $C$, $\neg \left ( (\forall x A) \wedge \exists y C\right )$ est vraie et $\exists x \neg (A \wedge \exists y C)$ est fausse!

Quel est le statut de $\neg (\exists z(z=z)) \wedge \neg \left ( (\forall x A) \wedge \exists y C\right ) \wedge \neg \exists x \neg (A \wedge \exists y C)$ dans une théorie égalitaire?

@Foys : tout séquent démontrable sans contexte l'est aussi avec contexte, pourvu que ce contexte soit suffisamment grand. Ça met un peu de complexité dans le binz, mais c'est la vie !

Par exemple, si $B$ a ses variables libres dans $V$ (disons qu'il s'agit de variables d'autres types que le type de $x$), alors on démontre $(\forall x\;A(x))\wedge B \vdash \forall x\;(A(x) \wedge $ dans le contexte $V$ tandis qu'on démontre $\forall x\;(A(x) \wedge \vdash (\forall x\;A(x))\wedge B$ dans le contexte $V,x$, mais pas dans le contexte $V$.