Чем "равно по определению" отличается от "равносильно"?

[_Ivana]

По моим заблуждениям, значки $\Rightarrow$, $\Leftarrow$ и $\Leftrightarrow$ являются символами операций логического вывода (по правилам той логики, которая по умолчанию принята в данном контексте рассуждений), могут связывать значения только одного типа - булевского, и только одного значения - истина. Знаки определения $\stackrel{\text{def}}=$ и тождественности $\equiv$ могут связывать любые объекты, отношения и операции любого типа в любой формальной системе, при этом определение подразумевает введение новой конструкции и конструктивное описание ее построения на основе базовых и ранее определенных конструкций данной системы, а тождество всегда (?) требует доказательства. Знак $=$ обозначает единственный вид бинарных отношений любых объектов любой системы, являющийся истинным при применении к одному и тому же объекту и ложным в противном случае.

С удовольствием скорректирую свои заблуждения в результате обсуждения.

[Aritaborian]

Munin, вы совершенно правы, а я и в самом деле свалил всё в одну кучу.

[arseniiv]

provincialka в сообщении #766018 писал(а):

Например, постоянную функцию можно описать равенством $y = 2$. Но равносильно ли оно равенству $2=y$?

Это же сокращение от $\forall x\in\operatorname{dom} y \mathrel. y(x) = 2$ или чего-то подобного, зависит от теории. В такой записи можно переставить $y(x)$ и $2$. Ничего бы не мешало менять их местами и в исходном, но там просто много способов понимания, из-за чего часто константность функции записывают не через $=$, а через $\equiv$: $y \equiv 2$. Хотя я бы в данном случае писал $y = x \mapsto 2$, например.

_Ivana в сообщении #766229 писал(а):

С удовольствием скорректирую свои заблуждения в результате обсуждения.

Вы намешали в одну кучу выводимость, истинность и то, что теория до определения и теория после — две разные (в первой — аксиомы $\mathcal A$, во сторой — $\mathcal A \cup\{\mathrm{NewDef}\}$). Вряд ли я смогу нормально описать, как это распутывать; надеюсь, кто-нибудь ещё заглянет.

Насчёт употребления $:=$ и $:\Leftrightarrow$ — мне казалось, каждый из них заменяет соответственно $=$ для термов и $\Leftrightarrow$ для предикатов.

[provincialka]

arseniiv, конечно, сокращение. Я имею в виду "школьный" вариант. Я думаю, что утверждения, содержащие знак "равно" могут иметь весьма разные смыслы. Вот, например, дифференциал функции $f$ часто обозначают не $df$, а $dy$, это удобно (инвариантность формы дифференциала). Я уж не говорю о записи $f(x)=o(g(x))$, которая равенством не является.

Даже простое на вид равенство может таить в себе весьма сложный смысл. Например, что такое $x=\sqrt2$? Или $t=\ln 2$. Казалось бы, в правых частях стоят просто числа, но на самом деле они существуют не сами по себе, а как результат пополнения по непрерывности.

[_Ivana]

arseniiv, спасибо и на том, просто буквально вчера прочитал Энциклопедию юных сурков Пособие к курсу лекций по темам "Логика естественных рассуждений" для студентов Санкт-Петербургского Университета Культуры и Искусств (СПбГУКИ), и начал задумываться над этими вопросами

provincialka в сообщении #766345 писал(а):

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

Имхо, при конструктивном подходе - да, а при аксиоматическом - сами по себе.

[provincialka]

Не очень поняла про аксиоматический подход. Я, наверное, неаккуратно выразилась. Существуют они конечно, сами по себе, но вот какое именно чило считать значением записи $\ln2$? И значением любой другой элементарной функции, кроме дробно-рациональной. За этой простой записью стоит целая теория, которая последовательно, начиная с простейших случаев, строит значения каждой функции, причем используется предельный переход и доказывается его корректность.
Про конструктивно-неконструктивно я не разбираюсь, говорю только о том, что проходят на 1 курсе.

[_Ivana]

Я тоже не разбираюсь, если бы разбирался - не писал бы здесь
Но давайте к 1 курсу: почему операция деления вам более симпатична, чем, например, функция натурального логарифма? В обоих случаях натуральные значения мы получаем нечасто, а бесконечные дроби разве не такой же предельный переход, как ваши примеры? Чем, собственно, "рациональность" чисел, как возможность их конструктивного построения через операцию деления натуральных аргументов, лучше, например, "логарифмичности", как построения через функцию логарифма? Ну, кроме исторического аспекта появления, конечно.

[provincialka]

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

[arseniiv]

deleted

[Xaositect]

_Ivana в сообщении #766583 писал(а):

Но давайте к 1 курсу: почему операция деления вам более симпатична, чем, например, функция натурального логарифма? В обоих случаях натуральные значения мы получаем нечасто, а бесконечные дроби разве не такой же предельный переход, как ваши примеры? Чем, собственно, "рациональность" чисел, как возможность их конструктивного построения через операцию деления натуральных аргументов, лучше, например, "логарифмичности", как построения через функцию логарифма? Ну, кроме исторического аспекта появления, конечно.

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

[_Ivana]

provincialka в сообщении #766587 писал(а):

боюсь, что мы далеко ушли от исходной темы

Да, ушли, но и тема к этому провоцирует. Надеюсь, ТС не обидится.

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

[Xaositect]

_Ivana в сообщении #766605 писал(а):

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

Да, вот проверка через приближения может доказать только неравенство, и не может равенство, а распутывание не работает на примерах типа $e^{5e^2} - 2e^{2e^2} - 1$. Так что в итоге пока доказанного алгоритма нет, есть только такие, у которых доказательство корректности опирается на недоказанные теоретико-числовые гипотезы. Можете почитать http://math.mit.edu/~tchow/closedform.pdf‎ , там на начальном уровне об этом сказано и ссылки на обзоры есть.

[ewert]

Xaositect в сообщении #766600 писал(а):

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

Мешает. Что значит "символически" -- на каком множестве-то?

[Xaositect]

ewert в сообщении #766610 писал(а):

Мешает. Что значит "символически" -- на каком множестве-то?

1. Любое рациональное число является термом.
2. Если $a$ и $b$ --- термы, то $a+b$, $ab$, $a/b$, $exp(a)$ и $ln b$ - также термы.
3. Других термов нет.

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

[ewert]

Xaositect в сообщении #766612 писал(а):

$exp(a)$ и $ln b$ - также термы.

Допустим, термы. И чему же они соответствуют? Например: чем $e^x$ отличается от $2^x$ ?

Xaositect в сообщении #766612 писал(а):

А по другому мы не умеем.

А оно нам нужно?

Ведь любая функция интересна лишь постольку, поскольку её значения можно хоть как-то, но посчитать. Уж экспонента-то точно лишь.