Τυποποίηση Των Principia Metaphysica Σε Isabelle/hol

Abstract

Σκοπός της διπλωματικής αυτής εργασίας είναι η κωδικοποίηση και ηαπόδειξη βασικών θεωρημάτων των Principia Metaphysica στον αποδείκτη Ιsabelle/HOL. Η τυποποίηση αυτή επιτρέπει έλεγχο ορθότητας των αποδείξεων των Principia Μetaphysica και παρέχει ένα χρήσιμο και επεκτάσιμο αποδεικτικό περιβάλλον που μπορεί να χρησιμεύσει στην απόδειξη ολόκληρης της θεωρίας. Τα Principia Μetaphysica (γνωστά και ως Θεωρία Αφηρημένων Αντικειμένων) είναι μία θεωρία τυπικής μεταφυσικής που χρησιμοποιεί τη γλώσσα της μαθηματικής λογικής προκειμένου να παρουσιάσει τα αξιώματα της, να ορίσει μεταφυσικά αντικείμενα και να προχωρήσεισε αποδείξεις για τις ιδιότητες αυτών. H τυπική γλώσσα της θεωρίας σε συνδυασμό με την ενσωμάτωση της σε αυτόματους αποδείκτες (όπως το Isabelle/HOL) παρέχει τη δυνατότητα για υπολογιστική μεταφυσική και επιστημολογίαπραγματώνοντας, σ' ένα βαθμό, την πρόβλεψη του Leibniz για φιλοσοφία ως υπολογιστική διαδικασία. Παρουσιάζονται η κωδικοποίηση της γλώσσας, των μεταθεωρητικών εννοιών, των βασικών αξιωμάτων καθώς και αποδείξεις βασικών θεωρημάτωντων Principia σε Isabelle/HOL, παράλληλα με την πρωτότυπη θεωρία όπως παρουσιάζεται στο mally.stanford.edu/principia.pdf..