Изменения

# <tex> a + 0 = a </tex>

# <tex> a + b' = (a + b)'</tex>

{{Лемма

|proof = Упражнение {{TODO | t = ща будет}}

}}

Но данная аксиоматика сформулирована неформально, поэтому мы не сможем доказать никаких содержательных утверждений про нее, пользуясь формальными средствами. Поэтому нам нужно эту конструкцию как-то объединить с исчислением предикатов, чем мы сейчас и займемся.

* Маленькими латинскими буквами a,b,... (возможно, с индексами) будем обозначать индивидные переменные.

* К логическим связкам добавляются такие: (<tex>=</tex>) &mdash; двуместный предикат, (<tex>+</tex>) и (<tex>\cdot</tex>) &mdash; двуместные функции, и (<tex>'</tex>) &mdash; одноместная функция. Все левоассоциативное, приоритеты в порядке убывания: (<tex>'</tex>), потом (<tex>\cdot</tex>), потом (<tex>+</tex>). Все логические связки имеют приоритет ниже. (Например, <tex>a= b'+b'+c \cdot c \& b = c</tex> надо интерпретировать как <tex>(a = (((b') + (b')) + (c \cdot c))) \& (b = c)</tex>)