kouzdra: A = A

A = A

scholar-vit@lj приводит пару цытат из Рэнд и Витгенштейна (вторая типа как "опровержение" первой), если поток сознания Рэнд imho просто не заслуживает разбора, то с Витгенштейном все забавнее:

"Вещь тождественна сама себе". Нет лучшего примера бесполезного утверждения.

Надо сказать, что Вики нам говорит:

Some basic logical properties of equality:
...
The reflexive property states: For any quantity a, a = a.

И таки да - отношение равенства является отношением эквивалентности, и рефлексивность - одно из определяющих свойств. Так что утверждение

(∀ A) A = A

не отличается глубиной, но и не бесполезно

(Добавить комментарий)

(Анонимно)
2013-11-01 10:24 (ссылка)

Если сравниваются только выражения одного типа, то кроме рефлексивности ничего и не надо. В теориях типов Мартин-Лефа равенство это индуктивное семейство:
data _==_ {A : Set}(a : A) : A -> Set where
refl : a == a

Симметричность, транзитивность и правило подстановки доказуемы.

Проблемы начинаются когда А является типом функций или универсумом. Тут основная рубка observational type theory vs. homotopy type theory.

(Ответить) (Ветвь дискуссии)

kouzdra
2013-11-01 12:14 (ссылка)

Традиционное определение равенства в математике вообще лейбницевское:

A = B iff (∀ P) P (A) ≡ P (B)

Из него естественно доказываются все свойства, но таки смысл рефлексивности все равно есть - в том, что (вместе с транзитивностью и симметричностью) равеноство является отношением эквивалентности.

(Ответить) (Уровень выше)

steinkrauz
2013-11-01 10:56 (ссылка)

Так и сам Витгенштейн говорит:
4.4611 Tautology and contradiction are, however, not senseless; they
are part of the symbolism, in the same way that “0” is part of
the symbolism of Arithmetic.

И вообще утверждение Витгенштейна имеет смысл в контексте дерева утверждений 5.5, а не само по себе.

(Ответить)