Доказательность не только не заканчивается функциями, но даже более того — она с них и не начинается.
Просто некоторые ограниченные бестолочи, которые кроме функций ничего не знают и знать не хотят, привнесли когда-то в университетские круги эту сомнительную моду.
У реальных бойцов данного фронта в ходу две аббревиатуры: SAT и SMT, ну и практическое воплощение SMT–сольвера — https://github.com/Z3Prover/z3.

PS. Насколько я, дилетант в данном деле, понимаю, начинать путь следует с предикативного исчисления, а не с функанов-теоркатов, и тем более не с ТФКП. Могу, конечно, и ошибаться.

Доказательность не только не заканчивается функциями, но даже более того — она с них и не начинается.
Просто некоторые ограниченные бестолочи, которые кроме функций ничего не знают и знать не хотят, привнесли когда-то в университетские круги эту сомнительную моду.
У практикующих бойцов данного фронта в ходу преимущественно две аббревиатуры: SAT и SMT, ну и конечно практическое воплощение сольвера — z3 (https://github.com/Z3Prover/z3).

PS. Насколько я, дилетант в данном деле, понимаю, начинать путь следует не с функанов-теоркатов, и тем более не с ТФКП, a с предикативного исчисления, карт Карно, синтеза микропрограммных автоматов и т.д. Могу, конечно, и ошибаться.

PPS. Про то, что ТФКП зачем-то проходят (мимо) в ВУЗах, а потом забывают за ненадобностью — это Вы зря. Оно полезно в цифровой обработке сигналов и в радиосвязи.

PPPS. Обратите также внимание, что z3 solver написан не на каком-нибудь Лиспе или Хаскелле, а вполне себе на прагматичном C++.