Логика. Множества. Вероятность. Лексаченко В.А. - 28 стр.

UptoLike

Составители: 

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 mono
prisoedinit~ sleduwie pravila, ne rasxirwie mnoestvo
dokazuemyh sekvenci$i:
a)
Γ
1
`A ; Γ
2
, A `
B
Γ
1
, Γ
2
`
B
(
seqenie)
,
b)
Γ, A, B
`C
Γ, A
B `C
(obedinenie 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