ТИ́ПОВ ТЕО́РИЯ

ТИ́ПОВ ТЕО́РИЯ в ло­ги­ке, сис­те­ма рас­ши­рен­но­го ис­чис­ле­ния пре­ди­ка­тов, вклю­чаю­щая пе­ре­мен­ные раз­лич­ных «ти­пов» (сор­тов, сте­пе­ней, по­ряд­ков). Фор­маль­ные объ­ек­ты этой тео­рии, со­глас­но сис­те­ме Рас­се­ла – Уайт­хе­да, раз­де­ля­ют­ся на ти­пы: пред­ме­ты (ин­ди­ви­ды), пре­ди­ка­ты, пре­ди­ка­ты от пре­ди­ка­тов и т. д. [объ­ек­ты n-го ти­па – это пре­ди­ка­ты от объ­ек­тов (n-1)-го и, быть мо­жет, мень­ших ти­пов]. При «двой­ст­вен­ной» фор­му­ли­ров­ке Т. т. как ак­сио­ма­ти­че­ской тео­рии мно­жеств объ­ек­ты n-го ти­па суть мно­же­ст­ва объ­ек­тов (n-1)-го (и, быть мо­жет, мень­ших) ти­па. Т. н. прин­цип свёр­ты­ва­ния (см. Аб­ст­рак­ция), не­ог­ра­ни­чен­ное ис­поль­зо­ва­ние ко­то­ро­го в рас­ши­рен­ном ис­чис­ле­нии пре­ди­ка­тов и в тео­рии мно­жеств при­во­дит к па­ра­док­сам, в Т. т. фор­му­ли­ру­ет­ся как «для вся­кой пре­ди­ка­тив­ной фор­му­лы со сво­бод­ной пе­ре­мен­ной x, не со­дер­жа­щей объ­ек­тов вы­ше (n-1)-го ти­па, су­ще­ст­ву­ет пре­ди­кат n-го ти­па, ис­тин­ный для тех и толь­ко тех зна­че­ний x, для ко­то­рых ис­тин­на дан­ная фор­му­ла» или «для лю­бо­го свой­ст­ва, в фор­му­ли­ров­ке ко­то­ро­го ис­поль­зу­ют­ся мно­же­ст­ва не вы­ше (n-1)-го ти­па, су­ще­ст­ву­ет мно­же­ст­во n-го ти­па, со­стоя­щее из тех и толь­ко тех пред­ме­тов, ко­то­рые об­ла­да­ют этим свой­ст­вом». В обе­их фор­му­ли­ров­ках вы­де­ле­ны сло­ва, до­бав­ле­ние ко­то­рых от­ли­ча­ет тео­ре­ти­ко-ти­по­вую фор­му прин­ци­па свёр­ты­ва­ния от обыч­ной и ко­то­рые пре­пят­ст­ву­ют воз­ник­но­ве­нию в Т. т. па­ра­док­сов, воз­ни­каю­щих в «на­ив­ной» тео­рии мно­жеств.

Од­на­ко ма­те­ма­ти­ка, по­стро­ен­ная на ба­зе Т. т., ока­зы­ва­ет­ся су­ще­ст­вен­но бед­нее, чем обыч­ная клас­сич. ма­те­ма­ти­ка. По­это­му Б. Рас­сел ввёл в свою сис­те­му т. н. ак­сио­му сво­ди­мо­сти, по­сту­ли­рую­щую, гру­бо го­во­ря, для ка­ж­до­го мно­же­ст­ва (пре­ди­ка­та) n-го ти­па су­ще­ст­во­ва­ние эк­ви­ва­лент­но­го ему мно­же­ст­ва 1-го ти­па. Но уже для этой ак­сио­мы ни на ка­кое «чис­то ло­ги­че­ское» обос­но­ва­ние ма­те­ма­ти­ки, как по­ка­зал сам Рас­сел, рас­счи­ты­вать не при­хо­дит­ся (в си­лу че­го про­грам­ма т. н. ло­ги­циз­ма, т. е. вы­ве­де­ния всей ма­те­ма­ти­ки из «чис­той» ло­ги­ки, ока­за­лась не­вы­пол­ни­мой).