aleatorius (
aleatorius) wrote2005-01-19 05:21 pm
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
Математик для физика -
это сумасшедший грамматик -который создаёт язык изучения языка - этакий искуственный интеллект познающий сам себя.
Тогда как для физика язык - есть коммуникация с реальностью - а заниматься всё время только подручными средствами - всё время совершенствуя приборы - и при этом не использовать по назначению - это кажется физику странным.
Т.е. тут вопрос соподчинения - для физика синтаксис подчинен семантике - а для математика - всё только сплошной синтаксис.
(Это всё оочень условно - нужна некая дихотомия была).
Тогда как для физика язык - есть коммуникация с реальностью - а заниматься всё время только подручными средствами - всё время совершенствуя приборы - и при этом не использовать по назначению - это кажется физику странным.
Т.е. тут вопрос соподчинения - для физика синтаксис подчинен семантике - а для математика - всё только сплошной синтаксис.
(Это всё оочень условно - нужна некая дихотомия была).
Автоматическая проверка доказательств?
Предположим, что доказательство формализовано тем или иным образом. Тогда можно построить такую метафору: док-во <-> программа, система проверки <-> компилятор. Что указывает на ошибочность док-ва (на метауровне, грамматические ошибки исключаем): использование недоказанных утверждений <-> обращение к несуществующим библиотекам, нарушение правил логического вывода <-> неправильный вызов функций и т.д.