Scribd
Importer
115 vues11 pages

Logique Propositionnelle: Calcul des Séquents

Le document décrit le calcul des séquents, une méthode de preuve logique introduite par Gentzen. Il présente les règles d'inférence structurelles et propositionnelles du calcul des séquents ainsi qu'un théorème sur l'élimination des coupures.

Transféré par

Na Ha
Copyright
© © All Rights Reserved
Nous prenons très au sérieux les droits relatifs au contenu. Si vous pensez qu’il s’agit de votre contenu, signalez une atteinte au droit d’auteur ici.
Formats disponibles
Téléchargez aux formats PPTX, PDF, TXT ou lisez en ligne sur Scribd
115 vues11 pages

Logique Propositionnelle: Calcul des Séquents

Le document décrit le calcul des séquents, une méthode de preuve logique introduite par Gentzen. Il présente les règles d'inférence structurelles et propositionnelles du calcul des séquents ainsi qu'un théorème sur l'élimination des coupures.

Transféré par

Na Ha
Copyright
© © All Rights Reserved
Nous prenons très au sérieux les droits relatifs au contenu. Si vous pensez qu’il s’agit de votre contenu, signalez une atteinte au droit d’auteur ici.
Formats disponibles
Téléchargez aux formats PPTX, PDF, TXT ou lisez en ligne sur Scribd

LOGIQUE MATHÉMATIQUE

CHAPITRE 1: LOGIQUE PROPOSITIONNELLE

L 2 I N F O R M AT I Q U E
LE CALCUL DES SÉQUENTS

• Méthode de preuve introduite par Gerhard Gentzen en


1934.
• Séquent : suit, suivent,
• Preuve sous forme d’arbre de bas en haut.
LE CALCUL DES SÉQUENTS

• Soit Σ une signature dont V est l’ensemble des variables.


Soient Γ,Δ,Λ et Π quatre ensembles de Σ-formules. Soient φ,ψ
deux Σ-formules. Soient x et y deux variables de V. Soient t, t1
et t2 des termes de TΣ(V). On considère l’ensemble des règles
d’inférence suivants :
LE CALCUL DES SÉQUENTS

• Règles structurelles :
affaiblissement
𝜞⊢𝜟 𝒃⊢𝒄
* * 𝜞⊢𝜟
𝒃⊢𝒄
𝝋,𝜞 ⊢𝜟 𝒂, 𝒃 ⊢ 𝒄 𝒃 ⊢ 𝒂, 𝒄 𝜞 ⊢ 𝜟 ,𝝋
diminution
𝝋 ,𝝋 , 𝜞 ⊢ 𝜟 𝒂 , 𝒃⊢ 𝒄 𝜞 ⊢ 𝜟 ,𝝋 ,𝝋
𝒃⊢ 𝒂, 𝒄
𝝋,𝜞⊢𝜟 𝒂, 𝒂, 𝒃 ⊢𝒄 𝜞 ⊢ 𝜟,𝝋
𝒃⊢ 𝒂, 𝒂, 𝒄
échange
𝜞 ,𝝋 ,𝝍 , 𝜦⊢ 𝜟 𝒃, 𝒂, 𝒄 ⊢ 𝒅 𝒄 ⊢ 𝒃 ,𝒂, 𝒅 𝜞 ⊢ 𝜦,𝝋 ,𝝍 , 𝜟
𝜞 ,𝝍 ,𝝋 , 𝜦⊢ 𝜟 𝒂, 𝒃, 𝒄 ⊢ 𝒅 𝒄 ⊢ 𝒂, 𝒃, 𝒅 𝜞 ⊢ 𝜦,𝝍 ,𝝋 , 𝜟
coupure 𝜞 ⊢ 𝜟 ,𝝋 𝝋 , 𝜦⊢ 𝜫 𝒂⊢ 𝒃,𝒆𝒆,𝒄 ⊢ 𝒅
𝜞 , 𝜦⊢ 𝜟, 𝜫 𝒂,𝒄 ⊢ 𝒃,𝒅
LE CALCUL DES SÉQUENTS

• Règles propositionnelles :
conjonction
𝜞 ,𝝋 , 𝝍 ⊢ 𝜟 𝒂 , 𝒃 ⊢ 𝒄 * *𝒂⊢ 𝒃 , 𝒄 𝒂⊢ 𝒃 , 𝒅 𝜞 ⊢ 𝜟 ,𝝋 𝜞 ⊢ 𝜟, 𝝍
𝜞 ,𝝋 ∧𝝍 ⊢ 𝜟 𝒂∧ 𝒃 ⊢𝒄 𝒂⊢ 𝒃 , 𝒄 ∧ 𝒅 𝜞 ⊢ 𝜟, 𝝋 ∧𝝍
disjonction
𝜞 ,𝝋 ⊢ 𝜟 𝜞 , 𝝍 ⊢ 𝜟 𝒂, 𝒃 ⊢ 𝒅 𝒂, 𝒄 ⊢ 𝒅 𝒂⊢ 𝒃 , 𝒄 𝜞 ⊢ 𝜟 ,𝝋 ,𝝍
𝜞 , 𝝋 ∨𝝍 ⊢ 𝜟 𝒂 , 𝒃∨ 𝒄 ⊢ 𝒅 𝒂⊢(𝒃 ∨ 𝒄) 𝜞 ⊢ 𝜟 ,(𝝋 ∨𝝍 )
négation
𝜞 ⊢ 𝜟 ,𝝋 ⊢ 𝒂,𝒃 𝒃⊢ 𝒂 𝜞 ,𝝋 ⊢ 𝜟
𝜞 ,¬ 𝝋⊢ 𝜟 ¬ 𝒂⊢ 𝒃 ⊢ 𝒂 ,¬ 𝒃 𝜞 ⊢ 𝜟 ,¬ 𝝋
implication
𝜞 ⊢ 𝜟 ,𝝋 𝜞 , 𝝍 ⊢ 𝜟 𝒂 ⊢ 𝒅 , 𝒃 𝒂, 𝒄 ⊢ 𝒅 𝒂⊢ 𝒃 𝜞 , 𝝋⊢ 𝜟 ,𝝍
𝜞 ,(𝝋 →𝝍 )⊢ 𝜟 𝒂 ,(𝒃 → 𝒄)⊢ 𝒅 ⊢(𝒂 → 𝒃) 𝜞 ⊢ 𝜟 ,(𝝋 →𝝍 )
LE CALCUL DES SÉQUENTS

• Un axiome

𝝋 ⊢𝝋 aa
LE CALCUL DES SÉQUENTS

• Théorème : (Élimination de coupures) Si ∆ ├ Γ est dérivable


dans le système G, alors il existe une dérivation de ∆ ├ Γ dans
G qui n'utilise pas la règle de coupure.
LE CALCUL DES SÉQUENTS
LE CALCUL DES SÉQUENTS

• Théorème : Le système G est correct, i.e., si ∆ ├G Γ, alors ∆ ├


Γ est valide.
LE CALCUL DES SÉQUENTS

• Exemple: ├(¬B→¬A)→ (A→B)

ax ax
A├A B├B
├ af ├ af
A├A,B B,A├B
¬├ ¬├
¬A, A├B A├¬B,B
→├
(¬B→¬A), A├B
├→
(¬B→¬A)├ (A→B)
├→
├(¬B→¬A)→ (A→B)
LE CALCUL DES SÉQUENTS

• Exercice:
i. a├ (b → a)
ii. (a→(b→c)) →((a→b)→(a→c))
iii. a →(b → c) ├ b →(a → c)
iv. (a →b), ¬b ├ ¬a

Vous aimerez peut-être aussi