LES  META-OPERATEURS DE LA DEDUCTION

La logique même devient l’objet d’un traitement  axiomatico-déductif analogue à celui de la géométrie. Les déductions ne peuvent plus invoquer  de critères logiques ; elles ne doivent  prendre appui que sur des axiomes et sur des règles établies d’une manière parfaitement explicite.  En théorie de la démonstration certains énoncés ou formules sont pris comme  « axiomes » et certaines « règles d’inférence » sont posées pour inférer de nouveaux énoncés.

A titre d’axiomes ,visant le calcul des propositions « classique » nous prenons les suivants :

1a. |=    P=>(Q=>P)
1b. |=  (P=>Q) = >{[(P=>(Q=>R)]=>(P=>R)}
3.  |=   P = > (Q=>(P&Q)	4a. |=  (P & Q) => P
	4b. |=  (P & Q) =>Q
5a. |=   P=> (PVQ)	6. |= (P=>R)=>[( Q=>R)=>((PVQ)=>R)]
5b. |=  Q=> (PVQ)
7.  |=  (P=>Q)=>[(P=>-Q)=>-P]	8°. |=   --P => P
9a. |=  (P=>Q) => [(Q=>P)=>(P=Q)]	10a. |=  (P=Q) => (P=>Q)
	10b. |=  (P=Q) => (Q=>P)
Modus ponens ou Règle =>     ->	P, P=>Q .=>.Q

Ces formules s’appellent « schémas d’axiomes ».Chaque schéma d’axiome inclut une infinité d’axiomes, un pour chaque choix des formules désignées par « P », « Q », « R ». Par exemple au n°1a : P=>(Q=>P) ce schéma  d’axiome général peut fournir les axiomes singuliers suivants : P=>(P=>P), P=>(Q=>P), Q=>(P=>Q), -P=>[(Q&R)=>-P], etc… Comme règle d’inférence unique, dite « modus ponens », ou règle de détachement, nous prenons  l’opération qui consiste à passer de deux formules de forme P et P=>Q à la formule B, pour n’importe quel choix des formules P et Q. Dans une inférence effectuée avec cette règle, P et P=>Q sont les prémisses, Q la conclusion.

On définit une démonstration formelle (dans le calcul des propositions « classique ») comme une liste finie d’occurrences de formules Qi : iN, dont chacune  ou bien est un axiome du calcul des propositions, ou bien est issue, par application de la règle :  modus ponens, d’une paire de formules qui la précèdent dans la liste. Une démonstration  est une démonstration de sa dernière formule Qi. Si une formule a une démonstration, on dit que Q est formellement démontrable ou encore que Q est un théorème ; en symboles : |- Q.

Exemple de déduction :  soit à démontrer C , à partir de A=>(B=>C), (A&B)

1. A&B	2ème hypothèse
2. (A&B) => A	Schéma d’axiome
3.A	MP:modus ponens: 1,2
4. A => (B=>C)	1ère hypothèse
5. B=>C	MP:3,4
6.  (A&B) => B	Schéma d’axiome
7. B	MP:1,6
8. C	MP:7,5
.=>.A=>(B=>C, A&B  |--  C