Page 23 - MATINF Nr. 4

Elemente computat , ionale de deduct , ie logic˘a 23

Pentru

S = H =⇒ Γ ∪ {θ} ,

dac˘a θ este formula selectat˘a, atunci regula Gentzen aplicabil˘a este G8 s , i rezult˘a

S 1
S

unde
S 1 = H ∪ {((α → β) ∨ ((¬α) → γ))} =⇒ Γ ∪ {(β ∨ γ)}

Definit , ia 8. Arborele T = (V (T) , E (T)) binar, cu r˘ad˘acina s , i vˆarfurile etichetate cu secvent ,i
este un arbore de deduct ,ie, dac˘a pentru orice n ∈ V (T) , not˘and cu ϕ (n) secventul etichet˘a
corespunz˘ator vˆarfului n, avem:

(i) dac˘a od (n) = 1 s , i n 1 este unicul succesor al lui n atunci ϕ(n 1 ) este regul˘a Gentzen;
ϕ(n)
(ii) dac˘a od (n) = 2 s , i n 1 , n 2 sunt succesorii vˆarfului n atunci ϕ(n 1 ), ϕ(n 2 ) este regul˘a Gentzen.
ϕ(n)

Definit , ia 9. Arborele de deduct ,ie T este un arbore de demonstrat ,ie pentru secventul etichet˘a a
vˆarfului r˘ad˘acin˘a dac˘a orice vˆarf terminal are ca etichet˘a un secvent axiom˘a.

Definit , ia 10. Arborele de deduct ,ie T este un arbore ˆıncheiat dac˘a toate vˆarfurile terminale au
etichete secvent ,i ˆıncheiat ,i.

Definit , ia 11. Arborele de deduct ,ie T este un arbore contraexemplu dac˘a exist˘a n ∈ V (T) astfel
ˆıncˆat ϕ (n) este secvent ˆıncheiat s , i nu este secvent axiom˘a.

Definit , ia 12. Secventul S este demonstrabil, notat ` S, dac˘a exist˘a T arbore de demonstrat ,ie
cu r eticheta r˘ad˘acinii.

Exemplul 6. Fie secventul S = {(α → β) , ((¬α) → γ)} =⇒ {(β ∨ γ)} .

Arborele T reprezentat ˆın figura urm˘atoare este un arbore de deduct , ie cu r eticheta rad˘acinii.
Deoarece vˆarfurile terminale sunt n 5 , n 7 , n 10 , n 11 s , i au etichetele secvent , i axiom˘a rezult˘a ` S.

n 7
↑

n 5 n 6 n 10 n 11
↑ ↑ ↑ ↑
n 3 n 4 n 8 n 9
-% -%

n 1 n 2
-%
r

Fig. 1