xn) jest wolny dla zmiennej y w formule φ, je´sli ˙zadne wyst¸epowanie wolne zmiennej y w φ nie znajduje si¸e w dziedzinie kwantyfikatora ∀xi dla xi wyst¸epuj¸acej w t

Logika A

4. SYSTEM DOWODZENIA LOGIKI PIERWSZEGO RZE¸ DU

M´owimy, ˙ze term t(x₁, ..., x_n) jest wolny dla zmiennej y w formule φ, je´sli ˙zadne wyst¸epowanie wolne zmiennej y w φ nie znajduje si¸e w dziedzinie kwantyfikatora ∀xi

dla x_i wyst¸epuj¸acej w t.

W poni˙zszych aksjomatach (zgodnie z uwag¸a 2.3 listy 2) sp´ojniki logiczne ∧ i ∨ s¸a rozwa˙zane jako skr´oty:

φ ∨ ψ = ¬φ → ψ φ ∧ ψ = ¬(φ → ¬ψ).

Sta la logiczna 1 b¸edzie zast¸epowa la φ → φ, a sta la 0 jest ¬1.

4.1. Aksjomaty logiczne (ni˙zej φ, ψ i θ s¸a dowolnymi formu lami logiki pier- wszego rz¸edu).

(A1) φ → (ψ → φ) ;

(A2) (φ → (ψ → θ)) → ((φ → ψ) → (φ → θ));

(A3) (¬φ → ¬ψ) → (ψ → φ) ;

(A4) ∀xφ → (φ)^x_t, gdzie t jest wolny dla x w φ ; (A5) (φ)^x_t → ∃xφ, gdzie t jest wolny dla x w φ ;

(A6) ∀x(φ → ψ) → (φ → ∀xψ), gdzie x nie jest wolna w φ.

(A7) ∀x(φ → ψ) → (∃xφ → ψ), gdzie x nie jest wolna w ψ.

4.2. Aksjomaty r´owno´sci.

(A8) ∀x(x = x) ; ∀x∀y((x = y) → (y = x)) ;

∀x∀y∀z((x = y) ∧ (y = z) → (x = z));

(A9) ∀x₀, x₁, ..., x_n((x₀ = x_j) ∧ P (x₁, ..., x_j, ..., x_n) → P (x₁, ..., x₀, ..., x_n)), gdzie P jest symbolem relacyjnym j¸ezyka L;

(A10) ∀x₀, x₁, ..., x_n((x₀ = x_j) → (t(x₁, ..., x_j, ..., x_n) = t(x₁, ..., x₀, ..., x_n))), gdzie t jest termem j¸ezyka L.

4.3. Regu ly dowodzenia.

( Modus Ponens ) φ , (φ → ψ) ψ ( Uog´olnienie: Gen) φ(x)

∀xφ(x)

Niech Γ b¸edzie zbiorem formu l j¸ezyka L. Niech φ b¸edzie pewn¸a formu l¸a (tego samego typu). Dowodem formu ly φ ze zbioru Γ nazywamy taki ci¸ag formu l φ1, ..., φk,

˙ze φ_k = φ i ka˙zda φ_i albo jest aksjomatem, albo nale˙zy do Γ, albo te˙z zosta la otrzy- mana z formu l wyst¸epuj¸acych przed φ_iw wyniku zastosowania regu ly (MP) lub (Gen).

W tym przypadku m´owimy, ˙ze φ jest wyprowadzalna (lub posiada dow´od) z Γ, co oznaczamy

Γ ` φ ( gdy Γ jest zbiorem pustym piszemy ` φ ) .

1

4.4. W lasno´sci dowodzenia.

(a) Γ ∪ {φ} ` φ;

(b) Je´sli Γ ` φ, to Γ ∪ {ψ} ` φ;

(c) Je´sli Γ ` φ i Γ ∪ {φ} ` ψ, to Γ ` ψ;

(d) Je´sli Γ ` φ<sub>1</sub>, ..., Γ ` φ_n i {φ₁, ..., φ_n} ` φ, to Γ ` φ.

4.5. Twierdzenie o dedukcji. Je´sli Γ ∪ {φ} ` ψ i istnieje odpowiedni dow´od, w kt´orym, przy ka˙zdym zastosowaniu regu ly (Gen) do formu ly <sup>1</sup> zale˙znej od φ <sup>2</sup> nie jest zwi¸azywana ˙zadna zmienna wolna z φ, to Γ ` (φ → ψ).

4.6. Wniosek. Je´sli Γ ∪ {φ} ` ψ, gdzie φ nie ma zmiennych wolnych, to Γ ` (φ → ψ).

4.7. Zadania. Wyprowadzi´c:

(a) φ, ∀xφ → ψ ` ∀xψ (wskaza´c formu ly w otrzymanym dowodzie zale˙zne od φ);

(b) ` ∀x₁∀x₂φ → ∀x₂∀x₁φ;

(c) ` ∀x(φ → ψ) → (∀xφ → ∀xψ);

(c) ` ∀x(φ → ψ) → (∃xφ → ∃xψ);

(d) ` ∀x(φ ∧ ψ) ↔ (∀xφ ∧ ∀xψ);

(e) ` ∀x₁...∀x_nφ → φ.

4.8. Zadania. Je´sli v nie jest zmienn¸a woln¸a formu ly ψ, to (a) Γ ` (∃yφ(y) → φ(v)) → ψ, to Γ ` ψ;

(b) Γ ` (φ(v) → ∀yφ(y)) → ψ, to Γ ` ψ.

1(np. θ)

2tzn. obecno´s´c θ w dowodzie jest oparta na obecno´sci φ w´sr´od hipotez Γ ∪ {φ}

2