Formal frameworks on proving and inquiry

Abstract

In this dissertation we address the problem of the formalisation of the process that leads to the solution of a problem or to the proof of a theorem. The subject is examined from two distinct, yet closely related, perspectives: the first is based on Algebraic Geometry, while the second combines elements from Topology, Probability Theory, and Abstract Model Theory. Within the first approach, using tools from Algebraic Geometry and in particular the structure of sheaves, we construct systems of provers, which are realized as multi-layered systems of presheaves. These systems are equipped with morphisms that express fundamental mathematical practices, such as proof attempts, abstraction, and refinement of strategy. The latter introduces new constraints, on the basis of which a new proof attempt is initiated. Moreover, building on Goguen’s theory of objects, we show that within this framework one can define a new object, the semantic brain, whose field of observations is the multi-layered system of provers. We call this object a semantic brain precisely because it allows for the modelling of sequences of thoughts with an emphasis on their temporal dimension. On this object, we describe a path of gaining experience during problem solving through a dynamic probabilistic framework, which assigns a probability of realization to each step of thought and adjusts its "weight" when it is realized. Finally, we construct systems of multiple semantic brains which, in combination with the application of argumentation logic to proof events, form a new framework (APEC-PS) through which collective problem-solving processes can be modelled. As an example of the applicability of this framework, we use the Mini-Polymath 4 project, which concerns the collaborative solution of a mathematical Olympiad problem by members of the mathematical community. In the second approach, we connect Formal Learning Theory, which constitutes a topological approach to learning, with Abstract Model Theory and, more specifically, with Institution Theory. This connection is achieved through the definition of appropriate learning topologies on the categories of models over the signatures of an Institution. In this way, a topological extension of the notions of Verifiability, Decidability, and Solvability in formal languages becomes possible. We present an example of such an extension of Propositional Logic. We then study properties of topologies suitable for expressing the relationship between syntax and semantics of a formal language, and we show that, based on their topological properties, one can derive logical properties of the language, and conversely. Subsequently, we extend our approach to include Statistical Learning. By introducing the definition of a Probabilistic Institution, we show how probabilistic versions of formal languages can be defined, using Propositional Logic as an example. Finally, we propose an approach to the geometry of generalized Aristotelian Squares of Opposition, exploiting the relationship between syntax and semantics within Institution Theory. We define the notion of closure of these diagrams and show how one can systematically search for squares of opposition corresponding to specific logics, as well as for translations between logics that preserve significant semantic properties.

Στην παρούσα διατριβή προσεγγίζουμε το ζήτημα της τυπικής περιγραφής της διαδικασίας που οδηγεί στην επίλυση ενός προβλήματος ή στην απόδειξη ενός θεωρήματος. Το θέμα εξετάζεται από δύο διαφορετικές, αλλά στενά συνδεδεμένες μεταξύ τους, σκοπιές: η πρώτη βασίζεται στην Αλγεβρική Γεωμετρία, ενώ η δεύτερη συνδυάζει στοιχεία από την Τοπολογία, τη Θεωρία Πιθανοτήτων και την Αφηρημένη Θεωρία Μοντέλων. Στο πλαίσιο της πρώτης προσέγγισης, χρησιμοποιώντας εργαλεία της Αλγεβρικής Γεωμετρίας και συγκεκριμένα τη δομή των δραγμάτων (sheaves), κατασκευάζουμε συστήματα αποδεικτών (provers), τα οποία υλοποιούνται ως πολυεπίπεδα συστήματα προδραγμάτων (presheaves). Τα συστήματα αυτά διαθέτουν μορφισμούς που εκφράζουν βασικές μαθηματικές πρακτικές, όπως οι προσπάθειες απόδειξης, η αφαίρεση και η προσαρμογή της στρατηγικής. Η τελευταία εισάγει νέους περιορισμούς, βάσει των οποίων εκκινεί μια νέα προσπάθεια απόδειξης. Επιπλέον, βασιζόμενοι στην θεωρία του Goguen για τα αντικείμενα (objects), δείχνουμε ότι στο πλαίσιο αυτής της προσέγγισης μπορούμε να ορίσουμε ένα νέο αντικείμενο, τον «σημασιολογικό νου» (semantic brain), του οποίου το πεδίο παρατηρήσεων είναι το πολυεπίπεδο σύστημα αποδεικτών. Ονομάζουμε το αντικείμενο αυτό σημασιολογικό νου, καθώς επιτρέπει τη μοντελοποίηση ακολουθιών σκέψεων με έμφαση στη χρονική τους διάσταση. Πάνω σε αυτό το αντικείμενο περιγράφουμε την απόκτηση εμπειρίας κατά την επίλυση προβλημάτων μέσω ενός δυναμικού πιθανοτικού πλαισίου, το οποίο αποδίδει πιθανότητα πραγματοποίησης σε κάθε στοιχειώδη σκέψη και προσαρμόζει το «βάρος» της όταν αυτή πραγματοποιείται. Τέλος, κατασκευάζουμε συστήματα πολλών σημασιολογικών νόων, τα οποία, σε συνδυασμό με την εφαρμογή του Επιχειρηματολογικού Λογισμού (argumentation logic) στα αποδεικτικά γεγονότα, συνθέτουν ένα νέο πλαίσιο (APEC-PS), μέσω του οποίου μπορούν να μοντελοποιηθούν συλλογικές διαδικασίες επίλυσης προβλημάτων. Ως παράδειγμα εφαρμογής του πλαισίου αυτού χρησιμοποιούμε το έργο Mini-Polymath 4, το οποίο αφορά τη συνεργατική επίλυση ενός προβλήματος μαθηματικής Ολυμπιάδας από μέλη της μαθηματικής κοινότητας. Στη δεύτερη προσέγγιση, συνδέουμε την Τυπική Θεωρία Μάθησης (Formal Learning Theory), η οποία αποτελεί μια τοπολογική προσέγγιση της μάθησης, με την Αφηρημένη Θεωρία Μοντέλων και, ειδικότερα, με τη Θεωρία Θεσμών (Institution Theory). Η σύνδεση αυτή επιτυγχάνεται μέσω του ορισμού κατάλληλων τοπολογιών μάθησης στις κατηγορίες μοντέλων πάνω από τις υπογραφές (signatures) ενός θεσμού (institution). Με αυτόν τον τρόπο, καθίσταται δυνατή η τοπολογική διεύρυνση των εννοιών της επαληθευσιμότητας (Verifiability), της αποφασισιμότητας (Decidability) και της επιλυσιμότητας (Solvability) στις τυπικές γλώσσες. Παρουσιάζουμε ως παράδειγμα μια τέτοια διεύρυνση της Προτασιακής Λογικής. Στη συνέχεια, μελετούμε ιδιότητες τοπολογιών κατάλληλων να εκφράσουν τη σχέση μεταξύ του συντακτικού και του σημασιολογικού μέρους μιας τυπικής γλώσσας και δείχνουμε ότι, βάσει των τοπολογικών τους ιδιοτήτων, μπορούμε να εξαγάγουμε λογικές ιδιότητες της γλώσσας, και αντιστρόφως. Έπειτα, επεκτείνουμε την προσέγγισή μας ώστε να περιλαμβάνει και τη Στατιστική Μάθηση. Εισάγοντας τον ορισμό του Πιθανοτικού Θεσμού (Probabilistic Institution), δείχνουμε πώς μπορούν να οριστούν πιθανοτικές εκδοχές τυπικών γλωσσών, παρουσιάζοντας εκ νέου το παράδειγμα της Προτασιακής Λογικής. Τέλος, προτείνουμε μια προσέγγιση στη γεωμετρία των γενικευμένων Αριστοτελικών Διαγραμμάτων Αντίθεσης, αξιοποιώντας τη σχέση μεταξύ συντακτικού και σημασιολογίας στη Θεωρία Θεσμών. Ορίζουμε την έννοια της κλειστότητας αυτών των διαγραμμάτων και δείχνουμε πώς μπορούν να αναζητηθούν συστηματικά διαγράμματα αντίθεσης που αντιστοιχούν σε συγκεκριμένες λογικές, καθώς και μεταφράσεις μεταξύ λογικών που διατηρούν σημαντικές σημασιολογικές ιδιότητες.