Rachunek predykatów drugiego rzędu – rozszerzenie logiki pierwszego rzędu wzbogacone o kwantyfikatory po zmiennych, które przebiegają relacje.
Istnieją odmiany logiki drugiego rzędu w których dopuszczalny zbiór kwantyfikatorów ograniczony jest jedynie do określonych rodzajów relacji, np. monadyczna logika drugiego rzędu jest częścią logiki drugiego rzędu obejmującym jedynie kwantyfikatory nad relacjami unarnymi (zbiorami).
Definicja formalna Każda formuła atomowa logiki pierwszego rzędu jest formułą logiki drugiego rzędu.
Co więcej:
Jeśli φ jest formułą logiki drugiego rzędu to ~φ jest formułą logiki drugiego rzędu Jeśli φ i ψ są formułami logiki drugiego rzędu to φ ∧ ψ jest formułą logiki drugiego rzędu Jeśli φ jest formułą logiki drugiego rzędu to ∃xφ jest formułą logiki drugiego rzędu dla dowolnej zmiennej x Jeśli φ jest formułą logiki drugiego rzędu to ∃Rnφ jest formułą logiki drugiego rzędu dla dowolnej n-argumentowej zmiennej relacyjnej R