Μαθηματική Λογική

Abstract

Η μαθηματική Λογική είναι στενά συνδεδεμένη με τα προγράμματα θεμελίωσης των Μαθηματικών. Το γνωστότερο και συνεκτικότερο από αυτά , το πρόγραμμα του Hilbert, εισήγαγε την έννοια του τυπικού αξιωματικού συστήματος και το ζήτημα της αποκρισιμότητας, δηλαδή τα δύο βασικά θεμέλια των επιστημών της Λογικής και της Πληροφορικής. Στόχος αυτού του προγράμματος ήταν η απόδειξη της συνέπειας των μαθηματικών θεωριών. Ο Gödel, αποδεικνύοντας την αδυναμία υλοποίησης αυτού του στόχου, εισήγαγε τις πρωτογενείς αναδρομικές συναρτήσεις καθώς και τη δυνατότητα των τυπικών συστημάτων να αναφέρονται στον εαυτό τους. Αυτό οδήγησε τον Turing να διατυπώσει το μοντέλο του υπολογισμού και να αποδείξει τα πρώτα αποτελέσματα αναποκρισιμότητας. Εισήχθησαν οι αναδρομικές συναρτήσεις και ξεκαθαρίστηκε το θολό τοπίο του υπολογίσιμου. Η κατάληξη ήταν η δημιουργία, σε θεωρητικό επίπεδο, της επιστήμης της πληροφορικής και ταυτόχρονα η αποφασιστική συμβολή στη θεμελίωση των μαθηματικών και της θεωρίας συνόλων.<br/> Σκοπός του βιβλίου είναι να παρουσιάσει όλα τα κλασικά αποτελέσματα της λογικής τα οποία στη συνέχεια έγιναν απαραίτητα σε κάθε σοβαρή μελέτη των θεμελίων των μαθηματικών και της (θεωρητικής) πληροφορικής. Η έννοια του τυπικού αποδεικτικού συστήματος, η αποδειξιμότητα , η ερμηνεία των τυπικών θεωριών, τα θεωρήματα πληρότητας, αποτελούν αντικείμενα του βιβλίου. Επίσης η μελέτη των αναδρομικών συναρτήσεων και η απόδειξη του θεωρήματος μη πληρότητας του Gödel, το οποίο μετεξελίχθηκε στο αποτέλεσμα αναποκρισιμότητας των Gödel, Turing και Church. <br/> Η θεωρία αποδείξεων, που πήρε την εκλεπτυσμένη της μορφή από τον Gentzen, ενδιαφέρεται όχι μόνον για το τι αποδεικνύεται αλλά και για το πώς αποδεικνύεται. Θα παρουσιαστούν όλα τα μεγάλα αποτελέσματα όπως ο sequent calculus, natural deduction και το περίφημο θεώρημα απαλοιφής των τομών, τα οποία, μέσω της ισομορφίας των αποδείξεων με τα προγράμματα, ουσιαστικά αποτελούν μαθηματική μελέτη της δομής των προγραμμάτων στο χώρο της πληροφορικής.

Mathematical Logic is closely connected with the foundational programs of Mathematics. The most well-known and coherent of these, Hilbert's program, introduced the concept of formal axiomatic systems and the issue of decidability, which are the two fundamental pillars of the sciences of Logic and Computer Science. The goal of this program was to prove the consistency of mathematical theories. Gödel, by demonstrating the impossibility of achieving this goal, introduced the primitive recursive functions as well as the ability of formal systems to reference themselves. This led Turing to formulate the model of computation and to prove the first results of undecidability. Recursive functions were introduced, clarifying the previously obscure landscape of computability. The outcome was the creation, at a theoretical level, of the science of Computer Science, while simultaneously making a decisive contribution to the foundation of mathematics and set theory. The purpose of this book is to present all the classical results of logic which subsequently became essential in any serious study of the foundations of mathematics and theoretical computer science. The concept of formal proof systems, provability, the interpretation of formal theories, and completeness theorems are subjects of the book. Additionally, the study of recursive functions and the proof of Gödel's incompleteness theorem, which evolved into the undecidability results of Gödel, Turing, and Church, will be explored. Proof theory, which took its refined form from Gentzen, is concerned not only with what is proven but also with how it is proven. All the major results will be presented, such as the sequent calculus, natural deduction, and the famous cut-elimination theorem, which, through the isomorphism of proofs with programs, essentially constitute a mathematical study of the structure of programs in the field of computer science.