Например, в гильбертовом (классическом) исчислении высказываний в его представлении Клини:

доказательство дистрибутивности дизъюнкции относительно конъюнкции только в одну сторону будет иметь 25 следующих шагов:

Вот что об изучении исчислений в математической логике пишут академик Российской академии наук Ю.Л. Ершов и профессор кафедры алгебры и математической логики Новосибирского государственного университета Е.А. Палютин (Ершов Ю.Л., Палютин Е.А. Математическая логика. – 6-е изд., испр. – М.: ФИЗМАТЛИТ, 2011. С.11. – ISBN 978-5-9221-1301-4): «Изучение исчислений составляет синтаксическую часть математической логики. Наиболее глубокое изучение (синтаксического) понятия доказательства в тех или иных исчислениях составляет самостоятельный раздел математической логики, который носит название теории доказательств. Наряду с синтаксическим изучением исчислений проводится также семантическое изучение формальных языков математической логики. Основным понятием семантики является понятие истинности для выражений (формул, секвенций и т. п.) формального языка. Семантические понятия также получили точные математические определения, что дало возможность систематического и строгого изучения различных понятий истинности. Классическая семантика языка исчисления предикатов составила весьма богатый раздел математической логики — теорию моделей, которая активно развивается, а ее методы и результаты успешно применяются и в других областях математики (алгебре, анализе). Основателями теории моделей являются А. Тарский и А. И. Мальцев».

Как заявляют авторы в их учебном издании «Математической логики»: «Изложение исчисления высказываний и исчисления предикатов не является традиционным и начинается с изучения секвенциальных вариантов исчислений натурального вывода (хотя традиционные исчисления также появляются здесь под названием гильбертовских). Основанием к этому являются: 1) возможность хорошего объяснения смысла всех правил вывода; 2) возможность более быстрого приобретения навыка формальных доказательств; 3) практическая возможность проделать все необходимые в курсе формальные доказательства в таких исчислениях. Многолетний опыт чтения старшим из авторов курса математической логики на математическом факультете Новосибирского государственного университета … показывает, что указанные выше возможности вполне реализуются».

Греческая "гамма" обозначает последовательность формул (возможно, пустую), греческие "фи", "пси", "хи" - произвольные формулы исчисления высказываний, готическая "эф" - тождественно ложную формулу

От себя замечу, что с эпистемологической и историко-научной точек зрения это учебное издание воплощает исходные принципы конструктивистского направления новосибирской школы математической логики.

О целях науки о доказательстве. Аристотель - один из величайших философов Древней Греции, по праву считающийся отцом-основателем логики, в дошедших до нас сочинениях не использует слово логика, но всегда говорит о науке о доказательстве или доказывающей науке. Термин логика для обозначения одного из разделов философии, наряду с физикой и этикой, впервые используют более молодые современники Аристотеля - философы-стоики, часть из которых были его учениками. Это обстоятельство свидетельствует о том, что изначально наука о доказательстве создавалась для того, чтобы изучающий ее приобрел знания о том, какие рассуждения являются правильными, а какие - нет, умел отличать правильные умозаключения от неправильных и приобрел способность целенаправлено, а не случайным образом, строить правильные или правдоподобные рассуждения.

Доказательство - это умозаключение, или рассуждение, то есть Всякое доказательство - это умозаключение, но Существуют такие умозаключения, которые не являются доказательствами. Предварительно заметим (поскольку, возможно, в ходе дальнейшего изложения нижеследующее утверждение потребует детализации и уточнения), что доказательством будем называть правильно построенное умозаключение (рассуждение), а неправильно построенное умозаключение (рассуждение) доказательством называть не будем.

Мы используем здесь приём, который называется явным родо-видовым определением - мы говорим: Доказательство - это правильно построенное умозаключение, и наоборот, правильно построенное умозаключение - это доказательство. Слова "доказательство" и "правильно построенное умозаключение (рассуждение)", как говорят, находятся в отношении тождества - то есть они имеют одно и то же значение, иными словами, обозначают одни и те же предметы. Используя грекоязычное заимствование из лингвистики, мы могли бы сказать, что это - синонимы, но с той поправкой, что они не имеют никаких различий.

Наше определение доказательства (того, что такое доказательство, или того, что называется доказательством) содержит определяемую часть - слово доказательство, и определяющую – словосочетание правильное умозаключение. И определяемая, и определяющая части определения выражаются понятиями. Кроме того, нужно заметить, что определение не является умозаключением, а представляет собой отдельно взятое утверждение, которое мы можем рассматривать как: 1) высказывание, истинное на некоторой предметной области; 2) допущение, необходимое для построения дальнейших рассуждений.

Сложносочинённые предложения «Всякое доказательство – умозаключение, но Существуют умозаключения, не являющиеся доказательствами» и «Доказательство – это правильно построенное умозаключение, и наоборот, правильно построенное умозаключение – это доказательство» не являются умозаключениями: в них нет тех предложений, которые выводились бы («получались») из других – в естественном языке на наличие умозаключения явным образом показывают выражения типа «следовательно», «значит», «поэтому». Предложения, предшествующие выражениям указанного типа называются посылками, а то предложение, которое следует за ним – заключением. В дальнейшем последовательность предложений естественного языка, в которых не встречается выражение, явным образом указывающее на наличие перехода от посылок к заключению (т.е. умозаключения), считать умозаключениями (или рассуждениями) не будем.

Другой особенностью посылок и заключения рассуждений является то, что они должны быть повествовательными предложениями – из побудительных предложений, выражающих эмоции или призыв к действию, или из вопросительных, выражающих заинтересованное ожидание разрешения некоторого неопределенного положения дел в известной предметной области, выводов делать не будем (разве что косвенным, как сказал бы Аристотель, «привходящим» образом) – например, призыв «Все на борьбу с Деникиным» может рассматриваться как свидетельство нехватки красноармейцев на фронте, а риторический вопрос: «Разве Волгоград не является городом-героем?» – как утверждение в форме вопросительного предложения.

"Виртуальная экскурсия"

О правильности и неправильности умозаключений и истинности и ложности высказываний.

Об умозаключениях (рассуждениях) мы будем говорить как о правильных либо как о неправильных - умозаключения не бывают истинными либо ложными (!).

О высказываниях, наоборот, говориться как об истинных либо ложных, но высказывания не бывают правильными либо неправильными (!).

Говорить на русском иначе - значит не обладать достаточным для науки о доказательстве знанием различий слов современного русского языка.
Слова "верно" и "неверно" (которые мы, например, часто использовали в школе при проверке правильности решения уравнений) двусмысленны - они могут употребляться и в значении правильно и истинно, и в значении неправильно и ложно (соответственно), поэтому их не следует использовать, чтобы избежать двусмысленности в строгих рассуждениях, в других случаях (например, когда двусмысленность целесообразна или контекст допускает очевидно однозначное прочтение) они окажутся вполне уместными и своевременными.

Когда мы говорим о высказываниях, то требуем, чтобы: во-первых, ни одно из них не могло быть одновременно и в одном и том же смысле истинным и ложным, то есть соответствующим и не соответствующим положению дел в рассматриваемой предметной области - это принцип противоречия; во-вторых, никакое высказывание не могло бы иметь какое-либо другое значение, кроме истина и ложь, иными словами, содержание высказывания может либо соответствовать реальному положению дел либо не соответствовать ему, и третьего не дано - tertium non datur - принцип исключённого третьего.

Когда мы говорим об умозаключениях (рассуждениях), то утверждаем, что: во-первых, одно и то же умозаключение в одном и том же отношении не может быть одновременно правильным и неправильным - в этом принцип противоречия; во-вторых, одно и то же умозаключение может быть либо правильным либо неправильным, третьего не дано - в этом принцип исключённого третьего.

Итак, мы определили доказательство как правильное умозаключение (рассуждение). В нашем случае сказать так всё равно, что сказать: "Мы определили понятие "доказательство" ". Заметим, что сегодня определения первого вида обычно называются реальными, а вторые - номинальными.
Примечание. Иногда в ходе занятий учителя ставят задачу, например: "дать понятие доказательству". Конечно, задачи подобного рода следует понимать в смысле предписания "дать определение понятию доказательство", поскольку буквально немыслящей сущности нельзя передать форму мышления.