The problem of (un)decidability

U ovom radu predstavljen je povijesno–popularni pregled problema (ne)odlučivosti. Krenuli smo od Cantorovog utemeljenja teorije skupova i postavljanja hipoteze kontinuuma. S obzirom da je još od Euklidovih ”Elemenata” bilo opće prihvaćeno kako se provode (geometrijski) dokazi, teorija skupova izazvala je veliku raspravu o tome koja su sredstva dozvoljena u matematičkim dokazima. S jedne strane rasprave nalazili su se intuicionisti i konstruktivisti, a s druge formalisti. Najistaknutija osoba rasprave bila je David Hilbert, pa smo predstavili njegov znameniti govor o matematičkim problemima (od kojih je jedan, drugi bio upravo problem dokaza konzistentnosti Peanove aritmetike) te Hilbertov program – prijedlog za formalno utemeljenje i ujedinjenje matematike. Dio toga programa je i znameniti Entscheidungsproblem, pitanje postoji li algoritam koji bi za dani aksiomatski sustav i tvrdnju dao odgovor je li ta tvdnja dokaziva. Pokušavajući riješiti drugi Hilbertov problem, Kurt Goedel je dokazao znamenite teoreme o nepotpunosti kojima je pokazao neostvarivost Hilbertovog programa. Gotovo istovremeno Alan Turing koji se bavio s Hilbertovim Entscheidungsproblem i negativno ga riješio uvevši koncept stroja koji se naziva Turingov stroj iz kojeg su se razvila današnja računala. Naime, uspio je dokazati je da se ne postoji algoritam koji bi za dani program i pripadni ulaz odredio hoće li se program ikada zaustaviti ili neće (neodlučivost problema zaustavljanja). To otkriće bilo je izrazito bitno jer se mnogi drugi neodlučivi problemi mogu svesti na problem zaustavljanja. U drugom dijelu rada ukratko smo opisali četiri primjera neodlučivih problema kao što su: pitanje može li se za dvije dane konfiguracije u Igri života utvrditi hoće li druga ikad nastati iz prve; problem utvrđivanja može li se danim skupom Wangovih pločica popločati ravnina; Hilbertov deseti problem; problem optimalne strategije u igri Magic: The Gathering.This thesis presents a historic and popular review of the problem of (un)decidability. We start with Cantor’s foundation of set theory and his posing of the continuum hypothesis. Given that since Euclid’s ”Elements” the way of carrying out (geometric) proofs generally established the appearance of set theory caused a great debate about which means are allowed in mathematical proofs. On one side of the debate were intuitionists and constructivists, and on the other were formalists. The most prominent person in this debate was David Hilbert. We describe his famous speech about mathematical problems (the second of which was the problem of determining the consistency of Peano arithmetic), and Hilbert’s programme – a proposal for the formal foundation and unification of mathematics. Trying to solve Hilbert’s second problem, Kurt Goedel proved his famous incompleteness theorems, which implied that Hilbert’s programme is not realisable. At the same time Alan Turing, was investigating Hilber’s Entscheidungsproblem, and solved it negatively by introducing the concept of a machine called the Turing machine, the basis of all modern computers. Namely, he proved the undecidability of the halting problem: there does not exist an algorithm which could for any given programme and input determine if the programme will ever halt (i.e., the halting problem is undecidable). This discovery was extremely important because many other undecidable problems can be reduced to the halting problem. In the second part, we give a short description of four famous and provenly undecidable problems: the problem of determining if a given configuration will ever transform to another given configuration in the Game of Life; the problem of determinin if a given set of Wang tiles can tile the plane; Hilbert’s tenth problem; the problem of optimal strategy in the game Magic: The Gathering