Бурбаки - тау и надстрочные линии

[Qurum]

Здравствуйте.
В книге "Основные структуры анализа" 1965 года издания запись $\tau_x(A)$ обозначает знакосочетание, полученное записью $\tau A$, соединением ведущего знака $\tau$ связью с каждым экземпляром буквы x в A и заменой иксов пустыми квадратиками. Как будет выглядеть знакосочетание $\tau_y(\vee sxy \tau_x(syx))$, где s - специальный знак веса 2, x и y - буквы? Надстрочные линии могут пересекаться? Из книги это не очевидно.

Попутно хочу разузнать о знаке тау и связях. Каким образом Бурбаки к ним пришли, является ли это их собственной разработкой или уже было кем-то придумано до них? Используются ли тау и связи в математической логике в наше время, или им на смену пришло что-то более современное? Если посоветуете литературу на эту тему, то буду признателен.

[Sonic86]

Qurum в сообщении #700640 писал(а):

Надстрочные линии могут пересекаться?

Могут.

Qurum в сообщении #700640 писал(а):

Попутно хочу разузнать о знаке тау и связях. Каким образом Бурбаки к ним пришли, является ли это их собственной разработкой или уже было кем-то придумано до них? Используются ли тау и связи в математической логике в наше время, или им на смену пришло что-то более современное?

Насколько я помню, это просто попытка явно показать, что переменная - немая, связанная.
В книгах по матлогике я такие значки не встречал.

Qurum в сообщении #700640 писал(а):

Как будет выглядеть знакосочетание $\tau_y(\vee sxy \tau_x(syx))$, где s - специальный знак веса 2, x и y - буквы?

Я в ТеХе такие штуки рисовать не умею Все равно теперь должно быть понятно.

[Qurum]

Sonic86, спасибо. То есть такое тау нигде, кроме как у бурбаков, не встречается?

[Sonic86]

Ну чтоб утверждать, что оно нигде не встречается, надо прочесть все книги, и убедиться, что в каждой тау нету Я, конечно, все не читал, но в том, что читал, тау нигде не видел, кроме бурбаков.

[Qurum]

Выяснилось, что Бурбаки использует созданное Гильбертом эпсилон-исчисление, только вместо знака эпсилон использует знак тау.
http://en.wikipedia.org/wiki/Epsilon_calculus
http://rudocs.exdat.com/docs/index-14834.html

[NQD]

Даже сами Бурбаки не используют свой тау-символ нигде, кроме "Теории множеств", так что можно не напрягаться. Просто читайте $\tau_x(A)$ так: "такой $x$, что $A$".

[AGu]

NQD в сообщении #701037 писал(а):

Даже сами Бурбаки не используют свой тау-символ нигде, кроме "Теории множеств", так что можно не напрягаться.

Я тоже долгое время так считал. Но в последнее время, размышляя над формализацией частично определенных термов (коих в обычной математике пруд пруди), стал склоняться к тому, что это тау, -- которое, кстати, частенько является йотой: $\iota x\,\varphi(x)$, -- вещуга весьма недооцененная. Формалисты до нее пока не дотянулись: им либо лень, либо скучно, либо просто есть дела поважнее.

[JMH]

Я, вобще-то, тоже считаю, что обозначение удачное, но, как мы знаем, порой приживаются не самые рациональные или самые удобные вещи...

AGu в сообщении #702695 писал(а):

...это тау, -- которое, кстати, частенько является йотой: $\iota x\,\varphi(x)$...

А что за йота такая и как случилось, что тау ею является "частенько", а, например, не всегда или никогда?

[AGu]

JMH в сообщении #702764 писал(а):

А что за йота такая и как случилось

Йота -- самая обычная. Пошла она, по всей видимости, от классиков -- Рассела, Гильберта, Бернайса...

[arseniiv]

Представляете, какая получится горячая смесь, если соединить их с $\lambda$!

[Joker_vD]

arseniiv
А зачем? Если мне в $\lambda$-исчислении совсем захочется избавиться от связанных переменных и проблем с подстановкой, я просто возьму индексы де Брёйна. В любом случае, просто это не делается.

[arseniiv]

Я как раз о внесении $\lambda$ в логику, а не наоборот. Или ничем не поможет? (Вот сказал, а сам не могу теперь понять, как это туда прилепить. )

-- Пт мар 29, 2013 23:39:04 --

А связанные переменные ведь всё равно будут, иота их ведь тоже связывает.

Дошло! Наверно, вы подумали, что я про обозначения с тау?