Les axiomes de calcul propositionnel

Par définition, un théorème est une formule qui est démontrable à partir d'un système d'axiomes donnés, étant données certaines règles de déduction, donc la réponse à la question telle qu'elle est posée est évidente.

Ce qui est plus surprenant, c'est que dans le système "classique" de démonstrations du calcul propositionnel, on peut démontrer toutes les tautologies (où $P$ est une tautologie si et seulement si toue évaluation de $P$ dans $\{0,1\}$ donne $1$); et qu'on a donc une coïncidence tautologies $\leftrightarrow$ théorèmes

Un système d'axiomes sera suffisant pour les théorèmes du calcul propositionnel classique si et seulement si il permet de prouver les formules suivantes (par contre il peut en prouver trop et n'être pas équivalent au calcul propositionnel classique), pour toutes formules $A,B,C$ :

$A\land A \iff A, A\lor A \iff A, A\land B\iff B\land A, A\lor B \iff B\lor A, A\land (B\land C) \iff (A\land \land C, A\land (A\lor \iff A, A\lor(A\land \iff A$

$A\land (B\lor C) \iff (A\land \lor (A\land C), A\lor (B\land C) \iff (A\lor \land (A\lor C)$

$A\land \top \iff A, A\lor \bot \iff A, A\land \bot \iff \bot, A\lor \top \iff \top$

$A\land \neg A \iff \bot, A\lor \neg A \iff \top$

Pour voir si le système que tu présentes permet de démontrer tous les théorèmes du calcul propositionnel, il te suffit de vérifier ces propriétés.
(Remarque: certains auteurs n'utilisent pas $\top, \bot$. Tu peux soit les prendre comme primitifs, soit choisir une proposition $A$ et dire $\bot = A\land \neg A, \top = A\implies A$)

Etant sur un pc, j'ai un peu plus de confort pour commenter ton:

shade a écrit:

un système complet de connecteurs se fait à l'aide des axiomes:
A1: (A->(B->A)) (si la partie droite est vraie alors toute l'implication est vraie)
A2: (A->(B->C))->((A->B)->(A->C)) (transitivité)
A3: (principe d'explosion: décrit en haut comme

1) Tes axiomes A1,A2 forment un système complet pour la logique intuitionniste. C'est le premier historiquement, mais les auteurs de livres ont une sale tendance à se ridiculiser à toujours le reprendre, alors qu'il est fort criticable par ailleurs. C'est à se demander s'ils écrivent leurs livres ou les copie-collent parfois. Je ne peux pas croire qu'ils n'en connaissent pas d'autres.

2) Pour obtenir la logique classique, tu peux AU CHOIX prendre un des suivants:

a) $((A\to \to A)\to A$
b) $((A\to \to \to ((B\to A)\to A)$ (qui littéralement dit (A ou => (B ou A))
c) $((A\to Tout)\to Tout)\to A$
d) $((A\to Tout)\to \to (((A\to \to )$ (qui littéralement dit que si A, ainsi que nonA impliquent tous les deux B alors
e) $(A\to \to ((B\to A) \to C)$ (qui littéralement installe qu'on a toujours A=>B ou B=>A)
Édit: e) (((A=>B)=>((B=>A)=>C))=>C

J'arrête là la liste, on a l'embarras du choix.

3) Je critique surtout A1 et A2, qui hélas ne présente pas du tout les choses de manière à ce que l'entendement puisse donner du relief. Enfin, la crotique porte surtout sur A2, qui mélange trnaistivité et duplication (il est réalisé par le combinateur appelé S qui agit ainsi: ((S u) v) w $\to $ ( uw ) (vw ) , dont on voit qu'il DUPLIQUE l'aliment w avant de le redistribuer à u et à v (un exemplaire chacun).

4) Mieux vaut séparer (tant pis, on a plus de formules mais ce n'est pas grave).

4.1)

a) $a\to (b\to a)$ (droit de jeter une hypothèse; ie droit de POUBELLE!!! C'est un prix, ce n'est pas rien que de disposer de poubelles)

b) $(a\to (b\to c))\to (b\to (a\to c))$ (commutativité des hypothèses: là, au moins, on "sent" qu'on est sur une logique bien plus sûre, puisque dans la vraie vie, les gens d'eux-mêmes affecte très exactement le même sens à des phrases si on a juste permuté leurs hypothèses, ceci venant d'ailleurs du fait qu'"in the real life", les hypothèses ne sont pas forcément listées "en ligne", elles peuvent être tacites ou dessinées)

c1) La VRAIE transitivité s'énonce plutôt en disant: $(a\to b)\to ((c\to a)\to (c\to b))$

c2) Mais tu peux aussi prendre A La PLACE: $(a\to b)\to ((b\to c)\to (a\to c))$

c3) ou encore $a\to ((a\to b)\to ((b\to c)\to c))$, etc, mais ce n'est possible ces interchangeable que si tu disposes de b)

d) et enfin pour finir, le DUPLICATEUR qui est l'axiome DE LOIN LE PLUS DANGEREUX ET LE PLUS PUISSANT DES MATHS: $(a\to (a\to b))\to (a\to b)$

4.2)


Sache aussi que tu peux te contenter de prendre :

a.bis) $a\to (1\to a)$

b.bis) $(1\to a)\to a$

c.bis) L'axiome ci-dessus numéroté (c.2)

poubelle.bis) $a\to 1$

truisme.bis) $1\to (a\to a)$

Ce système de 5 axiomes SUFFIT à obtenir les axiomes qui vont de (a) à (c) ci-dessus. Si tu es sérieux et veux me remercier de te donner toutes ces infos, tu peux faire l'exo (pas très facile) de le prouver en détails.

@shadesprit : j'ai déjà répondu à ta question en te listant une liste d'axiomes que ton système doit être capable de démontrer pour obtenir la complétude, et qui sont suffisants (si Poirot a raison et que tu parles en fait des tautologies et donc des theorèmes du calcul propositionnel classique)

De mon téléphone: merci et coquille corrigée.