Στα μαθηματικά και τη λογική, μία λογική ανώτερου βαθμού ή λογική ανώτερης τάξης (higher-order logic) διακρίνεται από μία λογική πρώτου βαθμού με βάση αρκετά χαρακτηριστικά. Ένα από αυτά είναι ο τύπος των μεταβλητών που εμφανίζονται στους ποσοδείκτες: γενικά, στην πρωτοβάθμια λογική, απαγορεύεται οι ποσοδείκτες να αναφέρονται σε κατηγορήματα, ενώ αυτό επιτρέπεται στη λογική δεύτερου βαθμού. Η λογική ανώτερου βαθμού διαφέρει επίσης από τη λογική πρώτου βαθμού στις δομές που η θεωρία τύπων της επιτρέπει να κατασκευάζονται. Ένα κατηγόρημα ανώτερου βαθμού είναι ένα κατηγόρημα που δέχεται σαν παραμέτρους κατηγορήματα. Γενικά, ένα κατηγόρημα βαθμού n παίρνει ένα ή περισσότερα κατηγορήματα βαθμού n − 1 σαν παραμέτρους, όπου n > 1. Παρόμοια ισχύουν και για τις συναρτήσεις ανώτερης τάξης.
Ο όρος λογική ανώτερης τάξης (Higher-order logic, συντομογραφία HOL), συχνά χρησιμοποιείται για απλές λογικές κατηγορημάτων ανώτερου βαθμού, δηλαδή λογικές των οποίων η θεωρία τύπων είναι απλή, όχι πολυμορφική ή με εξαρτώμενους τύπους.[1]
Οι λογικές ανώτερου βαθμού είναι πιο εκφραστικές, αλλά οι ιδιότητές τους, ειδικά όσον αφορά τη θεωρία μοντέλων, τις κάνουν δυσκολότερες στο χειρισμό για πολλές εφαρμογές. Λόγω ενός αποτελέσματος του Γκέντελ, η κλασική λογική ανώτερου βαθμού δεν επιδέχεται ενός (αναδρομικού και αξιωματικού) λογισμού αποδείξεων που να είναι συνεπής (sound) και πλήρης (complete) - ένας τέτοιος λογισμός όμως υπάρχει και είναι συνεπής και πλήρης όσον αφορά τα μοντέλα Χένκιν (Henkin models).
Παραδείγματα λογικών ανώτερου βαθμού είναι ο λ-λογισμός με απλούς τύπους του Τσερτς (Απλή Θεωρία των Τύπων), ο λογισμός των κατασκευών (calculus of constructions) του Κοκάν, που επιτρέπει εξαρτώμενους και πολυμορφικούς τύπους, και φυσικά η HOL.