Friedman D. P., Christiansen D. T. The Little Typer / D. P. Friedman, D. T. Christiansen, Cambridge, MA, USA: MIT Press, 2018. 424 c.
Суждение - это позиция, которую кто-либо занимает по отношению к выражению. Википедия определяет суждение как мысль, в которой утверждается наличие или отсутствие каких-либо положений дел. В математической логике суждениям соответствую высказывания.
Формы суждений:
_____есть (является экземпляром)____(_____is a____)_____есть такой же экземпляр____, как и_____(_____is the same____as____)_____является типом (_____is a type)_____и____являются одним и тем же типом (_____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.
Нормальная форма выражения - это наиболее простой способ его записи. Любые два тождественных выражения имеют идентичные нормальные формы, и наоборот, любые два выражения, имеющие идентичные нормальные формы, являются тождественными. Нормальные формы выражений также определяются типом. Любое выражение, описанное типом, имеет нормальную форму, определенную этим типом.
Тождественность всегда определяется относительно типа, поэтому нормальные формы определены для конкретных типов. Любое сравнение, любая попытка определить идентичность двух выражений обязательно должна учитывать тип обоих выражений (см. вторую форму суждений).
У каждого типа также есть своя нормальная форма, являющаяся наиболее простым способом записи типа. Если два выражения являются одним и тем же типом, то у них идентичные нормальные формы, и наоборот.