Επαγωγή στους φυσικούς αριθμούς και στους τύπους

Ισχυρισμοί για όλους τους τύπους

Στο μάθημα για τη γλώσσα της προτασιακής λογικής οι τύποι κατασκευάστηκαν από δύο σύμβολα, τα $\sigO$ και $\sigI$, που τα ονομάζουμε κύκλο και δίσκο, και από έναν μόνο κανόνα σχηματισμού. Υπάρχουν άπειροι τύποι, και πολλοί από τους ισχυρισμούς που έχουν σημασία αφορούν όλους: ότι κάθε τύπος τελειώνει σε δίσκο, ότι κανένας τύπος δεν διαβάζεται με δύο τρόπους, ότι σε κάθε τύπο υπάρχει μία μεταβλητή περισσότερη από τους συνδετικούς δίσκους. Τέτοιοι ισχυρισμοί δεν είναι τύποι της γλώσσας που μελετάμε, αλλά αποφάνσεις γι' αυτήν, διατυπωμένες στη μεταγλώσσα (στην ελληνική γλώσσα, με τη βοήθεια του μαθηματικού συμβολισμού)· η απόδειξή τους, επομένως, δεν είναι μια παραγωγή μέσα σε ένα τυπικό σύστημα, αλλά ένας συνηθισμένος μαθηματικός συλλογισμός που έχει ως αντικείμενο το τυπικό σύστημα. Γι' αυτό ονομάζονται μεταθεωρητικές ή εξωτερικές αποδείξεις.

Ωστόσο, κανένα πλήθος επαληθευμένων παραδειγμάτων δεν αποδεικνύει έναν ισχυρισμό για άπειρα αντικείμενα. Έπεται ότι χρειάζεται μια αρχή που να επιτρέπει να συμπεράνουμε, από πεπερασμένο πλήθος επαληθεύσεων, ότι μια ιδιότητα ισχύει σε άπειρες περιπτώσεις. Η αρχή αυτή είναι η επαγωγή. Παρουσιάζεται πρώτα στους φυσικούς αριθμούς, όπου είναι πιο οικεία, και έπειτα στους τύπους, όπου στηρίζεται στην προηγούμενη. Το ίδιο εργαλείο θα αποδείξει, στην ενότητα της μεταθεωρίας, την ορθότητα και την πληρότητα του παραγωγικού συστήματος.