CM1

Question 1

LJ ax

Answer 1

________
Γ, A ⊢ A

Question 2

LK ax

Answer 2

________
Γ, A ⊢ Δ, A

Question 3

LJ cont

Answer 3

Γ, A, A ⊢ Δ
____________
Γ, A ⊢ Δ

Question 4

LK cont_right

Answer 4

Γ ⊢ Δ, A, A
____________
Γ ⊢ Δ, A

Question 5

LK cont_left

Answer 5

Γ, A, A ⊢ Δ
____________
Γ, A ⊢ Δ

Question 6

LJ ⊤_right

Answer 6

_______
Γ ⊢ ⊤

Question 7

LK ⊤_right

Answer 7

_______
Γ ⊢ Δ, ⊤

Question 8

LJ ⊥_left

Answer 8

_________
Γ, ⊥ ⊢ Δ

Question 9

LK ⊥_left

Answer 9

_________
Γ, ⊥ ⊢ Δ

Question 10

LJ ¬_right

Answer 10

Γ, A ⊢
________
Γ ⊢ ¬A

Question 11

LK ¬_right

Answer 11

Γ, A ⊢ Δ
________
Γ ⊢ Δ, ¬A

Question 12

LJ ¬_left

Answer 12

Γ ⊢ A
__________
Γ, ¬A ⊢ Δ

Question 13

LK ¬_left

Answer 13

Γ ⊢ A, Δ
__________
Γ, ¬A ⊢ Δ

Question 14

LJ ∧_right

Answer 14

Γ ⊢ A | Γ ⊢ B
________________
Γ ⊢ A ∧ B

Question 15

LK ∧_right

Answer 15

Γ ⊢ Δ, A | Γ ⊢ Δ, B
________________
Γ ⊢ Δ, A ∧ B

Question 16

LJ ∧_left

Answer 16

Γ, A, B ⊢ Δ
_______________
Γ, A ∧ B ⊢ Δ

Question 17

LK ∧_left

Answer 17

Γ, A, B ⊢ Δ
_______________
Γ, A ∧ B ⊢ Δ

Question 18

LJ ∨_right1

Answer 18

Γ ⊢ A
___________
Γ ⊢ A ∨ B

Question 19

LJ ∨_right2

Answer 19

Γ ⊢ B
___________
Γ ⊢ A ∨ B

Question 20

LK ∨_right

Answer 20

Γ ⊢Δ, A
___________
Γ ⊢ Δ, A ∨ B

Question 21

LJ ∨_left

Answer 21

Γ, A ⊢ Δ | Γ, B ⊢ Δ
______________________
Γ, A ∨ B ⊢ Δ

Question 22

LK ∨_left

Answer 22

Γ, A ⊢ Δ | Γ, B ⊢ Δ
______________________
Γ, A ∨ B ⊢ Δ

Question 23

LJ ⇒_right

Answer 23

Γ, A ⊢ B
___________
Γ ⊢ A ⇒ B

Question 24

LK ⇒_right

Answer 24

Γ, A ⊢ Δ, B
_____________
Γ ⊢ Δ, A ⇒ B

Question 25

LJ ⇒_left

Answer 25

Γ ⊢ A | Γ, B ⊢ Δ ___________________ Γ, A ⇒ B ⊢ Δ

Question 26

LK ⇒_left

Answer 26

Γ ⊢ Δ, A | Γ, B ⊢ Δ ___________________ Γ, A ⇒ B ⊢ Δ

Question 27

LJ ⇔_right

Answer 27

Γ, A ⊢ B | Γ, B ⊢ A _____________________ Γ ⊢ A ⇔ B

Question 28

LK ⇔_right

Answer 28

Γ, A ⊢ Δ, B | Γ, B ⊢ Δ, A _________________________ Γ ⊢ Δ, A ⇔ B

Question 29

LJ ⇔_left1

Answer 29

Γ ⊢ A | Γ, B ⊢ Δ __________________ Γ, A ⇔ B ⊢ Δ

Question 30

LJ ⇔_left2

Answer 30

Γ ⊢ B | Γ, A ⊢ Δ __________________ Γ, A ⇔ B ⊢ Δ

Question 31

LK ⇔_left

Answer 31

Γ ⊢ Δ, A, B | Γ, A, B ⊢ Δ _________________________ Γ, A ⇔ B ⊢ Δ

Question 32

LJ ∀_right, x !∈ Γ

Answer 32

Γ ⊢ A(x) _____________ Γ ⊢ ∀x. A(x)

Question 33

LK ∀_right, x !∈ Γ, Δ

Answer 33

Γ ⊢ Δ, A(x) _____________ Γ ⊢ Δ, ∀x. A(x)

Question 34

LJ ∀_left

Answer 34

Γ, A(t) ⊢ Δ _______________ Γ, ∀x. A(x) ⊢ Δ

Question 35

LK ∀_left

Answer 35

Γ, A(t) ⊢ Δ _______________ Γ, ∀x. A(x) ⊢ Δ

Question 36

LJ ∃_right

Answer 36

Γ ⊢ A(t) ____________ Γ ⊢ ∃x. A(x)

Question 37

LK ∃_right

Answer 37

Γ ⊢ Δ, A(t) ____________ Γ ⊢ Δ, ∃x. A(x)

Question 38

LJ ∃_left, x !∈Γ, Δ

Answer 38

Γ, A(x) ⊢ Δ _______________ Γ, ∃x. A(x) ⊢ Δ

Question 39

LK ∃_left, x !∈Γ, Δ

Answer 39

Γ, A(x) ⊢ Δ _______________ Γ, ∃x. A(x) ⊢ Δ

Question 40

LJ cut

Answer 40

Γ ⊢ A | Γ, A ⊢ B _________________ Γ ⊢ B

Question 41

LK cut

Answer 41

Γ ⊢ Δ, A | Γ, A ⊢ Δ, B _________________ Γ ⊢ Δ, B

Question 42

LJ_em em

Answer 42

Γ ⊢ ¬¬A _________ Γ ⊢ A

Question 43

Quelles priorité appliquer sur les règles ?

Answer 43

Appliquer d'abord les opérateurs qui ne branches pas et les quantificateurs qui skolémisent

Question 44

Théorème de Herbrand

Answer 44

En logique classique, ∃x.P(x) ≡ il existe n termes t₁, t₂, . . ., t_n tels que P(t₁) ∨ P(t₂) ∨ . . . ∨ P(t_n) est vraie