Re: Sumrak sw. industrijeMeđutim, mi ovde ne raspravljamo o takvim programima, već o programima iz stvarnog sveta, dakle, onim programima čiji rad razumeju oni koji su ga pisali.
Kao i većina drugih matematičkih teorija predikatski račun prvog reda spada u teorije koje su poluodlučive, ali nisu odlučive. To znači da postoji procedura koja može za svaku logičku istinu predikatskog računa da dokaže u konačnom broju koraka da je zaista logička istina, ali ne postoji procdura koja bi za formulu koja nije logička istina mogla da dokaže da nije logička istina.
No, aparat se ne svodi samo na predikatski račun prvog reda. Matematika se aksiomatizuje (uobičajeno) ZFC sistemom aksioma teorije skupova. On je dovoljno jak da se sve poznate matematičke teorije mogu izložiti unutar njega i sve poznate matematičke teoreme izvesti unutar njega. Dakle, i Koši i Lagranž i Gaus i Njutn, svi su oni u ZFC-u.
No, za automatsko dokazivanje softvera se obično ne koristi teorija skupova več predikatski račun drugog reda, koji za razliku od predikatskog računa prvog reda nije čak ni poluodlučiv. To je ekvivalentno sa činjenicom da ga nije moguće kompletno aksiomatizovati (ovo nema veze sa Gedelovim teoremama nepotpunosti), tj. da je nemoguće zadati formalan sistem ili napisati proceduru za dokazivanje, koji bi obuhvatili sve logičke istine ovog računa.
No, to ne znači da postojeće (nekompletne) aksiomatike ove teorije nisu dovoljno jake za dokazivanje korektnosti softvera iz stvarnog sveta programiranja. Itekako su dovoljne da dokažu korektnost doktorata (koji radi vrlo složenu stvar) jednog mog prijatelja.
Nije bitno koji su zaključci izvučeni, već kako se do njih došlo.
