Adaptez les exercices résolus à votre matière. Inscrivez-vous gratuitement
Règles d'inférence
| Légende | |
|---|---|
| α, β, γ | Ce sont des formules bien formées. |
| ψ | C'est un prédicat (P, Q, R...) |
| c, c´, c´´... | C'est une constante d'individu (a, b, c...) |
| v, v´, v´´ | C'est une variable d'individu (x, y, z...) |
RÈGLES DE BASE
| B | ^ | v | → | ↔ | ¬ | ∀ | ∃ | = | ι |
|---|---|---|---|---|---|---|---|---|---|
| (I) |
α β -- α ∧ β
|
α --- αVβ |
┌α |... ┗β --- α→β |
α→β β→α --- α↔β |
┌ ¬α |......... ┗β∧¬β ----- α
|
α --- ∀vα |
α --- ∃vα |
ψϲ -- ∀v(v=ϲ →ψv) |
ψ(ιvα) --- ∃v∀v´ ( α ↔ x=y) |
| (E) |
α ∧ β -- α β
|
┌α |... ┗ γ ┌β |... ┗ γ --- γ |
α→β α --- β |
α↔β ---- α→β β→α |
¬¬α ---- α |
∀vα --- α
|
∃vα --- α |
∀v(v=ϲ →ψv) -- ψϲ |
∃v∀v´ ( Φ ↔ x=y) --- ψ(ιvΦ) |
RÈGLES DÉRIVÉES
Règles dérivées de l'implication
| RÈGLES | → |
|---|---|
| Transitive du conditionnel (Tr→) | α→β β→γ ---- α→γ |
| Modus Tollens (MT) | α→β ¬β ---- ¬α |
| Dilemmes (Dil) | Dil1 α ∨ β α→γ β→γ ---- γ
Dil2 ¬α ∨ ¬β γ→α γ→β ---- ¬γ |
| Chargement de prémisses (CrPr) | β ---- α→β |
| Contraposition (Ctrp) | α→β ---- ¬β→¬α |
| Mutation du conditionnel (Mut →) | α→(β→γ) ---- β→(α→γ) |
| Importation/Exportation(Imp/Exp) | α→(β→γ) ---- α^β→γ |
| Monotonie (Mon) | α→β ---- α ∧ γ→β |
Règles dérivées de la conjonction / disjonction
| RÈGLES | ^ | v |
|---|---|---|
| Syllogisme Disjonctif (SD) | α ∨ β ¬α ---- β
α ∨ β ¬β ---- α |
|
| Idempotence (Idp ∧ / Idp v) | α ∧ α ----- α |
α ∨ α ---- α |
| Absorption (Absc ^/Absc v) | α ∧ (α ∨ β) ---- α |
α ∨ (α ∧ β) ---- α |
| Commutative (Comm ^) | α ∧ β ---- β ∧ α |
α ∨ β ---- β ∨ α |
| Associative (Assoc ^/Assoc v) | (α ∧ β) ∧ γ ---- α ∧ (β ∧ γ) |
(α ∨ β) ∨ γ ---- α ∨ (β ∨ γ) |
| Distributive (Dist ^/Dist v) | α ∧ (β ∨ γ) ---- (α ∧ β) ∨ (α ∧ γ) |
α ∨ (β ∧ γ) ---- (α ∨ β) ∧ (α ∨ γ) |
Règles dérivées des quantificateurs
| RÈGLES | ∀ | ∃ | ||
|---|---|---|---|---|
| Négation du Quantificateur Universel ou Existentiel (Nég Univ ou Nég Exist) | ¬∀vα ---- ∃v¬α |
¬∃vα ---- ∀v¬α |
||
| Descente du quantificateur (Desc Quant) | ∀vα ---- ∃vα |
---- | ||
| Mutation de variable (Mut Var) | ∀vα ---- ∀v´α |
∃vα ---- ∃v´α |
||
| Contraction du Quantificateur Universel ou Existentiel (Contrac Univ Disj ou Contrac Exist Cond) | ∀vα ∨ ∀vβ ---- ∀v(α ∨ β) |
∃vα → ∃vβ ---- ∃v(α → β) |
||
Permutations des quantificateurs universels (Perm Univ) |
∀v∀v´α ----- ∀v´∀vα |
∃v∃v´α ----- ∃v´∃vα |
||
∃v∀v´α ----- ∀v´∃vα |
||||
| Distributive du Quantificateur Universel ou Existentiel en conjonction (Dist Univ ∧ / Dist Exist ^) | ∀v(α ∧ β) ---- ---- ∀vα ∧ ∀vβ |
∃v(α ∧ β)
---- ∃vα ∧ ∃vβ |
||
| Distributive du Quantificateur Existentiel en disjonction (Dist Exist v) | ---- | ∃v(α ∨ β) ---- ---- ∃vα ∨ ∃vβ |
||
| Distribution du Quantificateur Universel et Existentiel en conditionnel (Dist Univ →/Dist Exist →) | ∀v(α→β) ----
∀vα→∀vβ |
∃v(α→β) ---- ---- ∀vα→∃vβ |
||
| Distribution du Quantificateur Universel en Biconditionnel (Dist Univ ↔) | ∀v(α↔β)
----
∀vα↔∀vβ |
|||
Distribution Conditionnée du quantificateur universel pour conjonction, disjonction, antécédent et conséquent. (Dist Univ ^/v/Antéc/Conséq) |
α ∧ ∀vβ ---- ∀v(α ^β) |
α ∨ ∀vβ ---- ∀v(α vβ) |
∀vβ → α --- ∃v(β →α) |
α→∀vβ ---- ∀v(α→β) |
Distribution Conditionnée du quantificateur existentiel pour conjonction, disjonction, antécédent et conséquent. (Dist Exist) ^/v/Antéc/Conséq) |
α ∧ ∃vβ ---- ∃v(α ^β) |
α ∨ ∃vβ ---- ∃v(α vβ) |
∃vβ → α --- ∀v(β →α) |
α→∃vβ ---- ∃v(α→β) |
Règles dérivées de l'identité
| RÈGLES | = |
|---|---|
| Leibniz1 | c=c' ψc ---- ψc' |
| Leibniz2 | c=c' ψc´ ---- ψc
|
| Leibniz3 | ψc ¬ψc´ ---- c≠c´ |
| Leibniz4 | ¬ψc ψc´ ---- c≠c´ |
| Réflexive de l'identité (Réfl =) | ---- c=c' |
| Symétrique de l'identité (Sym =) | c = c´ ---- c´= c |
| Transitive de l'identité (Tr =) | c=c' c´=c´´ ---- c = c´´ |
| Indiscernabilité (Indiscern) | c=c' ---- ψc↔ψc´ |
| Euclide | c=c' ---- fc=fc´ |
Règles de définition
| RÈGLES | Connecteur 1 | Connecteur 2 |
|---|---|---|
| DM ^/v v/v | ¬(α ∧ β) ---- ¬α ∨ ¬ β |
¬(α ∨ β) ---- ¬α ∧ ¬ β |
| Définition ^/v v/^ | α ∧ β ---- ¬(¬α ∨ ¬ β) |
α ∨ β ---- ¬(¬α ∧ ¬ β) |
| Définition ^/→ v/→ | α ∧ β ---- ¬(α → ¬ β) |
α ∨ β ---- ¬α → β |
| Définition ∃/∀ ∀/∃ | ∀vα ---- ¬∃v¬α |
∃vα ---- ¬∀v¬α |
Retourner aux exercices de déduction naturelle
S'il vous plaît, laissez votre avis sur les exercices de la page web afin que je puisse les améliorer ou les compléter. Merci beaucoup à tous ! < <
Commentaires, suggestions et critiques