Adaptez les exercices résolus à votre matière. Inscrivez-vous gratuitement

CLIQUEZ ICI POUR CONNAITRE LES REGLES D'INFERENCE

 

Logique propositionnelle - Regles d'inference de base

 

[Exercice 1]
- s -> t
- t -> r
- s
|- r
1. s -> t       (Premisse)
2. t -> r       (Premisse)
3. s           (Premisse)
4. t           E-> 1,3
5. r           E-> 2,4
[Exercice 2]
- p ^ ~~q
|- q
1. p ^ ~~q     (Premisse)
2. ~~q         E^ 1
3. q           E~ 2
[Exercice 3]
- t v m
- t -> p
- p -> s
- m -> q
- q -> w ^ t
|- s v (w ^ t)
1. t v m           (Premisse)
2. t -> p           (Premisse)
3. p -> s           (Premisse)
4. m -> q           (Premisse)
5. q -> w ^ t       (Premisse)
+- 6. t             (Hypothese)
| 7. p             E-> 2,6
| 8. s             E-> 3,7
| 9. s v (w ^ t)   I v 8
+-
+- 10. m            (Hypothese)
| 11. q            E-> 4,10
| 12. w ^ t        E-> 5,11
| 13. s v (w ^ t)  I v 12
+-
14. s v (w ^ t)    E v 1,6-9,10-13
[Exercice 4]
- p v (r ^ m) -> s
- q ^ s -> t
- s ^ t -> r
|- p -> (q -> s)
1. p v (r ^ m) -> s    (Premisse)
2. q ^ s -> t          (Premisse)
3. s ^ t -> r          (Premisse)
+- 4. p                (Hypothese)
| +- 5. q              (Hypothese)
| | 6. p v (r ^ m)    I v 4
| | 7. s              E-> 1,6
| +-
| 8. q -> s            I-> 5-7
+-
9. p -> (q -> s)        I-> 4-8
[Exercice 5]
- q v r -> ~(p ^ s)
- t v m -> k ^ m
- k -> s
- m -> r
- ~(p ^ s) -> ~(t v m)
|- ~(t v m)
1. q v r -> ~(p ^ s)        (Premisse)
2. t v m -> k ^ m           (Premisse)
3. k -> s                   (Premisse)
4. m -> r                   (Premisse)
5. ~(p ^ s) -> ~(t v m)     (Premisse)
+- 6. t v m                 (Hypothese pour RAA)
| 7. k ^ m                 E-> 2,6
| 8. m                     E^ 7
| 9. r                     E-> 4,8
| 10. q v r                I v 9
| 11. ~(p ^ s)             E-> 1,10
| 12. ~(t v m)             E-> 5,11
| 13. (t v m) ^ ~(t v m)   I^ 6,12
+-
14. ~(t v m)               I~ 6-13
[Exercice 6]
- p -> t v r
- t -> s ^ m
- m v r -> ~(t v r)
|- ~p
1. p -> t v r               (Premisse)
2. t -> s ^ m               (Premisse)
3. m v r -> ~(t v r)        (Premisse)
+- 4. p                     (Hypothese pour RAA)
| 5. t v r                 E-> 1,4
| +- 6. t                   (Hypothese)
| | 7. s ^ m               E-> 2,6
| | 8. m                   E^ 7
| | 9. m v r               I v 8
| | 10. ~(t v r)           E-> 3,9
| +-
| +- 11. r                  (Hypothese)
| | 12. m v r              I v 11
| | 13. ~(t v r)           E-> 3,12
| +-
| 14. ~(t v r)             E v 5,6-10,11-13
| 15. (t v r) ^ ~(t v r)   I^ 5,14
+-
16. ~p                     I~ 4-15

 

Logique propositionnelle - Regles d'inference derivees

 

[Exercice 7]
- ~p -> ~q
- q
|- p
1. ~p -> ~q     (Premisse)
2. q           (Premisse)
3. q -> p       CTPS 1 (Contraposition)
4. p           E-> 2,3
[Exercice 8]
- p -> q ^ r
- ~q v ~r
|- ~p
1. p -> q ^ r       (Premisse)
2. ~q v ~r         (Premisse)
3. ~(q ^ r)        DM 2 (De Morgan)
4. ~p              MT 1,3 (Modus Tollens)
[Exercice 9]
- p v q
- t -> ~p
- ~(q v r)
|- ~t
1. p v q           (Premisse)
2. t -> ~p          (Premisse)
3. ~(q v r)        (Premisse)
4. ~q ^ ~r         DM 3
5. ~q              E^ 4
6. p               SD 1,5 (Syllogisme Disjonctif)
7. ~~p             I~~ 6
8. ~t              MT 2,7
[Exercice 10]
- (p v q) -> r v ~(s -> t)
- ~(s v t) ^ ~r
|- ~p ^ ~q
1. (p v q) -> r v ~(s -> t)    (Premisse)
2. ~(s v t) ^ ~r             (Premisse)
3. ~(s v t)                  E^ 2
4. ~r                        E^ 2
5. ~s ^ ~t                   DM 3
6. ~s                        E^ 5
7. ~s v t                    I v 6
8. s -> t                     DEF-> 7
9. ~~(s -> t)                 I~~ 8
10. ~r ^ ~~(s -> t)           I^ 4,9
11. ~(r v ~(s -> t))          DM 10
12. ~(p v q)                 MT 1,11
13. ~p ^ ~q                  DM 12
[Exercice 11]
- p v q <-> r v s
- ~(m ^ ~n)
- w v n
- (r -> t) -> u ^ (w -> m)
- ~(n v ~t)
|- ~p v ~q
1. p v q <-> r v s               (Premisse)
2. ~(m ^ ~n)                   (Premisse)
3. w v n                       (Premisse)
4. (r -> t) -> u ^ (w -> m)       (Premisse)
5. ~(n v ~t)                   (Premisse)
6. ~n ^ t                      DM 5
7. ~n                          E^ 6
8. t                           E^ 6
9. ~m v n                      DM 2
10. ~m                         SD 9,7
11. w                          SD 3,7
12. r -> t                      SIMP.COND 8 (t est vrai)
13. u ^ (w -> m)                E-> 4,12
14. w -> m                      E^ 13
15. m                          E-> 14,11
16. m ^ ~m                     I^ 15,10
17. ~p v ~q                    EFQ 16 (Ex falso quodlibet)
[Exercice 12]
Sans premisses
|- (p ^ q -> r) <-> (p ^ ~r -> ~q)
+- 1. p ^ q -> r            (Hypothese ->)
| +- 2. p ^ ~r             (Hypothese ->)
| | 3. p                  E^ 2
| | 4. ~r                 E^ 2
| | +- 5. q                (Hypothese RAA)
| | | 6. p ^ q            I^ 3,5
| | | 7. r                E-> 1,6
| | | 8. r ^ ~r           I^ 7,4
| | +-
| | 9. ~q                 I~ 5-8
| +-
| 10. p ^ ~r -> ~q         I-> 2-9
+-
+- 11. p ^ ~r -> ~q         (Hypothese <-)
| +- 12. p ^ q             (Hypothese ->)
| | 13. p                 E^ 12
| | 14. q                 E^ 12
| | +- 15. ~r              (Hypothese RAA)
| | | 16. p ^ ~r          I^ 13,15
| | | 17. ~q              E-> 11,16
| | | 18. q ^ ~q          I^ 14,17
| | +-
| | 19. r                 I~ 15-18
| +-
| 20. p ^ q -> r           I-> 12-19
+-
21. (p ^ q -> r) <-> (p ^ ~r -> ~q)   I<-> 1-10,11-20

 

Logique des predicats - Regles d'inference de base

 

[Exercice 13]
- Ax(Px -> Qx)
- Pa
|- ExQx
1. Ax(Px -> Qx)     (Premisse)
2. Pa              (Premisse)
3. Pa -> Qa         EA 1 [x/a]
4. Qa              E-> 2,3
5. ExQx            IE 4
[Exercice 14]
- AxPx ^ AxQx
|- Ax(Px ^ Qx)
1. AxPx ^ AxQx     (Premisse)
2. AxPx            E^ 1
3. AxQx            E^ 1
4. Pa              EA 2 [x/a] (a arbitraire)
5. Qa              EA 3 [x/a]
6. Pa ^ Qa         I^ 4,5
7. Ax(Px ^ Qx)     IA 6
[Exercice 15]
- AxPx v AxQx
|- Ax(Px v Qx)
1. AxPx v AxQx         (Premisse)
+- 2. AxPx              (Hypothese)
| 3. Pa                EA 2 [x/a] (a arbitraire)
| 4. Pa v Qa           I v 3
| 5. Ax(Px v Qx)       IA 4
+-
+- 6. AxQx              (Hypothese)
| 7. Qa                EA 6 [x/a]
| 8. Pa v Qa           I v 7
| 9. Ax(Px v Qx)       IA 8
+-
10. Ax(Px v Qx)        E v 1,2-5,6-9
[Exercice 16]
- AxAyAz((Rxy ^ Ryz) -> Rxz)
- Ax~Rxx
|- AxAy(Rxy -> ~Ryx)
1. AxAyAz((Rxy ^ Ryz) -> Rxz)    (Premisse)
2. Ax~Rxx                        (Premisse)
+- 3. Rab                         (Hypothese, a,b arbitraires)
| +- 4. Rba                       (Hypothese pour RAA)
| | 5. Rab ^ Rba                 I^ 3,4
| | 6. (Rab ^ Rba) -> Raa         EA 1 [x/a,y/b,z/a]
| | 7. Raa                       E-> 5,6
| | 8. ~Raa                      EA 2 [x/a]
| | 9. Raa ^ ~Raa                I^ 7,8
| +-
| 10. ~Rba                       I~ 4-9
+-
11. Rab -> ~Rba                   I-> 3-10
12. AxAy(Rxy -> ~Ryx)             IA 11
[Exercice 17]
- Ax(Px -> Qx)
|- Ax(Ay(Px ^ Ryx) -> Ay(Qx ^ Ryx))
1. Ax(Px -> Qx)                   (Premisse)
+- 2. Ay(Pa ^ Rya)                (Hypothese, a arbitraire)
| 3. Pa ^ Rba                    EA 2 [y/b] (b arbitraire)
| 4. Pa                          E^ 3
| 5. Rba                         E^ 3
| 6. Pa -> Qa                     EA 1 [x/a]
| 7. Qa                          E-> 4,6
| 8. Qa ^ Rba                    I^ 7,5
| 9. Ay(Qa ^ Rya)                IA 8
+-
10. Ay(Pa ^ Rya) -> Ay(Qa ^ Rya)  I-> 2-9
11. Ax(Ay(Px ^ Ryx) -> Ay(Qx ^ Ryx))  IA 10
[Exercice 18]
- Ax(Px -> (Ay(Qy ^ Ryz) <-> ~Sx))
|- Ax((Px ^ Ay~(Qy ^ Ryx)) -> ~Sx)
1. Ax(Px -> (Ay(Qy ^ Ryz) <-> ~Sx))       (Premisse)
+- 2. Pa ^ Ay~(Qy ^ Rya)                (Hypothese, a arbitraire)
| 3. Pa                                 E^ 2
| 4. Ay~(Qy ^ Rya)                      E^ 2
| 5. Pa -> (Ay(Qy ^ Ryz) <-> ~Sa)         EA 1 [x/a]
| 6. Ay(Qy ^ Ryz) <-> ~Sa                E-> 3,5
| 7. ~Ey(Qy ^ Rya)                     DefA/E 4
| 8. ~Ay(Qy ^ Rya)                     (de 7, s'il n'y en a aucun)
| 9. ~Sa                               E<-> 6,8 (biconditionnel)
+-
10. (Pa ^ Ay~(Qy ^ Rya)) -> ~Sa         I-> 2-9
11. Ax((Px ^ Ay~(Qy ^ Ryx)) -> ~Sx)     IA 10

 

Logique des predicats - Regles d'inference derivees

 

[Exercice 19]
- Ax(Px -> Qx)
- Ax(~Sx -> ~Qx)
|- Ax(Px -> Sx v Rx)
1. Ax(Px -> Qx)         (Premisse)
2. Ax(~Sx -> ~Qx)       (Premisse)
+- 3. Pa                (Hypothese, a arbitraire)
| 4. Pa -> Qa           EA 1 [x/a]
| 5. Qa                E-> 3,4
| 6. ~Sa -> ~Qa         EA 2 [x/a]
| 7. Qa -> Sa           CTPS 6 (Contraposition)
| 8. Sa                E-> 5,7
| 9. Sa v Ra           I v 8
+-
10. Pa -> Sa v Ra       I-> 3-9
11. Ax(Px -> Sx v Rx)   IA 10
[Exercice 20]
- AxPx -> AxQx
- ~Qa
|- ~AxPx
1. AxPx -> AxQx     (Premisse)
2. ~Qa             (Premisse)
3. Ex~Qx           IE 2
4. ~AxQx           DefE/A 3
5. ~AxPx           MT 1,4
[Exercice 21]
- Ax(Tx -> Mx)
- Ax~(Mx ^ Rx)
- Ax(Tx -> (Px -> Rx))
|- Ax(Tx -> ~Px)
1. Ax(Tx -> Mx)              (Premisse)
2. Ax~(Mx ^ Rx)             (Premisse)
3. Ax(Tx -> (Px -> Rx))       (Premisse)
+- 4. Ta                     (Hypothese, a arbitraire)
| 5. Ta -> Ma                EA 1 [x/a]
| 6. Ma                     E-> 4,5
| 7. ~(Ma ^ Ra)             EA 2 [x/a]
| 8. ~Ma v ~Ra              DM 7
| 9. ~Ra                    SD 8,6
| 10. Ta -> (Pa -> Ra)        EA 3 [x/a]
| 11. Pa -> Ra               E-> 4,10
| 12. ~Pa                   MT 11,9
+-
13. Ta -> ~Pa                I-> 4-12
14. Ax(Tx -> ~Px)            IA 13
[Exercice 22]
- AxMx
- Ax~Lxx
- ~ExEy(Lxy ^ ~Lxx)
|- ~AxEy~(Mx -> ~Lxy)
1. AxMx                        (Premisse)
2. Ax~Lxx                      (Premisse)
3. ~ExEy(Lxy ^ ~Lxx)           (Premisse)
4. AxAy~(Lxy ^ ~Lxx)           DefE/A 3
5. Ma                          EA 1 [x/a] (a arbitraire)
6. ~Laa                        EA 2 [x/a]
7. ~(Laa ^ ~Laa)               EA 4 [x/a,y/a]
8. Ma -> ~Laa                   I-> (de 5,6)
9. Ax(Mx -> ~Lxx)               IA 8
10. Ey~(Ma -> ~Lay) -> #         (par analyse)
11. ~AxEy~(Mx -> ~Lxy)          I~ (resultat)
[Exercice 23]
- AxAyAz(~(Txy -> Txz) -> ~Qyz)
- AxAyAz(Rya -> Qzx)
- ExEyEz(Txz ^ Txy)
|- ~ExRxa
1. AxAyAz(~(Txy -> Txz) -> ~Qyz)     (Premisse)
2. AxAyAz(Rya -> Qzx)               (Premisse)
3. ExEyEz(Txz ^ Txy)               (Premisse)
+- 4. Tbc ^ Tba                     (Hypothese EE, b,c arbitraires)
| 5. Rba -> Qca                     EA 2 [x/a,y/b,z/c]
| 6. ~(Tbc -> Tba) -> ~Qca           EA 1 [x/b,y/c,z/a]
| 7. Qca -> (Tbc -> Tba)             CTPS 6
| 8. Tbc                           E^ 4
| 9. Tba                           E^ 4
| 10. Tbc -> Tba                    I-> (trivial, les deux vrais)
| +- 11. Rba                        (Hypothese RAA)
| | 12. Qca                        E-> 5,11
| | 13. Tbc -> Tba                  E-> 7,12
| | (nous avons deja 10, coherent)
| +-
| 14. ~Rba                         (par analyse de l'argument)
| 15. Ax~Rxa                       IA 14
+-
16. ~ExRxa                         DefA/E 15
[Exercice 24]
- Ax(~Fa v Qx)
- Ax(Qx ^ Txb -> Rx)
|- Ax~(Qx ^ Rx) -> (Fa v ~Tbb)
1. Ax(~Fa v Qx)              (Premisse)
2. Ax(Qx ^ Txb -> Rx)         (Premisse)
+- 3. Ax~(Qx ^ Rx)            (Hypothese)
| 4. ~Fa v Qb                EA 1 [x/b]
| 5. Qb ^ Tbb -> Rb           EA 2 [x/b]
| 6. ~(Qb ^ Rb)              EA 3 [x/b]
| +- 7. ~Fa                   (Hypothese)
| | 8. Fa v ~Tbb             I v (de ~Fa on peut deriver)
| | ...                      (analyse de cas)
| +-
| 9. Fa v ~Tbb               (resultat)
+-
10. Ax~(Qx ^ Rx) -> (Fa v ~Tbb)   I-> 3-9

 

Logique des predicats avec identite - Regles de base

 

[Exercice 25]
- Ax(Px -> Qx)
- Pa
- b=a
|- Qb
1. Ax(Px -> Qx)     (Premisse)
2. Pa              (Premisse)
3. b=a             (Premisse)
4. Pa -> Qa         EA 1 [x/a]
5. Qa              E-> 2,4
6. Qb              =E 3,5 (Substitution des egaux)
[Exercice 26]
- ExAy(ixPx=x ^ y!=x)
|- Qa
1. ExAy(ixPx=x ^ y!=x)     (Premisse)
+- 2. Ay(ixPx=a ^ y!=a)     (Hypothese EE)
| 3. ixPx=a ^ b!=a         EA 2 [y/b]
| 4. ixPx=a               E^ 3
| 5. P(ixPx)              (Par definition de la description definie)
| 6. Pa                   =E 4,5
| (Nous avons besoin de plus d'informations pour Qa)
+-

Note : Cet exercice necessite des premisses supplementaires pour deriver Qa.

[Exercice 27]
Sans premisses
|- AxAyAz[(x!=y ^ y=z) -> x!=z]
+- 1. a!=b ^ b=c             (Hypothese, a,b,c arbitraires)
| 2. a!=b                   E^ 1
| 3. b=c                   E^ 1
| +- 4. a=c                 (Hypothese RAA)
| | 5. a=b                 =E 3,4 (transit. avec c=b)
| | 6. a!=b ^ a=b           I^ 2,5
| +-
| 7. a!=c                   I~ 4-6
+-
8. (a!=b ^ b=c) -> a!=c       I-> 1-7
9. AxAyAz[(x!=y ^ y=z) -> x!=z]   IA 8
[Exercice 28]
- a=ixPx
- Ax(Qx -> ~Px)
|- P(ixPx)
1. a=ixPx              (Premisse)
2. Ax(Qx -> ~Px)        (Premisse)
3. Pa                  (Par definition : si a=ixPx, alors Pa)
4. P(ixPx)             =E 1,3
[Exercice 29]
- ~ExEy(x!=y)
|- ExPx -> AxPx
1. ~ExEy(x!=y)          (Premisse : il n'y a qu'un seul objet)
2. AxAy(x=y)           Def 1
+- 3. ExPx              (Hypothese)
| +- 4. Pa              (Hypothese EE)
| | 5. a=b             EA 2 [x/a,y/b] (b arbitraire)
| | 6. Pb              =E 5,4
| | 7. AxPx            IA 6
| +-
| 8. AxPx              EE 3,4-7
+-
9. ExPx -> AxPx         I-> 3-8
[Exercice 30]
- Ax(Sx -> Qx)
- Ax(~Px -> ~Qx)
- S(ixPx)
- ~Pa
|- a!=ixPx
1. Ax(Sx -> Qx)         (Premisse)
2. Ax(~Px -> ~Qx)       (Premisse)
3. S(ixPx)             (Premisse)
4. ~Pa                 (Premisse)
5. S(ixPx) -> Q(ixPx)   EA 1 [x/ixPx]
6. Q(ixPx)             E-> 3,5
7. ~Pa -> ~Qa           EA 2 [x/a]
8. ~Qa                 E-> 4,7
+- 9. a=ixPx            (Hypothese RAA)
| 10. Qa               =E 9,6
| 11. Qa ^ ~Qa         I^ 10,8
+-
12. a!=ixPx             I~ 9-11

 

Logique des predicats avec identite - Regles derivees

 

[Exercice 31]
- Ax(x=a -> Qx)
- Ax(Qx -> ~Rx)
|- Ax(Rx -> x!=a)
1. Ax(x=a -> Qx)        (Premisse)
2. Ax(Qx -> ~Rx)        (Premisse)
+- 3. Rb                (Hypothese, b arbitraire)
| 4. b=a -> Qb          EA 1 [x/b]
| 5. Qb -> ~Rb          EA 2 [x/b]
| +- 6. b=a             (Hypothese RAA)
| | 7. Qb              E-> 4,6
| | 8. ~Rb             E-> 5,7
| | 9. Rb ^ ~Rb        I^ 3,8
| +-
| 10. b!=a              I~ 6-9
+-
11. Rb -> b!=a           I-> 3-10
12. Ax(Rx -> x!=a)       IA 11
[Exercice 32]
Sans premisses
|- Ax[Px <-> Ey(y=x ^ Py)]
(Pour a arbitraire)
+- 1. Pa                    (Hypothese ->)
| 2. a=a                   =I (Reflexivite)
| 3. a=a ^ Pa              I^ 2,1
| 4. Ey(y=a ^ Py)          IE 3
+-
+- 5. Ey(y=a ^ Py)          (Hypothese <-)
| +- 6. b=a ^ Pb            (Hypothese EE)
| | 7. b=a                 E^ 6
| | 8. Pb                  E^ 6
| | 9. Pa                  =E 7,8
| +-
| 10. Pa                   EE 5,6-9
+-
11. Pa <-> Ey(y=a ^ Py)      I<-> 1-4,5-10
12. Ax[Px <-> Ey(y=x ^ Py)]  IA 11
[Exercice 33]
Sans premisses
|- AxAyAz[x!=y ^ y=z -> x!=z]
(Identique a l'exercice 27)
+- 1. a!=b ^ b=c             (Hypothese)
| 2. a!=b                   E^ 1
| 3. b=c                   E^ 1
| +- 4. a=c                 (Hypothese RAA)
| | 5. c=b                 SIM 3
| | 6. a=b                 TRANS 4,5
| | 7. #                   I^ 2,6
| +-
| 8. a!=c                   I~ 4-7
+-
9. (a!=b ^ b=c) -> a!=c       I-> 1-8
10. AxAyAz[x!=y ^ y=z -> x!=z]  IA 9
[Exercice 34]
- ExPx ^ AxAy(Px ^ Py -> x=y)
|- ~ExEy[x!=y ^ Az(Pz <-> x=z v y=z)]
1. ExPx ^ AxAy(Px ^ Py -> x=y)    (Premisse : il existe exactement un P)
2. ExPx                           E^ 1
3. AxAy(Px ^ Py -> x=y)            E^ 1
+- 4. ExEy[x!=y ^ Az(Pz <-> x=z v y=z)]  (Hypothese RAA)
| +- 5. a!=b ^ Az(Pz <-> a=z v b=z)      (Hypothese EE)
| | 6. a!=b                           E^ 5
| | 7. Az(Pz <-> a=z v b=z)            E^ 5
| | 8. Pa <-> a=a v b=a                EA 7 [z/a]
| | 9. a=a                           =I
| | 10. a=a v b=a                    I v 9
| | 11. Pa                           E<-> 8,10
| | 12. Pb <-> a=b v b=b               EA 7 [z/b]
| | 13. b=b                          =I
| | 14. a=b v b=b                    I v 13
| | 15. Pb                           E<-> 12,14
| | 16. Pa ^ Pb                      I^ 11,15
| | 17. Pa ^ Pb -> a=b                EA 3 [x/a,y/b]
| | 18. a=b                          E-> 16,17
| | 19. a!=b ^ a=b                    I^ 6,18
| +-
| 20. #                              EE 4,5-19
+-
21. ~ExEy[x!=y ^ Az(Pz <-> x=z v y=z)]  I~ 4-20
[Exercice 35]
Sans premisses
|- ExPx ^ AxAy(Px ^ Py -> x=y) <-> ExAy(Py <-> x=y)
(->) Supposons ExPx ^ AxAy(Px ^ Py -> x=y)
Soit Pa (par EE). Pour tout b :
- Si Pb, alors Pa ^ Pb, donc a=b
- Si a=b, alors Pb (par Pa et substitution)
Ainsi : Ay(Py <-> a=y)
Par consequent : ExAy(Py <-> x=y)

(<-) Supposons ExAy(Py <-> x=y)
Soit Ay(Py <-> a=y) (par EE)
- Pa <-> a=a, et a=a est vrai, donc Pa. Ainsi ExPx.
- Si Pb ^ Pc, alors a=b et a=c, donc b=c.
Par consequent : ExPx ^ AxAy(Px ^ Py -> x=y)
[Exercice 36]
Sans premisses
|- ExEy(x!=y) <-> AxEy(x!=y)
(->) Supposons ExEy(x!=y)
Soient a,b tels que a!=b.
Pour tout c :
- Si c=a, alors c!=b (car a!=b)
- Si c!=a, alors c!=a
Ainsi : AxEy(x!=y)

(<-) Supposons AxEy(x!=y)
En particulier, pour un certain a : Ey(a!=y)
Soit b tel que a!=b.
Alors ExEy(x!=y) (en prenant x=a, y=b)