Le jeu "QED - an interactive textbook"

JDG
JDG
dans Fondements et Logique
Bonjour, je m’intéresse à la logique de premier ordre sur mon temps libre.
Je joue au jeu de Terence Tao https://teorth.github.io/QED/ .
Je suis bloqué au niveau 12.1 (a) reduction ad absurdum.
J'aurai besoin d'aide pour la démonstration suivante : étant donné : A => B et non-B déduire non-A
Si jamais quelqu'un y joue je veux bien sa solution !

[Activation du lien. AD]

Réponses

  • Titi le curieux
    Titi le curieux
    Salut,
    Je n'ai pas installé le jeu, mais si ça utilise les règles de la logique du premier ordre, ça doit pouvoir se régler comme suit (symbole |- pour "prouve"):

    - Affaiblissement axiomatique (tu ajoutes A aux hypothèses)
    - Modus ponens (tu déduis B de A et A -> B)
    - élimination de la négation (tu as B et non(B) tu déduis FAUX )
    - Introduction de la négation ( c'est-à-dire puisque A->B, non(B),A |- FAUX, tu conclus A->B, non(B) |- non(A) )

    Et le tour est joué (à deux introductions de l'implication près si tu veux comme forme finale (A->B) -> (nonB-> nonA) ).
    Il a l'air chouette ce jeu! J'ai bien envie d'essayer.
  • Titi le curieux
    Titi le curieux
    Re,

    J'ai tenté le coup avec le jeu. Il se trouve que les lois présentés dans les séries 11 et 12 sont présentés sous des formes un peu différentes que ce que j'ai appris. Du coup ma proposition précédente ne s'applique pas.

    Si tu n'as pas trouvé et que tu veux chercher encore tu dois savoir ceci (la première information est donnée dans l'énoncé, la seconde est une aide de ma part):

    - Il suffit que tu clique le A sur les formules pour avoir accès à ta loi du tiers-exclu sur A dans tes prémisses.
    - ***** petit spoiler ***** tu peux facilement déduire non.A de B et non.B (par l'absurdité intuitionniste, c'est la règle de la série 11 - "ex falso quodlibet").


    ******* GROS SPOILER *******

    Si tu veux directement la réponse, voici la preuve que j'ai obtenu, je commente un peu si c'est un problème de manip:

    -prérequis, dans les formules tu demandes un not A (tu cliques A et c'est proposé)

    Proof

    B AND (NOT B) [assuming A]. [given]

    From B AND (NOT B) [assuming A]: deduce NOT A [assuming A]. [EX FALSO QUODLIBET]

    -pour l'avoir: tu extrais B et not B. De B tu fais B or not A puis tu appliques not B à cette nouvelle formule.

    Deduce NOT A [assuming NOT A]. [IMPLICATION INTRODUCTION]

    - tu ajoutes juste l'hypothèse not A puis ...

    From NOT A [assuming A], NOT A [assuming NOT A]: deduce NOT A [assuming A OR (NOT A)]. [CASE ANALYSIS]
    Deduce A OR (NOT A). [EXCLUDED MIDDLE]

    - la loi est proposée quand tu cliques A dans les formules

    From A OR (NOT A), NOT A [assuming A OR (NOT A)]: deduce NOT A. [MODUS PONENS (ASSUMPTION FORM)]
    QED!


    Bon là-dessus, je continue ma série, je suis intéressé par les exercices sur les quantificateurs (parce que j'ai l'impression que je n'ai pas pigé un truc avec l'élimination du quantificateur universel).

    Bon courage à toi!
  • Titi le curieux
    Titi le curieux
    Je viens de faire la 12.c, je te conseille fortement de la faire avant la 12.a
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 36

AlegDomJean-Louis AymeLirone93Rescassolbiguine_equationchanig +29 Invités