Friedman D. P., Christiansen D. T. The Little Typer / D. P. Friedman, D. T. Christiansen, Cambridge, MA, USA: MIT Press, 2018. 424 c.

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

Формы суждений:

1. _____ есть (является экземпляром) ____ (_____ is a ____)
2. _____ есть такой же экземпляр ____, как и _____ (_____ is the same ____ as ____)
3. _____ является типом (_____ is a type)
4. _____ и ____ являются одним и тем же типом (_____ and ____ are the same type)

Тип - это выражение, описывающие другие выражения.

Предложения (высказывания) получают свои значения от тех, кто понимает их. Они фиксируют наши мысли, а мысли более важны, чем слова, которыми их выражают.

Sentences get their meaning from those who understand them. The sentences capture thoughts that we have, and thoughts are more important than the words we use to express them.

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

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

У каждого типа также есть своя нормальная форма, являющаяся наиболее простым способом записи типа. Если два выражения являются одним и тем же типом, то у них идентичные нормальные формы, и наоборот.