Solutions de quelques exercices 1 p /\ q => q /\ p introImp introEt q elimEt2 Axiome p elimEt1 axiome 2 p /\ (q /\ r) => (p /\ q) /\ r introImp introEt q elimEt1 p elimEt1 axiome introEt r elimEt2 p elimEt1 Axiome q/\r elimEt2 Axiome 3 ( (p /\ q) /\ r) => p /\ (q /\ r) introImp introEt introEt p/\q elimEt1 Axiom p elimEt1 r elimEt2 Axiom q elimEt2 r elimEt2 Axiom 4 p /\ (q /\ r) <=> (p /\ q) /\ r (a vous d'encoder <=> grace a => et /\) composer les 2 precedetnts 5 p \/ q => q \/ p introImp p q elimOu introOu1 Axiome introOu2 Axiome Axiome 6 (p \/ (q \/ r) => (p \/ q) \/ r ) introImp p q\/r elimOu q r elimOu introOu2 Axiom introOu1 introOu2 Axiome Axiome introOu1 introOu1 Axiome Axiome 7 (p \/ q) \/ r => p \/ (q \/ r) introImp p\/q r elimOu introOu2 introOu2 Axiome p q elim0u introOu2 introOu1 Axiome introOu1 Axiome Axiome Axiome 8 (p /\ (q \/ r) => (p /\ q) \/ (p /\ r)) introImp q r elimOu introEt Axiome q\/r elimEt2 Axiome introOu1 introEt Axiome q\/r elimEt2 Axiome p elimEt1 Axiome 9 (p \/ (q /\ r) => (p \/ q) /\ (p \/ r)) introImp introEt p q/\r elimOu introOu2 q elimEt1 Axiome introOu1 Axiome Axiome p q/\r elimOu introOu2 r elimEt2 Axiome introOu1 Axiome Axiome 10 (p => q) /\ (q => r) => (p => r) introImp introImp q elimImp p elimImp Axiome q=>r elimEt2 Axiome p=>q elimEt1 Axiome 11 ((p /\ q => r) => (p => (q => r))) introImp introImp introImp p/\q elimImp introEt Axiome Axiome Axiome 12 ((p \/ q => r) => (p => r) /\ (q => r)) /\( (p => r) /\ (q => r) => (p \/ q => r) ) 13 (p => ~ ~ p)/\ (p <= ~ ~ p) le reecrire (p => ~ ~ p)/\ (~ ~ p =>p) introEt introImp elimFaux ~p introFaux Axiome Axiome introImp introNon p introFaux Axiome Axiome 14 (p => q) => (~ q => ~ p) introImp introImp introNon q introFaux Axiome p elimImp Axiome Axiome 15 (~ q => ~ p) => (p => q) IntroImp introImp p elimFaux p introFaux ~q elimImp Axiome Axiome Axiome 16 ~ (p \/ q) <=> ~ p /\ ~ q (a vous d'encoder <=> grace a => et /\) 16-1 ~ (p \/ q) => ~ p /\ ~ q IntroImp IntroEt introNon introFaux p\/q IntroOu1 Axiom Axiom introNon introFaux p\/q IntroOu2 Axiom Axiom 16-2 ~ p /\ ~ q => ~ (p \/ q) introImp introNon elimOu p q Axiom introFaux p Axiom elimEt2 ~q Axiom introFaux q Axiom elimEt1 ~p Axiom 17 ~ (p /\ q) <=> ~ p \/ ~ q (a vous d'encoder <=> grace a => et /\) 17-1 ~ (p /\ q) => ~ p \/ ~ q IntroImp ElimFaux ElimNon ~p\/~q Axiom introOu1 introNon elimNom ~p\/~q Axiom introOu2 introNon elimNon p/\q axiom introEt axiom axiom 17-2 ~ p \/ ~ q => ~ (p /\ q) introImp introNon introFaux p elimEt2 q axiom introNon introFaux q elimEt1 p axiom elimOu ~p ~q Axiom elimNon p axiom axiom elimNon q axiom axiom 18 ~ (p => q) <=> p /\ ~ q (a vous d'encoder <=> grace a => et /\) 18-1 ~ (p => q) => p /\ ~ q introImp introEt ElimFaux introFaux p=>q introImp ElimNon p axiom axiom axiom introNon introFaux p elimFaux introFaux p=>q introImp axiom axiom introNon introFaux p=>q introImp axiom axiom 18-2 p /\ ~ q => ~ (p => q) IntroImp introNon introFaux q elimImp p axiom elimEt2 ~q axiom elimEt1 p axiom