Logique formelle

Pour la question (e), il devrait y avoir un théorème du cours qui te dit que si $A\vdash B$, alors $\vdash A\to B$, non ?

Pour la question (f), je ne sais pas ce que sont les règles dérivées, ni le principe d'hypothèse; et "les axiomes" dépend de ce que vous avez vu en cours donc il faudra préciser.

Pour la question (g), il faudra préciser ce que veut dire "preuve axiomatique pure".

J'explique un peu pourquoi il faut préciser les définitions ici : en logique de base comme ici, il y a souvent 100000 manières de présenter les choses (en fait, une par enseignant.e en gros), et donc les noms utilisés etc. ne sont jamais les mêmes. On a de la chance puisque la logique de base, c'est "robuste", donc essentiellement toutes ces présentations sont équivalentes; mais néanmoins pour écrire l'équivalence il faut les détails, qui manquent ici.

Je regarderai tout ça quand mon mal aux yeux sera un peu moins fort, mais dis donc ça t'en fait des documents. En tout cas, on va pouvoir t'aider (mais peut-être pas ce soir, même quand c'est écrit gros, j'ai du mal là...

Chaurien a écrit:

se rédigent en français, ou bien dans une autre langue du monde, mais non dans cette espèce de suite de sigles et d'assemblages de signes cabalistiques ne faisant appel à aucun souci de signification.

Cet extrait me fait penser aux critiques des non matheux à l'égard des matheux, allant jusqu'à dire que ces derniers ne pensent pas car ils expriment certains passages de leur discours avec des symboles.
Ce passage ne contient pas plus de symboles que n'importe quel texte d'analyse. S'il y a des critiques à formuler elles ne portent pas sur ça (par exemple, AS3 et AS13 sont équivalents en supposant les autres axiomes dans le système retenu. Noter que ça n'invalide pas la construction)

Il y a eu des progrès énormes depuis la toute fin du 19ième siècle en logique et cette dernière n'a plus rien à voir avec ce qu'elle était aux autres époques que tu cites Chaurien. Le langage mathématique ainsi que la notion de preuve eux-mêmes sont l'objet d'une étude scientifique et en fait mathématique. On peut ne pas connaître mais dans ce cas mieux vaut s'abstenir de porter de tels jugements.

Je trouve ça intéressant. D'ailleurs si vous avez un bon cours pour méga débutant je suis preneur.

ps: Je ne connais que la logique vue dans les première années avec les tables de vérité.

mais j'avoue que si je comprends théoriquement et globalement ce qu'il attend que je fasse, c'est très difficile à envisager quand on ne fait jamais de mathématiques !

Tu as tout dit dans cette phrase. On peut comprendre théoriquement le vélo, mais avoir un prof qui vous dit "vas-y" c'est autre chose.

Bon la question e, n'a pas d'intérêt (en tout cas ne demande pas de manipulation)

Sinon, je te donne un truc général pour prouver FORMELLEMENT les choses, puis tu enlèves la pollution française et tu complètes.

Tu supposes [ non (A et ] et veux prouver [ (nonA) ou (nonB) ]

Que ferais-tu dans le vraie vie?

Un truc du genre, "si j'ai pas (nonA) ou (nonB), alors j'ai pas nonA et j'ai pas nonB"? Pas avoir nonA, c'est avoir A, idem pour B.

Déjà, j'ai utilisé "naturellement" une contraposée, il suffit de retrouver dans tes sigles du document où il est autorisé d'en faire une.

Donc tu peux tenter de compléter cette trame naturelle:

1/ Prouver $non((nonA) \vee (nonB))\vdash (A\wedge $

2/ Conclure

Ensuite, tu peux décortiquer (1):

(1.1) Où se trouve l'axiome qui dit $(non(X\vee Y)) \to (nonX)$

C'est en utilisant DEUX fois cet axiome que :

1.2/ Tu déduiras $non(nonA)$ de $non((nonA) \vee (nonB))$

1.3/ Tu déduiras $non(nonB)$ de $non((nonA) \vee (nonB))$

Voilà, je reste à ta dispo pour décortiquer plus.

Remarque: c'est un peu étrange que votre prof ait choisi ce théorème qui est classique et non intuitionniste, mais bon. Avec "non non = Identité", de toute façon ça passe comme une lettre à la poste.

Je vois que personne ne l'a fait, alors je vais me permettre de faire une petite "explication de texte" de l'exemple présenté : dans ce genre de système de preuve, parfois appelé "axiomatique" ou "à la Hilbert", le principe est simple : on a un certain nombre de formules, "PREM" dans l'exemple (sans doute "prémisses"), dont on veut déduire une autre formule. La démonstration consiste en une suite de formules que l'on peut déduire, ici en 7 étapes. Pour chaque étape, on ne peut ajouter une formule que dans un des trois cas suivants :
- la formule est une des prémisses
- la formule est un des axiomes (par exemple AS8 ligne 3)
- la formule se déduit des précédentes à partir d'une des règles (par exemple ED ligne 5, appliquée aux lignes 2, 3 et 4)
Dans un système à la Hilbert classique (sans doute ce qui est appelé une "preuve axiomatique pure" dans le cours), la seule règle est le modus ponens. Ici, on a un certain nombre de règles dérivées, qui facilitent la rédaction d'une démonstration (car, on ne va pas se mentir, une "preuve axiomatique pure" est très pénible à lire !). En particulier la règle que le cours note PH est très pratique, car elle permet de poser une hypothèse B (HYP dans l'exemple), et si on dérive la formule C (ligne 6 de l'exemple), on peut en déduire la formule $B \rightarrow C$. Poser une hypothèse revient à ajouter une prémisse. Dans l'exemple, "+HYP2" signifie que la formule écrite se déduit de ce qui précède, mais avec la prémisse supplémentaire de l'hypothèse de la ligne 2. La règle PH (ligne 7) signifie en gros : sous l'hypothèse de la ligne 2 ($p \lor q$), on peut déduire la ligne 6 ($(q \lor p) \land r$), et par conséquent on a, sans hypothèse supplémentaire ("HYP2" n'est plus marqué) :
\[ p \lor q \rightarrow (( q \lor p) \land r) \]

christophe c
C'était aussi une réponse pour ceux qui, comme Chaurien, ne sont pas habitués à la logique formelle.

[Inutile de reproduire le message précédent. AD]

@GR, je crois qu'elle a ressenti intuitivement la forte puissance de tes gênes trolliques :-D :-D