Раздзел 2. Злiчэнне выказванняў

– Ну! – падумала Алiса. – Бачыла я катоў без усмешак, але ўсмешка без ката! Гэта самае дзiўнае, што я бачыла ў сваiм жыццi!

(Льюiс Кэрал. Прыгоды Алiсы ў краiне цудаў)

§1. Фармальныя тэорыi

Мэта гэтага параграфу – даць дакладнае азначэнне паняццяў “матэматычны доказ”, “тэарэма”, “сцверджанне вынікае з сцверджанняў ”.

Спачатку прааналiзуем працэс доказу ў матэматыцы на простым прыкладзе.

Прыклад. Разгледзiм сцверджанне: “Функцыя , дыферэнцавальная на адрэзку , абмежаваная на гэтым адрэзку”. Абазначым праз наступныя выказваннi:

“ дыферэнцавальная на адрэзку ”, “ непарыўная на адрэзку ”, “ абмежаваная на адрэзку ” (мы раней адзначалі, што падобныя сцверджанні не з’яўляюцца выказваннямі, бо мы не ведаем, чаму роўная і таму не можам сказаць, праўдзівыя гэтыя сцверджанні ці непраўдзівыя; таму мы будзем лічыць, што - адвольная, але фіксаваная функцыя, а для фіксаванай функцыі кожнае з гэтых сцверджанняў – выказванне). Запiшам доказ нашага сцверджання ў выглядзе паслядоўнасцi формулаў:

(1) ; (2) ; (3) ; (4) ; (5) .

Формула (1) – умова нашага сцверджання, формулы (2) i (3) – вядомыя тэарэмы, формула (4) вынiкае з формулаў (1) i (2), а формула (5) – з (4) i (3) паводле правiла:

ёсць вынiк формулаў i .

Цяпер дамо нашым iнтуiцыйным уяўленням пра працэс доказу дакладную форму.

Фармальная (аксiяматычная) тэорыя лiчыцца вызначанай, калi выконваюцца наступныя ўмовы:

(1) Ёсць злiчонае мноства сымболяў – сымболяў тэорыi . Канцоўныя паслядоўнасцi сымболяў тэорыi называюцца выразамi тэорыi .

(2) Ёсць падмноства выразаў тэорыi , якiя называюцца формуламi тэорыi (звычайна ёсць эфектыўная працэдура, якая дазваляе па дадзеным выразе вызначыць, цi з’яўляецца ён формулай).

(3) Вылучана пэўная сукупнасць формулаў, якiя называюцца аксiёмамi тэорыi (звычайна ёсць магчымасць эфектыўна высветлiць, цi з’яўляецца дадзеная формула аксiёмай).

(4) Ёсць канцоўнае мноства дачыненняў памiж формуламi, якiя называюцца правiламi вывядзення Для кожнага iснуе натуральны такi, што для ўсякага мноства з формулаў i кожнай формулы эфектыўна развязваецца пытанне пра тое, цi знаходзяцца дадзеныя формулаў у дачыненні з формулай , i калi так, тады называецца непасрэдным вынiкам дадзеных формулаў паводле правiла .

У нашым прыкладзе мы карысталiся наступным правiлам вывядзення: формула ёсць непасрэдны вынiк формулаў i .

Азначэнне. Вывядзеннем ў называецца ўсякая паслядоўнасць формулаў такая, што для кожнага i – або аксiёма тэорыi , або непасрэдны вынiк некаторых папярэднiх формулаў паводле аднаго з правiлаў вывядзення.

Азначэнне. Формула тэорыi называецца тэарэмай (ці выводнай формулай), калi iснуе вывядзенне ў , апошняй формулай у якiм з’яўляецца ; гэтае вывядзенне называецца вывядзеннем формулы (доказам тэарэмы ).

Азначэнне. Тэорыя называецца развязальнай, калi iснуе алгарытм, якi дазваляе вызначыць па дадзенай формуле тэорыi , цi з’яўляецца яна тэарэмай; у адваротным выпадку тэорыя называецца неразвязальнай.

Азначэнне. Формула называецца вынiкам мноства формулаў у тэорыi , калi iснуе такая паслядоўнасць формулаў , што , i для кожнага i — або аксiёма, або элемент , або непасрэдны вынiк некаторых папярэднiх формулаў паводле аднаго з правiлаў вывядзення. Гэтая паслядоўнасць называецца вывядзеннем з , а элементы — гiпотэзамi, або ўмовамi вывядзення.

Тое, што ёсць вынiк , будзем запiсваць наступным чынам: ├ . Калi — пустое мноства, г.зн., – тэарэма тэорыi , будзем пiсаць ├ .

У прыкладзе на пачатку параграфу ├ .

У якасцi прыкладу аксiяматычнае тэорыi ў наступным параграфе мы разгледзiм тэорыю, якая называецца злiчэннем выказванняў.