возможность/интуиция различать и отделять вызвала к жызни натуральные числа с ихним дискретным вполне упорядочением далеко ДО восхождения формализма, хотя как раз эмпиризм материальных (!) знаков придаёт формализму особые якобы убедительность и "строгость" именно благодаря наглядной реализации абстрактной интуиции об различении и отделимости; потому формализм всё-таки вторичен и не может переплюнуть фундаментальную содержательную интуицию, на которой сам зиждется
Мне трудно, ув.Хайдук, делать заключения о "вторичности" и протчая касательно такой материи, как интуиция.
Собссно, это схоластика.
Ну пусть будет вторична. Что это меняет...
наглядная убедительность эмпирического автоматизма формализма не должна заслонять глубинную первичность концепции о вполне упорядоченной дискретности конечного
эмпирический автоматизм безошибочен и в этом смысле "строг" (с точностью до порою каверзной содержательной интерпретации своей), да и компы в нём преуспевают - в этом его бесспорная и большущая ценность
Если брать любимые Вами компы, то роль формализма там играет ассемблер
Можно разложить любой процесс на атомы и понять, что же точно он делает
Но писать на ассемблере мало кто любит и в этом полная аналогия с формальной математикой
Декомпилировать же код в более высокий уровень однозначно уже не получится обычно
И понимать, что же точно происходит в программе, написанной на языке высокого уровня уже нельзя. Когда например garbage collector запустится... Этого точно программа уже не контролирует. Поэтому правильно ли она работает, покрывается только тестами, что по сути и есть эмпирика.
Это опять же почти прямая аналогия.
Вы занимаетесь схоластикой, ув.Хайдук. И что Вы хотите доказать, совершенно неясно.
Есть разные уровни и математики и программ для компов. Вот и фсё.
Точными являются только формальные подходы, но они очень громоздки.
думаю, что аналогия с ассемблером неудачная, поскольку в математике исторически формализма мат. логики не было, тот вырос довольно поздно в попытках прецизировать рассуждения и бороться со всё более усложняющимися доказательствами - сколько уже "громких" теорем годами сидит в подвешенном состоянии, потому что эксперты не в силах придти к консенсусу насчёт их корректности, тут даже сам формализм не смог помочь, поскольку у самого те же проблемы громоздкости, запутанности и подверженности тупым ошибкам. Если что-то (формализм, то бишь) никогда не было реализовано и опробовано, то как можем быть уверены, что оно сработает или что вообще существует/достижимо? Где стандартный формализм, дабы применить к любой трудной анонсированной теореме, над которой эксперты барахтаются годами?
казалось бы, что по идее такой формализм должен обитать в абсолютном мире-пещере Платона, но не думаю, что сам Платон нашёл бы тому место в своём раю-пещере...
думаю, что аналогия с ассемблером неудачная, поскольку в математике исторически формализма мат. логики не было
А это неважно, что было исторически. Может для кого, кроме Бейсика ничего и нет
Главное, что лежит в основе
Сейчас формализм есть и по сути эквивалентен энтому ассемблеру
Известные учёные и их открытия
30 Сен 2018 12:36 #731
инфолиократ
Vladimirovich wrote:
Хайдук wrote:
думаю, что аналогия с ассемблером неудачная, поскольку в математике исторически формализма мат. логики не было
А это неважно, что было исторически. Может для кого, кроме Бейсика ничего и нет
Главное, что лежит в основе
Сейчас формализм есть и по сути эквивалентен энтому ассемблеру
У формализма - собственная гордость: Я прав.
У практицизма - есть тоже своя гордасть: Я нужнее.
У ЯВУ (языка высокого уровня) - тоже: Я - главнее. (Без обыкновенного национального языка не обойтись).
Вывод: как в геометрии (поправьте, если ошибаюсь) за первооснову можно было брать
1. точку
2. линию
3.плоскость.
И потом имея одно понятие легко определять остальные. И что лучше: набор точек= линия ИЛИ пересечение линий=точка?
Все триедино. З павагай да неабыякавых
Сейчас формализм есть и по сути эквивалентен энтому ассемблеру...
Точными являются только формальные подходы, но они очень громоздки.
a микропрограммы/firmware учитываете? ассемблер их включает или исключает?
точность внушают дискретность, конечность и прежде всего ... эмпиричность двух предыдущих, но эти две намного фундаментальнее (своей) эмпиричности; настоящая точность определяется ещё сугубо неформальным смыслом/содержанием эти эмпирические, дискретные и конечные знакосочетания неизбежно наделены, АТО точность их самих по себе тривиальна.
a микропрограммы/firmware учитываете? ассемблер их включает или исключает?
Какая разница?
Хайдук wrote:
точность внушают дискретность, конечность и прежде всего ... эмпиричность двух предыдущих, но эти две намного фундаментальнее (своей) эмпиричности; настоящая точность определяется ещё сугубо неформальным смыслом/содержанием эти эмпирические, дискретные и конечные знакосочетания неизбежно наделены, АТО точность их самих по себе тривиальна.
Это достойно пера Хайдеггера, но я ничего не понял
формализьму влепили некую как-бы идеальную, абсолютную точность/строгость, чуть ли не со стен рая-пещеры Платона так никогда и не слезал ; мне это представляется неким обольщением, заманчивым, но обманчивым, ускользающим и недостижимым миражОм
формализьму влепили некую как-бы идеальную, абсолютную точность/строгость, чуть ли не со стен рая-пещеры Платона так никогда и не слезал ; мне это представляется неким обольщением, заманчивым, но обманчивым, ускользающим и недостижимым миражОм
Вот попробую объяснить на пальцах ( хотя Григорий и рассердится )
Пусть у нас есть некие схемы для знакосочетаний
Как у классиков
CF1. Если А и В—соотношения теории J, то \/АВ есть соотношение теории J.
Для простоты - у нас есть слова. Слово легально (соотношение), если он находится в некотором словаре
Пусть наша схема гласит - если мы меняем в слове 1 или две буквы, и новое слово легально, то из А следует B
Итак
брага
крага
драка
дойка
водка
Это легальный вывод ( доказательсттво теории J)
Имеет ли значение значение данных слов в нашей теории?
НИКАКОГО.
Главное, что они есть в словаре
"эмпирики" нет, но и тривиальности зашкаливает , комбинаторика, теория (натуральных) чисел и ... программирование компов тоже могут похвастаться железными конструкциями наподобие сферху.
полагаю, что реальный формализм призван решать задачи гораздо более громоздкие, запутанные и концептуально (!) каверзные
с помощью формальных систем даже результат Гёделя о неполноте получено компом (!), но я хотел бы видеть как формализм поможет отсудить правильны ли, скажем, давеча новопреставленные решения таких гипотез как abc или Римана, скажем?
с помощью формальных систем даже результат Гёделя о неполноте получено компом (!), но я хотел бы видеть как формализм поможет отсудить правильны ли, скажем, давеча новопреставленные решения таких гипотез как abc или Римана, скажем?
Я уже говорил, что формализм это чисто потенциальная возможность.
А не практический метод. Ибо усилий стоит немеряно.
Напишите программу по переводу математического текста в бурбаковский формализм и проверку на соответствие схемам и аксиомам
И enjoy
Воеводский, кстати,последние годы жизни посвятил работе по формальной записи математических доказательств - чтобы их можно было проверять автоматически(мечта Лейбница) - "унивалентные основания".
не уверен, к сожалению, что даже они смогут убедить - слишком много и долго читал и думал, дабы надеятся на логическую панацею, пришёл к выводу, что такой не существует в принципе
это частный случай в море численных решений, а логика вообще любых задач это океан... forget about it, избежать ошибок при громоздкой формализации не проще, чем для обычных громоздких рассуждений, недаром все гламурные "доказательства" давеча в математике подвешены годами уже, а эксперты суетятся вокруг в нерешительности...