Ονομάζουμε αποδεικτική διαδικασία κάθε μέθοδο που χρησιμοποιείται για ν' αποδείξουμε ότι ένας τύπος είναι λογική συνέπεια κάποιου συνόλου τύπων . Συνήθως, οι τύποι στο ονομάζονται υποθέσεις (premises) και ο συμπέρασμα (conclusion) της απόδειξης.
Μια απόδειξη αποτελείται από ένα ή περισσότερα βήματα, σε καθένα από τα οποία παράγεται ένας νέος τύπος από τις υποθέσεις και τους προηγούμενα παραγμένους τύπους. Κάθε βήμα της απόδειξης βασίζεται σε κάποιους κανόνες παραγωγής (derivation rules). Μια διαδικασία απόδειξης που συνήθως χρησιμοποιείται στα μαθηματικά, είναι η modus ponens. Σύμφωνα με τη διαδικασία αυτή, από το σύνολο των τύπων μπορούμε να πάρουμε τον τύπο . Μπορούμε να συνδέσουμε πολλούς κανόνες modus ponens μαζί, ώστε να έχουμε μια απόδειξη. Αν ο τύπος μπορεί να παραχθεί από το με χρήση κάποιων κανόνων παραγωγής, λέμε ότι ο είναι θεώρημα του υπολογισμού από το και των συγκεκριμένων κανόνων παραγωγής.
Η ορθότητα (soundness) και η πληρότητα (completeness) είναι δυο επιθυμητές ιδιότητες των αποδεικτικών διαδικασιών. Μια αποδεικτική διαδικασία ονομάζεται ορθή (sound), όταν επιτρέπει μόνο λογικές συνέπειες να παράγονται από τις υποθέσεις. Ονομάζεται πλήρης (complete), όταν είναι ικανή να παράγει όλες τις λογικές συνέπειες των υποθέσεων. Ο modus ponens είναι ορθός, αλλά όχι πλήρης.