Составители:
Рубрика:
Slaboe udalenie (A , A `
B ).
1)
A,
A, B `
A
— svo$istvo 1,
2) A, A, B
`
A
— svo$istvo 1,
3) A, A
`
B
— vvedenie
1, 2,
4)
B
→ B —
AS
10
,
5) A, A `
B —
MP 3, 4.
Pravila vvedeni i udaleni kvivalencii osnovany na
pravilah vvedeni i udaleni konnkcii.
Dokaem pravilo obedineni dl spiskov dopuweni$i (pust~
A, B `C , togda A∧
B
`C
).
1)
A, B
`C
— po uslovi,
2)
A∧
B `A — udalenie
∧,
3) A∧B
`
B
— udalenie ∧
,
4) A
∧B
`
C — svo$istvo 3, 1, 2, 3.
Dokaem pravilo raswepleni dl spiskov dopuweni$i (pust~
A∧
B `
C , togda
A, B
`
C ).
1) A
∧B `
C — po uslovi,
2)
A, B
`
A∧B
— vvedenie ∧
,
3)
A, B
`
C
— svo$istvo 3, 1, 2.
Netrudno dokazat~, qto dl formal~nyh sekvenci$i primenim
metod rezolci$i.
Teper~ imets vse osnovani utverdat~, qto dokazatel~-
stvom sekvencii A
1
,
. . . , A
m
`C vlets dokazatel~stvo sekven-
cii
A
1
, . . .
, A
m
|
= C
s pomow~ teorem 2.3 — 2.6, v kotorom
znak
|=
zamenen na
`
. Na samom dele spravedliv bolee ob-
wi$i rezul~tat, kotory$i zdes~ privedem bez dokazatel~stva.
Teorema 2.11 (O polnote IV).
Esli
A
1
,
. . .
, A
n
|
= B
, to
A
1
,
. . . , A
n
`
B .
Teorema 2.12 (O neprotivoreqivosti IV). Esli
`A
, to
|= A.
D o k a z a t e l ~ s t v o . Shemy aksiom IV vlts tavtologi-
mi, a pravilo MP perevodit tavtologii v tavtologii. J
Sledstvie. (O prosto$i neprotivoreqivosti IV).
Ni dl kako$i
formuly
A ne vypolnets odnovremenno
`A
i `
A
.
Svo$istva znaka
`
, teoremy o ravnosil~nosti spiskov do-
puweni$i, pravila vvedeni i udaleni logiqeskih znakov v
opredelennom smysle zament aksiomy isqisleni vyskazy-
vani$i IV. Mono tak vybrat~ sistemu pravil vyvoda, qto
ostanets lix~ odna shema aksiom. ta ide realizuets v
aksiomatiqeskom isqislenii vyskazyvani$i IS, v kotorom os-
novnym obektom vlts sekvencii vida Γ
`B,
`
B, Γ ` .
26
Страницы
- « первая
- ‹ предыдущая
- …
- 24
- 25
- 26
- 27
- 28
- …
- следующая ›
- последняя »