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

UptoLike

ВУЗ: 

СПб ГУАП | Санкт-Петербург

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

Рубрика: 

4. Formal~nye sistemy
V bol~xinstve aksiomatiqeskih teori$i matematiki, obek-
ty i utverdeni tih teori$i traktuts soderatel~no, qto
moet inogda privesti k nerazreximym protivoreqim (para-
doksam). Vyhod zaklqaets v tom, qtoby rassmatrivat~ ma-
tematiqeskie teorii kak formal~nye sistemy
, t. e. kak siste-
my operaci$i nad formulami nekotorogo toqnogo logiko-matema-
tiqeskogo zyka
, bez kako$i-libo soderatel~no$i interpretacii
formul. Postroenie formal~no$i sistemy svodits k zadani
zyka, aksiom i pravil vyvoda sistemy. zyk opredelets
alfavitom
(pereqnem ishodnyh simvolov) i
sintaksisom —
pravilami postroeni formul sistemy: 1) termov
(predmetov),
2)
sootnoxeni$i (utverdeni$i).
Rassmotrim formal~nu sistemu sovremenno$i matematiki,
nazyvaemu isqisleniem predikatov pervogo pordka s funkci-
onal~nymi i predikatnymi znakami (IPFP).
Opredelenie 4.1 (zyk IPFP).
Alfavit soderit:
predmetnye peremennye
a, b,
. . . , x, y, z,
a
1
, a
2
, . . . , a
0
, a
00
,
. . . ;
simvoly f
n
j
j
predmetnyh funkci$i n
j
pred-
metnyh argumentov,
n
j
= 0,
1
, . . . ,
(simvoly funkci$i
0
argumen-
tov nazyvats predmetnymi konstantami);
simvoly
P
n
j
j
pre-
dikatov
n
j
predmetnyh argumentov, n
j
= 1, 2, . . ., vklqa pre-
dikat ravenstva
= ;
logiqeskie znaki
∨,
∧,
, →,
∼
,
∀, ∃, τ
;
vspo-
mogatel~nye znaki ”
,
”
,
”(”
, ”)”.
Pravila postroeni termov.
T
1
. Predmetnye peremennye i konstanty vlts termami.
T
2
. Esli
T
1
, . . .
, T
n
j
— termy, to f
n
j
j
(T
1
,
. . .
, T
n
j
)
— term.
T
3
. Formuly naqinawies so znaka τ
vlts termami.
T
4
. Nikakih termov, krome opredelennyh pp. T
1
— T
3
, net.
Pravila postroeni sootnoxeni$i.
R
1
. Esli T
1
,
. . .
, T
n
j
— termy, to
P
n
j
j
(
T
1
, . . . , T
n
j
)
—
sootnoxenie.
R
2
. Esli A, B
— sootnoxeni,
x
— predmetna peremenna,
to
A, A
∧
B, A ∨ B, A →
B,
(∀x
)
A, (∃
x)A — sootnoxeni.
R
3
. Nikakih sootnoxeni$i, krome opredelennyh pp.
R
1
, R
2
net.
Opredelenie 4.2 (Podstanovki termov v formuly). Pust~ for-
mula A
(
x
) soderit svobodno peremennu
x
. Term T
nazyvaet-
s svobodnym dl x v
A(x
), esli ni odna iz peremennyh terma
ne svzyvaets pri ego podstanovke vmesto
x.
37

Страницы