Составители:
Рубрика:
Po pravilu utonqeni, esli Γ
` , to
Γ `A
i
Γ `A, t. e.
simvol
Γ ` oboznaqaet protivoreqivy$i spisok
Γ
.
Opredelenie 2.8 (Vyvod v IS). Vyvodom v IS nazyvaets
taka koneqna posledovatel~nost~ sekvenci$i Σ
1
, . . .
, Σ
n
, qto
Σ
i
(
i = 1
,
. . . , n
) est~ libo aksioma, libo neposredstvennoe sleds-
tvie predyduwih sekvenci$i po pravilam 1 — 15.
Dl uproweni dokazatel~stv k pravilam vyvoda IS mono
prisoedinit~ sleduwie pravila, ne rasxirwie mnoestvo
dokazuemyh sekvenci$i:
a)
Γ
1
`A ; Γ
2
, A `
B
Γ
1
, Γ
2
`
B
(
seqenie)
,
b)
Γ, A, B
`C
Γ, A
∧
B `C
(obedinenie dopuweni$i
),
v)
Γ, A
∧B `C
Γ, A, B
`C
(
rasweplenie dopuweni$i),
g)
Γ, A
`C
; Γ, B `C
Γ, A
∨
B `
C
(razbor sluqaev)
,
d)
Γ, A `B
Γ, B
`
A
(kontrapozici
)
,
e)
Γ, B `A
Γ, A
`B
(
dokazatel~stvo ot protivnogo
),
)
Γ `B
`
V
Γ
→
B
(
vvedenie
∧
i →),
z)
`
V
Γ
→
B
Γ `
B
(udalenie
∧
i →
)
.
Primer. Vyvod v IS sekvencii A, A→
B, B
→
C, C →D
`
D
.
1) A `A — aksioma,
2)
A →
B `
A →
B — aksioma,
3)
A, A →
B
`
B — udalenie
→
, 1, 2,
4) B
→
C `
B
→ C — aksioma,
5)
A, A →
B, B →
C `C
— udalenie →, 3, 4.
6)
C →
D
`C →
D — aksioma,
7) A, A
→ B, B
→
C, C → D `
D
— udalenie
→, 5, 6.
Teorema 2.13 (O polnote IS). V IS `
A
togda i tol~ko togda,
kogda |=
A
.
Bez dokazatel~stva.
28
Страницы
- « первая
- ‹ предыдущая
- …
- 26
- 27
- 28
- 29
- 30
- …
- следующая ›
- последняя »