Вывод формальный. Формальным выводом высказывания (формулы) Д из множества исходных посылок Г в формальной (логической) систе­ме S с аксиомами Ai...An и прави­лами вывода Ki...Rm наз. последова­тельность высказываний (формул), каждое из к-рых есть или ак­сиома, или одна из посылок Г, или непосредственно выводима из пред­шествующих ей в выводе высказы­ваний (формул) по одному из правил Ri...R,n. Последнее высказы­вание (формула) этой последова­тельности и есть Д. Высказывание Д наз. выводимым из данных посы­лок Г заключением или конечной формулой вывода. Говорить о вы­воде Д имеет смысл только как о выводе Д в данной системе. Таково синтаксическое понятие выводимо­сти. Отношение выводимости рас­сматривается и в семантическом смысле: Д логически следует из Ар-.А,, и Г тогда, и только тогда, когда оно выполняется для каждой интерпретации (Интерпретация и модель), в к-рой выполняются А,...А„ и Г.