oleg.kНу если вы так ударяетесь в метаматематику равенства, то тут можно поискать какой-то интуиции в конструктивной математике. Можно считать, что нет, равенство не определено (и не будет никем записано) для пары каких попало вещей, а обе эти вещи должны быть в каком-то одном и том же типе вещей. И что предполагается, что для каждого такого типа вещей мы можем установить, принадлежит ему вещь или нет, и взяв пару вещей, про которые мы установили, что они из него, установить, равны они или нет; при этом такая процедура должна удовлетворять аксиомам отношения эквивалентности. При этом нет нужды сковывать себя какими-то маленькими формальными теориями типа
Слева у меня интеграл из анализа, а справа у меня операция
из аддитивной абелевой группы вещественных чисел.
но и не нужно считать, что всё погружено в именно ZF(C) (пока не понадобится что-то специфическое именно из ZF(C)). Покуда мы оперируем вещами лишь в пределах соглашений с другими математиками, как ими оперировать, и вообще рассматриваем такой круг вещей, как и они, в таком околоконструктивном смысле, что мы имеем довольно твёрдую надежду, что разберём, что что означает и т. д., не нужно пытаться формализовать. Формализовать всю математику как она сейчас есть — довольно безнадёжно. А иметь в виду, почему рассуждения могут быть некорректными, а почему не могут — полезнее.
Вот например мы строим анализ, используя вещественные числа; мы определяем интеграл от функции
так, чтобы он был вещественным числом, ну и тогда нет никаких проблем спрашивать о равенстве его сумме двух вещественных чисел, которая тоже вещественное число. Нам не нужно думать о том, что слева функция каких-то аргументов и справа функция других аргументов, сама формальная математика оперирует как исходными понятиями выражениями и переменными. Слева число, зависящее быть может от того и сего, и справа число, зависящее быть может от третьего, и факт равенства их обоих зависит от всего этого сразу, ничего более хитрого.
Да, можно
гипотетически попасть в ситуацию, где спрашивается о равенстве двух штук, которые как будто действительно из разных миров. Вот в таком случае нужно собраться с людьми вместе и подумать. В каждом конкретном наверно отдельно, вряд ли тут можно сказать что-то философическое сразу про все. Они выглядят очень редкими.
Но обычной пресуппозицией должно быть, что равенство — это совпадение всех свойств, как придумал Лейбниц. То есть
тогда и только тогда, когда выражения
обозначают одну и ту же штуку: тогда и симметричность очевидна, и рефлексивность, и транзитивность, и подстановка. Когда же непонятно, с какой точностью рассматривать штуки, достаточно убедиться, что они определяются через такие штуки, про которые мы уверены, когда они равны, а когда нет (см. верх поста) и какие они вообще бывают — вот например натуральные числа или строки над каким-то конечным алфавитом, или функции между такими понятными вещами и т. д., или наконец объекты какой-то формальной теории (описание которой нами считается ясным и однозначным!), где есть символ
, ведущий себя сообразно отношению равенства.