система, неинтерпретированное исчисление , класс выражений (формул) которого задаётся обычно индуктивно v посредством задания исходных ('элементарных', или 'атомарных') формул и правил образования (построения) формул, а подкласс доказуемых формул (теорем) v посредством задания системы аксиом и правил вывода (преобразования) тео