Здравейте,
Гледам теоремата за генерализация и едната и посока (правата) ми се струва малко странна.
Ако Γ = { ∀x(p(x)), p(x) }, то Γ ⊢ ∀x(p(x)), според теоремата може да се покаже, че Γ ⊢ p(x) и x ∉ FV[Γ], като последното не е вярно, защото x ∈ FV(p(x)).
Може би клаузата x ∉ FV[Γ] трябва да е предпоставка и в двете посоки, а еквивалентността да е само между Γ ⊢ ∀x(p(x)) и Γ ⊢ p(x)?