ФОРМА́ЛЬНАЯ СИСТЕ́МА

ФОРМА́ЛЬНАЯ СИСТЕ́МА, уточ­не­ние по­ня­тия ак­сио­ма­ти­че­ской тео­рии, ха­рак­те­ри­зую­щее­ся пред­став­ле­ни­ем по­след­ней в ви­де ис­чис­ле­ния. Про­цесс по­строе­ния Ф. с. в ка­че­ст­ве точ­но­го ана­ло­га дан­ной ак­сио­ма­тич. тео­рии обыч­но на­зы­ва­ет­ся фор­ма­ли­за­ци­ей этой тео­рии.

По­строе­ние Ф. с. на­чи­на­ет­ся с опи­са­ния фор­ма­ли­зо­ван­но­го язы­ка. На­бор ис­ход­ных сим­во­лов (ал­фа­вит) язы­ка и пра­ви­ла по­строе­ния ос­мыс­лен­ных вы­ра­же­ний (фор­мул) вы­би­ра­ют­ся так, что­бы фор­ма­ли­зов. язык мог слу­жить для за­пи­си всех пред­ло­же­ний дан­ной ак­сио­ма­тич. тео­рии. За­тем вы­де­ля­ет­ся класс фор­мул, на­зы­вае­мых ак­сио­ма­ми. Обыч­но мно­же­ст­во ак­си­ом за­да­ёт­ся спи­ском (ес­ли оно ко­неч­но) или с по­мо­щью ал­го­рит­ма, ко­то­рый для лю­бой фор­му­лы по­зво­ля­ет про­ве­рить, яв­ля­ет­ся ли она ак­сио­мой. В ка­че­ст­ве ак­си­ом ча­ще все­го вы­би­ра­ют фор­му­лы, слу­жа­щие для за­пи­си ак­си­ом фор­ма­ли­зуе­мой ак­сио­ма­тич. тео­рии (соб­ст­вен­ные, или не­ло­ги­че­ские, ак­сио­мы), к ко­то­рым до­бав­ля­ют­ся т. н. ло­гич. ак­сио­мы – фор­му­лы, ко­то­рые уже в си­лу сво­его строе­ния яв­ля­ют­ся за­пи­ся­ми ис­тин­ных пред­ло­же­ний. Кро­ме ак­си­ом, при по­строе­нии Ф. с. за­да­ёт­ся (обыч­но ко­неч­ный) класс пра­вил вы­во­да, ко­торые долж­ны как мож­но бо­лее пол­но от­ра­жать спо­со­бы ло­гич. вы­во­да, при­ме­няе­мые в ма­те­ма­тич. рас­су­ж­де­ни­ях. В ма­те­ма­тич. ло­ги­ке вы­ра­бо­та­ны стан­дарт­ные сис­те­мы ло­гич. ак­си­ом и пра­вил вы­во­да, с по­мо­щью ко­то­рых мож­но по­лу­чить все ло­гич. след­ст­вия из дан­ных не­ло­гич. ак­си­ом (см. Пре­ди­ка­тов ис­чис­ле­ние). До­ка­за­тель­ст­вом в Ф. с. на­зы­ва­ет­ся ко­неч­ная по­сле­до­ва­тель­ность фор­мул, в ко­то­рой ка­ж­дая фор­му­ла ли­бо яв­ля­ет­ся ак­сио­мой, ли­бо не­по­сред­ст­вен­но вы­во­ди­ма по од­но­му из пра­вил вы­во­да из не­ко­то­рых фор­мул, пред­ше­ст­вую­щих ей в этой по­сле­до­ва­тель­но­сти. Фор­му­ла на­зы­ва­ет­ся тео­ре­мой, ес­ли су­ще­ст­ву­ет до­ка­за­тель­ст­во, по­след­ней фор­му­лой ко­то­ро­го она яв­ля­ет­ся.

Ф. с. суть точ­ные ма­те­ма­тич. объ­ек­ты, ис­сле­до­ва­ние ко­то­рых мож­но вес­ти ма­те­ма­тич. ме­то­да­ми. Фор­ма­ли­за­ция осн. раз­де­лов ма­те­ма­ти­ки и обос­но­ва­ние их не­про­ти­во­ре­чи­во­сти пу­тём ана­ли­за до­ка­за­тельств в со­от­вет­ст­вую­щих Ф. с. бы­ли со­став­ной ча­стью вы­дви­ну­той Д. Гиль­бер­том про­грам­мы обос­но­ва­ния ма­те­ма­ти­ки (см. Ме­та­ма­те­ма­ти­ка).