Изворни код странице Геделова теорема о потпуности

'''Геделова теорема о потпуности''' је теорема [[математичка логика|математичке логике]] коју је доказао [[Курт Гедел]] у својој докторској дисертацији [[1929]]. и касније у раду објављеном [[1930]]. У свом најпознатијем облику, она тврди да је у [[логика првог реда|предикатском рачуну првог реда]] свака логички [[ваљана формула]] доказива. Ово је једна од најважнијих теорема математичке логике, јер показује да класичан предикатски рачун „садржи“ све законе логике који се могу исказати [[предикатска формула|предикатским формулама]].

У формулацији Геделове теореме о потпуности, реч ''доказива'' је [[синтакса|синтактичке]] природе: она означава да постоји формално извођење [[формула (математичка логика)|формуле]] у [[теорија (математичка логика)|теорији]] у питању, у овом случају у предикатском рачуну првог реда. Такво извођење–''доказ'' је коначан списак корака у којем се сваки корак или позива на [[аксиома|аксиому]] теорије или се добија из претходних корака применом основних [[правило закључивања|правила закључивања]]. Када је такво извођење дато, исправност сваког од корака се може проверити [[алгоритам]]ски (на пример, помоћу [[рачунар]]а, или ручно). Појам ваљане формуле, пак, је [[семантика|семантички]]: формула је ''ваљана'' ако је тачна у сваком [[модел (математичка логика)|моделу]] језика формуле (односно свака таква [[интерпретација (математичка логика)|интерпретација]] је и један њен модел).

Геделова теорема о потпуности показује да су аксиоме и правила закључивања предикатског рачуна првог реда „потпуни“ у смислу да никакве додатне аксиоме или правила закључивања нису потребни како би се извеле све логички ваљане формуле. Комплементарно својство је ''исправност'' (семантичка конзистентност или [[непротивуречност]]). [[Теорема о исправности]] тврди да је предикатски рачун првог реда семантички исправан, односно да се у њему могу извести '''једино''' логички ваљана тврђења. Понекад се теорема о исправности третира као део једног, свеобухватног исказа о потпуности, попут формулације самог Гедела из 1929., која у основи гласи:
:Постоји [[рачун (математичка логика)|рачун]] предикатске логике првог реда такав да за сваки скуп формула &Gamma; и сваку формулу &phi; важи: &phi; следи из &Gamma; ако и само ако се &phi; може извести из &Gamma; у овом рачуну.

Теорема о потпуности установљава темељну везу између семантике ([[теорија модела|теорије модела]], која изучава шта је тачно у различитим интерпретацијама) и синтаксе ([[теорија доказа|теорије доказа]], која изучава шта се може доказати у појединачним [[логички систем|формалним системима]]). Ако <math>\vDash</math> означава семантичку последицу и <math>\vdash</math> изведивост у рачуну, горња Геделова теорема гласи
:<math>\Gamma\vDash\varphi\,\Leftrightarrow\,\Gamma\vdash\varphi</math>.
Овде, смер здесна налево одговара исправности, а слева надесно потпуности рачуна. Слабији исказ Геделове теореме о потпуности цитиран на почетку чланка, одговара случају када је &Gamma; празан скуп формула (заправо се може доказати да су „слабији“ и „јачи“ исказ еквивалентни). Ова теорема, међутим, ''не'' укида нити маргинализује разлику између ова два приступа. У ствари, други резултат који је прославио Гедела, његова [[Геделова теорема о непотпуности|теорема о непотпуности]], показује да постоје суштинска ограничења у погледу тога шта се у математици може постићи формалним доказима: конкретно, да се унутар довољно богатих теорија не може свака доказати сваки ваљан исказ. (Пажња: име Геделове теореме о непотпуности се односи на друго значење речи „потпун“. Види чланак [[Теорија модела]].)

Геделова теорема о потпуности успоставља теоријску основу [[аутоматско доказивање|аутоматских доказивача]], дакле изради и провери доказа помоћу рачунарских програма. Првобитно је чинила и први корак у оквиру [[Хилбертов програм|Хилбертовог програма]] (израда потпуног и непротивуречног рачуна за целу [[математика|математику]]), све док програм није дотучен управо [[Геделове теореме о непотпуности|Геделовом теоремом о непотпуности]].

== Идеја доказа ==
Изворни Геделов доказ се данас углавном више не користи. Уместо њега, обично се употребљава следећа „Основна теорема логике првог реда“, коју је формулисао [[Леон Хенкин|Хенкин]] [[1949]].:
:Сваки конзистентан скуп формула има модел.
Овде се конзистентност односи на синтаксни појам: кажемо да је скуп формула &Gamma; конзистентан (непротивуречан), ако се из њега у датом рачуну не може извести [[контрадикција]], односно не постоји формула &phi; таква да је <math>\Gamma\vdash\varphi</math> и <math>\Gamma\vdash\lnot\varphi</math>.

Теорема о потпуности се може једноставно доказати претпостављајући ову теорему. И заиста, претпоставимо да је <math>\Gamma\vDash\varphi</math>, али није <math>\Gamma\vdash\varphi</math>. Рачун има својство да се конзистентном скупу формула може придружити негација формуле која се из њега не може извести при чему је и новодобијени (бројнији) скуп формула и даље конзистентан. У нашем случају, <math>\Gamma\cup\{\lnot\varphi\}</math> је такође конзистентан скуп формула и према Хенкиновој теореми има модел. У таквом моделу је, међутим, &phi; нетачна, супротно претпоставци да је у питању ваљана формула.

== Уопштења и везе са другим тврђењима ==
Важи и следећи општији облик Геделове теореме о потпуности:
:У свакој [[теорија првог реда|теорији првог реда]] ''T'', за дату реченицу ''S'' у језику ове теорије постоји извођење ''S'' из ''T'' ако и само ако је ''S'' задовољена у сваком моделу теорије ''T''.

Теорема о потпуности је средишње својство логике првог реда и не вреди у другим логикама. Логика другог реда, на пример, нема своју теорему о потпуности. Такође, потпуност је својство појединачног рачуна ''P'' (ознака <math>\vdash</math> за изведивост заправо означава <math>\vdash_P</math>) и доказ се изводи за конкретан појединачан рачун. Гедел је своју теорему доказао у [[Хилбертов рачун|Хилбертовом рачуну]]. Такође потпун је, на пример, [[Генценов рачун секвената]], облика [[природна дедукција|природне дедукције]].

Геделова теорема о потпуности је екививалентна [[лема о ултрафилтрима|леми о ултрафилтрима]], слабом облику [[аксиома избора|аксиоме избора]], у смислу да се еквиваленција може доказати у [[Зермело-Френкел теорија скупова|Зермело-Френкел теорији скупова]] без аксиоме избора (-{ZF}-).

== Изворни докази ==
* Курт Гедел, „О потпуности логичког рачуна“ (-{Kurt Gödel, "Über die Vollständigkeit des Logikkalküls"}-), докторска дисертација, Универзитет у Бечу, 1929. Ова дисертација садржи изворни доказ теореме о потпуности.
* Курт Гедел, „Потпуност аксиома логичког функцијског рачуна“ (-{Kurt Gödel, "Die Vollständigkeit der Axiome des logischen Funktionen-kalküls"}-), -{Monatshefte für Mathematik und Physik}- 37 (1930), 349-360. Овај чланак садржи исти материјал као дисертација, али у прерађеном и скраћеном облику. Докази и објашњења су краћи и изостављен је дугачак увод.

{{нормативна контрола}}

[[Категорија:Математичка логика]]
[[Категорија:Теорија модела]]
[[Категорија:Теорија доказа]]
[[Категорија:Математичке теореме]]