'Εστω ένα πρόβλημα 
. Υποθέτουμε ότι υπάρχει ένας αλγόριθμος ο οποίος μπορεί να δίνει σωστές απαντήσεις, σε κάθε στιγμιότυπο
(instance) του . Τότε, το πρόβλημα θα ονομάζεται υπολογίσιμο (computable). Μια ειδική κλάση προβλημάτων,
είναι αυτή που η απάντηση του αλγορίθμου σε κάθε στιγμιότυπο ενός προβλήματος μπορεί να είναι είτε ``ναι'' είτε ``όχι''. Εάν ένα πρόβλημα από
αυτή την κλάση είναι υπολογίσιμο, θα ονομάζεται αποφασίσιμο (decidable) και ο αλγόριθμος που το επιλύει διαδικασία
απόφασης (decision procedure). Αν ένα τέτοιο πρόβλημα δεν είναι υπολογίσιμο, θα ονομάζεται
μη-αποφασίσιμο (undecidable).
Η λογική συνεπαγωγή στη λογική πρώτης τάξης 
είναι ένα παράδειγμα προβλήματος που είναι μη-αποφασίσιμο.
Για κάθε 
και κάθε σύνολο τύπων 
, δεν υπάρχει απλός αλγόριθμος που ν' αποτελείται από πεπερασμένου πλήθους βήματα
και να μπορεί πάντοτε ν' αποφαίνεται, για το αν ο είναι λογική συνέπεια του (θεώρημα του Church). Ωστόσο, υπάρχουν
διαδικασίες που βελτιώνουν την κατάσταση, οι λεγόμενες αποδεικτικές διαδικασίες (proof procedures).