GEB, стр. 210–212
Правила ТТЧ:
Спецификация: ∀u:x → x (можно убрать квантор и подставить терм)
Обобщение: x → ∀u:x (можно вернуть квантор)
Обмен: ∀u:~x ↔ ~∃u:x
Существование: от "2 простое" к "∃ простое"
Следование: r=t → Sr=St
🌀 Правила начинают приближаться к рассуждениям математиков.