ВЫСКА́ЗЫВАНИЙ ИСЧИСЛЕ́НИЕ

ВЫСКА́ЗЫВАНИЙ ИСЧИСЛЕ́НИЕ (про­по­зи­цио­наль­ное ис­чис­ле­ние), об­щее на­зва­ние ак­сио­ма­тич. сис­тем (см. Ак­сио­ма­ти­че­ский ме­тод), пред­на­зна­чен­ных для до­ка­за­тель­ст­ва ут­вер­жде­ний (фор­мул), со­став­лен­ных из про­стей­ших (не ана­ли­зи­руе­мых в рам­ках дан­ной сис­те­мы) ут­вер­жде­ний при по­мо­щи ло­гич. свя­зок, та­ких как «не», «или», «ес­ли… то…» и др.

С син­так­сич. точ­ки зре­ния раз­ли­ча­ют неск. ви­дов В. и.: т. н. гиль­бер­тов­ские, се­к­вен­ци­аль­ные (ген­це­нов­ские), сис­те­мы на­ту­раль­но­го вы­во­да и др. Важ­ней­шим при­ме­ром В. и. яв­ля­ет­ся клас­сич. В. и., где ис­поль­зу­ют­ся тра­диц. ло­гич. связ­ки: «или» (∨), «и» (&), «ес­ли..., то...» (→), «не» (¬). При этом ут­вер­жде­ния ин­тер­пре­ти­ру­ют­ся как бу­ле­вы функ­ции, при­ни­маю­щие два зна­че­ния: «ис­ти­на» (1) и «ложь» (0); связ­ки со­от­вет­ст­ву­ют стан­дарт­ным опе­ра­ци­ям на мно­же­ст­ве {0,1}: ∨ – взя­тию мак­си­му­ма, & – взя­тию ми­ни­му­ма, и т. д. В гиль­бер­тов­ской фор­му­ли­ров­ке ис­поль­зу­ют­ся схе­мы ак­си­ом (та­кие как A→(B→A); A&B→A; B→A∨B; A∨¬A и др.) и един­ст­вен­ное пра­ви­ло вы­во­да modus ponens (пра­ви­ло от­де­ле­ния), по­зво­ляю­щее из фор­мул A и A→B по­лу­чить B. Тео­ре­ма­ми это­го ис­чис­ле­ния яв­ля­ют­ся в точ­но­сти все тав­то­ло­гии – фор­му­лы, от­ве­чаю­щие то­ж­де­ст­вен­но ис­тин­ным бу­ле­вым функ­ци­ям. От­сю­да сле­ду­ет ал­го­рит­мич. раз­ре­ши­мость, т. е. су­ще­ст­во­ва­ние ал­го­рит­ма, рас­по­знаю­ще­го тео­ре­мы дан­но­го ис­чис­ле­ния (см. Ал­го­рит­ми­че­ская про­бле­ма).

По­ми­мо клас­сич. В. и., из­вест­ны раз­но­об­раз­ные не­клас­сич. В. и., в ко­то­рых лoгич. связ­ки уже не все­гда сво­дят­ся к бу­ле­вым функ­ци­ям. Ин­туи­цио­ни­ст­ское В. и. бы­ло пред­ло­же­но для фор­ма­ли­за­ции ло­гич. прин­ци­пов ин­туи­цио­низ­ма (см. Кон­ст­рук­тив­ная ло­ги­ка). Оно по­лу­ча­ет­ся из клас­сич. В. и. уда­ле­ни­ем схе­мы ак­си­ом A∨¬A, вы­ра­жаю­щей ис­клю­чён­но­го третье­го за­кон. Мно­го­числ. мо­даль­ные В. и. яв­ля­ют­ся, как пра­ви­ло, рас­ши­ре­ни­ем клас­сич. В. и. и ис­поль­зу­ют но­вые связ­ки: «не­об­хо­ди­мо», «воз­мож­но», «до­ка­зуе­мо» и др. (см. Мо­даль­ная ло­ги­ка); раз­но­вид­но­стью мо­даль­ных яв­ля­ют­ся вре­мен­ны́е и ди­на­мич. В. и., рас­смат­ри­ваю­щие связ­ки «все­гда бу­дет», «вче­ра», «c тех пор, как» и т. п. Ис­сле­ду­ют­ся так­же мно­го­знач­ные и не­чёт­кие В. и. (см. Мно­го­знач­ная ло­ги­ка).

Мно­гие ви­ды В. и. тес­но свя­за­ны с др. ти­па­ми фор­маль­ных сис­тем, например лям­бда-ис­чис­ле­ния­ми и фор­маль­ны­ми грам­ма­ти­ка­ми. В. и. иг­ра­ют важ­ную роль в ин­фор­ма­ти­ке, ма­те­ма­тич. лин­гвис­ти­ке, тео­рии до­ка­за­тельств, тео­рии слож­но­сти вы­чис­ле­ний.