Page 22 - MATINF Nr. 4

22 D. Constantin, A.F. S , tefan

2 Sistemul de inferent , ˘a s , i deduct , ie logic˘a Gentzen

Definit , ia 4. Se numes , te secvent o pereche de mult ,imi (H, Γ) de formule ˆın care apar numai
conectivele logice din mult ,imea L \ {↔} . Prima component˘a a perechii se numes , te antecedent,
respectiv, cea de a doua component˘a se numes , te succedent. Convent ,ional secventul (H, Γ) se
reprezint˘a prin H =⇒ Γ. Demonstrarea logic˘a a unui secvent de forma (H, Γ) are semnificat ,ia
c˘a avem mult ,imea de formulele logice din H demostrabil˘a pe baza formulelor logice din mult ,imea
Γ.

Observat ,ia 5. Se va pune ˆın evident , ˘a un algoritm de verificare a deduct , iei logice a mult , imii de
formule logice H pe baza informat , iilor redate de formulele logice din mult , imea Γ prin utilizarea
unui set de reguli de inferent , ˘a logic˘a specifice sistemului de deduct , ie natural˘a Gentzen.
Observat ,ia 6. Pentru conectiva logic˘a de echivalent , ˘a se utilizeaz˘a exprimarea semantic echivalent˘a
la nivel logic prin care o formul˘a logic˘a de forma (β ↔ γ) se substituie cu ((β → γ) ∧ (γ → β)),
adic˘a avem: (β ↔ γ) ≡ ((β → γ) ∧ (γ → β)).
Definit , ia 5. Secventul H =⇒ Γ este secvent axiom˘a dac˘a H ∩ Γ 6= Ø.

Definit , ia 6. Secventul H =⇒ Γ este secvent ˆıncheiat dac˘a mult ,imile componente cont ,in numai
propozit ,ii elementare; H ∪ Γ ⊂ V .

2.1 Regulile de inferent , ˘a Gentzen

Definit , ia 7. Regulile de inferent ,˘a Gentzen sunt:
H=⇒Γ∪{α}
G1. ( regula negat , iei la stˆanga);
H∪{(¬α)}=⇒Γ
G2. H∪{α,β}=⇒Γ ( regula conjunct , iei la stˆanga);
H∪{(α∧β)}=⇒Γ
G3. H∪{α}=⇒Γ, H∪{β}=⇒Γ ( regula disjunct , iei la stˆanga);
H∪{(α∨β)}=⇒Γ
G4. H∪{β}=⇒Γ, H=⇒Γ∪{α} ( regula implicat , iei la stˆanga);
H∪{(α→β)}=⇒Γ
H∪{α}=⇒Γ
G5. ( regula negat , iei la dreapta);
H=⇒Γ∪{(¬α)}
H=⇒Γ∪{α}, H=⇒Γ∪{β}
G6. ( regula conjunct , iei la dreapta);
H=⇒Γ∪{(α∧β)}
G7. H=⇒Γ∪{α,β} ( regula disjunct , iei la dreapta);
H=⇒Γ∪{(α∨β)}
G8. H∪{α}=⇒Γ∪{β} ( regula implicat , iei la dreapta).
H=⇒Γ∪{(α→β)}
unde H, Γ sunt mult ,imi arbitrare de formule; α, β ∈ FORM.

Observat ,ia 7. Regulile Gentzen definesc modalit˘at , ile de descompunere ˆın formule de adˆancime
mai mic˘a, a formulelor selectate din mult , imile antecedent/succedent. Se observ˘a c˘a pentru
o formul˘a selectat˘a, regula Gentzen aplicabil˘a exist˘a ¸si este unic˘a s , i anume este definit˘a
de conectiva principal˘a corespunz˘atoare formulei s , i de provenient , a ei (antecedent respectiv
succedent). Regulile G1, G2, G5, G7 s , i G8 vor fi referite ca reguli de tipul 1, respectiv regulile
G3, G4 s , i G6 sunt reguli de tipul 2.
Exemplul 5. Presupunem c˘a formula selectat˘a este

θ = (((α → β) ∨ ((¬α) → γ)) → (β ∨ γ))
s , i S = H ∪ {θ} =⇒ Γ. Atunci regula Gentzen aplicabil˘a este G4 s , i rezult˘a S 1 ,S 2 unde
S
S 1 = H ∪ {(β ∨ γ)} =⇒ Γ, S 2 = H =⇒ Γ ∪ {((α → β) ∨ ((¬α) → γ))} .