Birds and Frogs

[Slavomir Kaslev]

http://www.ams.org/notices/200902/rtx090200212p.pdf

--
Slavomir Kaslev

[Stefan Kanev]

Текст, кратко обяснение, нещо?

[Krasimir Angelov]

Интересно четиво. Класификацията на Жаби и Птици може да се приложи
към всяка наука.

2013/12/12 Slavomir Kaslev <slavomi...@gmail.com>:
> http://www.ams.org/notices/200902/rtx090200212p.pdf
>
> --
> Slavomir Kaslev
>
> --
> You received this message because you are subscribed to the Google Groups
> "Polyglot Quine" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to polyglot-quin...@googlegroups.com.
> To post to this group, send email to polyglo...@googlegroups.com.
> Visit this group at http://groups.google.com/group/polyglot-quine.
> For more options, visit https://groups.google.com/groups/opt_out.

[Krasimir Angelov]

Ето това ми беше по вкуса:

I tell you my guess, just to give you something to think about. I
consider it unlikely that string theory will turn out to be either
totally successful or totally useless.

Както и другите коментари по темата. Определено се вдига прекалено
много шум за струните, а алтернативните теории се игнорират. При
положение, че няма доказателства за която и да е от теориите, то те
следва да се изучават паралелно.


2013/12/12 Krasimir Angelov <kr.an...@gmail.com>:

[Boyko Bantchev]

> При
> положение, че няма доказателства за която и да е от теориите, то те
> следва да се изучават паралелно.

Там е работата, че „доказателства“ едва ли и ще има.
Теориите на физиците са модели и като такива, ако използването им
помага да се решават някакви задачи от практиката, те се смятат за
успешни, а ако не – отпадат. За „вярност“ няма как да се говори.
Все едно да кажем, че C++ е „верен“ език за програмиране, а Хаскел
не е, или обратното.

Дори и с математиката е донякъде така. Евклидовата геометрия „вярна“
ли е? Между другото Р.Пенроуз (математикофизик) например обича да
казва, че евклидовата геометрия е физическа теория. Изобщо
математиката също е в крайна сметка моделиране. Някои отричат, че
тя _открива_ каквото и да е обективно, смятайки че само _изобретява_
(модели).

[Krasimir Angelov]

На 12 декември 2013, 15:20, Boyko Bantchev <boy...@gmail.com> написа:
>> При
>> положение, че няма доказателства за която и да е от теориите, то те
>> следва да се изучават паралелно.
>
> Там е работата, че „доказателства“ едва ли и ще има.

Вярно. Трябваше да кажа "наблюдения" или нещо такова. Експерименти
които подкрепят или отхвърлят която и да е от алтернативите. Иначе ако
задълбаем ще стигнем до научните революции на Thomas Kuhn:

http://en.wikipedia.org/wiki/The_Structure_of_Scientific_Revolutions

Между другото за хора с философски наклонности, книгата на Kuhn е
интересно четиво. Докато я четеш си мислиш до колко науката се
различава от религията.

[Stefan Kanev]

Между другото за хора с философски наклонности, книгата на Kuhn е
интересно четиво. Докато я четеш си мислиш до колко науката се
различава от религията.

Added to wish list.

[cutthroat]

 

Там е работата, че „доказателства“ едва ли и ще има.
Теориите на физиците са модели и като такива, ако използването им
помага да се решават някакви задачи от практиката, те се смятат за
успешни, а ако не – отпадат.  За „вярност“ няма как да се говори.

Не съм напълно съгласен.  Във физиката говорим за експериментални доказателства.  Например, стандарният модел е успешен защото имаме доказателства, че явленията които предрича наистина се проявяват.  Някои негови аспекти като съществуването на антиматерия, Хигс бозони и т.н. едва ли ще имат скорошни приложения.  Те са без значение.

Друг пример са Нютоновата и Айнщайновата теории за гравитацията.  Нютоновата стотици години е стояла без приложения.  Айнщайновата не толкова много, но дори тя в създаването си е била доста несвързана с практиката.  Днес, редица съвременни технологии не биха били възможни без тях.  Но отново, тези теории са били успешни не заради скорошните им приложения, а защото са били експериментално потвърдени.  Например, те описват планетните орбити със доста задоволителна точност.

 

Все едно да кажем, че C++ е „верен“ език за програмиране, а Хаскел
не е, или обратното.

Това сравнение според мен е неуместно, защото тук говорим за неща изкуствено създадени.  Физиката е естествена наука.  Тя изучава обикалящият ни свят.  Хаскел и C++ са инструменти за изразяване на изчислителни процеси.  Уместно сравнение би било с хипотезата на Чърч и Тюринг, макар и да нямам идея какво би било експериментално доказателство в нейна полза.

 

Дори и с математиката е донякъде така.  Евклидовата геометрия „вярна“
ли е?  Между другото Р.Пенроуз (математикофизик) например обича да
казва, че евклидовата геометрия е физическа теория.  Изобщо
математиката също е в крайна сметка моделиране.

Може би изглежда противоречиво, но съм съгласен че математиката до голяма степен е физика.  Разликата е, че при нея експериментите са логически.  Арнолд твърди, че математиката е частта от физиката, в която експериментите са евтини.  Въпреки, че светът който изследва математиката изглежда просто плод на човешкото съзнание, т.е. е изкуствен, това не е съвсем така.  Голяма част от абстрактната математика всъщност има връзка със реални физически явления.  В посочената статия, Дайсън дава чудесен пример с комплексните числа.

А относно, че няма вярна геометрия, да, всичко в математиката е относително.  Относително спрямо базовите постулати, т.е. аксиомите които приемаме за верни.  На пръв поглед може да си помислим, че работата на естествената наука е доказва абсолютни твърдения, но според мен това е едно нереалистично изискване.  Най-малкото, защото едва ли ще някога ще имаме пълно познание за света около нас.  Това към което може да се стремим е все по-точно приближение и приложимост в по-широк кръг от ситуации.

[Boyko Bantchev]

> Не съм напълно съгласен. Във физиката говорим за експериментални
> доказателства.

Бих ги нарекъл по-скоро не доказателства, а свидетелства за
адекватността на модела. Ако се търси да се докаже нещо, то е точно
това, че моделът „работи“. Но това не са формалните или поне
формализуеми доказателства на съвременния математик, а свидетелства,
които получаваме от опита, и такива свидетелства никога не са
окончателни. Потвърждаването на теория чрез опит не изключва
възможността за друг опит, който да намери пукнатини в теорията.
Обаче безкрайността на множеството от простите числа е окончателно
_доказан_ факт, който не може да бъде опроверган от опита.

> тези теории са били успешни не заради скорошните им приложения, а
> защото са били експериментално потвърдени

Именно, подкрепени от опита, но не доказани в строгия смисъл. И нека
уточня, че когато по-рано казах „задачи от практиката“ нямах предвид
непременно „приложения“ в тесния смисъл, а изобщо пресичането на
теорията с практиката. В частност и поставянето на експерименти за
проверяване на теориите, и използването на теории за опознаване на
природата, т.е. използването на едни модели за създаване на други,
са също „задачи от практиката“.

> Това сравнение според мен е неуместно, защото тук говорим за неща
> изкуствено създадени. Физиката е естествена наука. Тя изучава
> обикалящият ни свят. Хаскел и C++ са инструменти за изразяване на
> изчислителни процеси.

Езиците за програмиране са не повече изкуствени инструменти, отколкото
са физическите модели. И едните, и другите са метафори, създадени от
нас за активно възприемане на съответната част от света под определен
ъгъл. Ако се окаже, че вършат работа, ползваме ги. Едни се оказват
дълготрайни, други не – опитът ги пресява! Дори дълготрайните обаче
биват уточнявани, усъвършенствани, за да се съгласуват все по-добре с
нуждите и опита ни.

~~~~

Понеже стана дума за книги с, да го наречем, философски поглед върху
математиката и физиката, да добавя и аз някои, които са ме впечатлили:

http://www.ozon.ru/context/detail/id/5134264
http://www.ozon.ru/context/detail/id/17513376
http://www.amazon.co.uk/dp/0099440687
http://www.amazon.co.uk/dp/0743294068

Последната от тези, както впрочем и книгата на Кун, която спомена
Краси, е преведена и на български. Предпоследната е най-обемната и
най-амбициозната от няколкото книги на Пенроуз, в които той се опитва
да обясни света на полупопулярен език. Впрочем всичките книги на
Пенроуз са тежки за четене, защото стилът му е изморителен, а
повествованието така разпиляно, че лесно се губи нишката, ако я има.

[Slavomir Kaslev]

2013/12/12 Krasimir Angelov <kr.an...@gmail.com>

Ето това ми беше по вкуса:

I tell you my guess, just to give you something to think about. I
consider it unlikely that string theory will turn out to be either
totally successful or totally useless.

Както и другите коментари по темата. Определено се вдига прекалено
много шум за струните, а алтернативните теории се игнорират. При
положение, че няма доказателства за която и да е от теориите, то те
следва да се изучават паралелно.

Докато още не знаем какъв е отговора, дори непълна и частична информация 

за него е полезна. Теория на струните може да не е отговора, но има правилни

идеи. Според мен, (a wild guess) окончателната теория ще има повече общо с

теория на числата и групите отколкото с теория струните и ще е написана на

homotopy type theory език. Но докато не знаем, всички идеи за ценни.

[Slavomir Kaslev]

2013/12/12 cutthroat <silent.c...@gmail.com>

 

Там е работата, че „доказателства“ едва ли и ще има.
Теориите на физиците са модели и като такива, ако използването им
помага да се решават някакви задачи от практиката, те се смятат за
успешни, а ако не – отпадат.  За „вярност“ няма как да се говори.

Не съм напълно съгласен.  Във физиката говорим за експериментални доказателства.  Например, стандарният модел е успешен защото имаме доказателства, че явленията които предрича наистина се проявяват.  Някои негови аспекти като съществуването на антиматерия, Хигс бозони и т.н. едва ли ще имат скорошни приложения.  Те са без значение.

Друг пример са Нютоновата и Айнщайновата теории за гравитацията.  Нютоновата стотици години е стояла без приложения.  Айнщайновата не толкова много, но дори тя в създаването си е била доста несвързана с практиката.  Днес, редица съвременни технологии не биха били възможни без тях.  Но отново, тези теории са били успешни не заради скорошните им приложения, а защото са били експериментално потвърдени.  Например, те описват планетните орбити със доста задоволителна точност.

 

Все едно да кажем, че C++ е „верен“ език за програмиране, а Хаскел
не е, или обратното.

Това сравнение според мен е неуместно, защото тук говорим за неща изкуствено създадени.  Физиката е естествена наука.  Тя изучава обикалящият ни свят.  Хаскел и C++ са инструменти за изразяване на изчислителни процеси.  Уместно сравнение би било с хипотезата на Чърч и Тюринг, макар и да нямам идея какво би било експериментално доказателство в нейна полза.

Ако си съгласен с:

"Хаскел и C++ са инструменти за изразяване на изчислителни процеси."

сигурно ще се съгласиш и със:

"Физичните теории са инструменти за изразяване на естествени процеси."

 

 

Дори и с математиката е донякъде така.  Евклидовата геометрия „вярна“
ли е?  Между другото Р.Пенроуз (математикофизик) например обича да
казва, че евклидовата геометрия е физическа теория.  Изобщо
математиката също е в крайна сметка моделиране.

Може би изглежда противоречиво, но съм съгласен че математиката до голяма степен е физика.  Разликата е, че при нея експериментите са логически.  Арнолд твърди, че математиката е частта от физиката, в която експериментите са евтини.  Въпреки, че светът който изследва математиката изглежда просто плод на човешкото съзнание, т.е. е изкуствен, това не е съвсем така.  Голяма част от абстрактната математика всъщност има връзка със реални физически явления.  В посочената статия, Дайсън дава чудесен пример с комплексните числа.

А относно, че няма вярна геометрия, да, всичко в математиката е относително.  Относително спрямо базовите постулати, т.е. аксиомите които приемаме за верни.  На пръв поглед може да си помислим, че работата на естествената наука е доказва абсолютни твърдения, но според мен това е едно нереалистично изискване.  Най-малкото, защото едва ли ще някога ще имаме пълно познание за света около нас.  Това към което може да се стремим е все по-точно приближение и приложимост в по-широк кръг от ситуации.

--

You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Krasimir Angelov]

На 12 декември 2013, 20:20, Boyko Bantchev <boy...@gmail.com> написа:
> http://www.ozon.ru/context/detail/id/5134264
> http://www.ozon.ru/context/detail/id/17513376
> http://www.amazon.co.uk/dp/0099440687
> http://www.amazon.co.uk/dp/0743294068

Последните две съм ги чел, а книгата на Манин я намерих тук:

http://www.math.ru/lib/files/pdf/manin.pdf

Не съм чел книги на руски от години. Ще е забавно да си припомня
старите времена :-).

[cutthroat]

12 декември 2013, четвъртък, 20:20:35 UTC+1, Boyko Bantchev написа:

> Не съм напълно съгласен.  Във физиката говорим за експериментални
> доказателства.

Бих ги нарекъл по-скоро не доказателства, а свидетелства за
адекватността на модела.  Ако се търси да се докаже нещо, то е точно
това, че моделът „работи“.  Но това не са формалните или поне
формализуеми доказателства на съвременния математик, а свидетелства,
които получаваме от опита, и такива свидетелства никога не са
окончателни.

Напротив, дори формализируемите доказателства на съвременния математик са свидетелства, които получаваме от опита.  Всяко математическо доказателство зависи от базови логически постулати.  Но такива постулати няма как да са абсолютни.  Логическите "закони" са точно толкова закони колкото и физичните.  Добре нам иезвестният спор -- общовалиден ли е законът за изключеното трето?  Това е нещо което приемаме на доверие.  Няма как да го докажем.  Но опитът ни подсказва че е верен в редица случаи.  Дори да си помислим, че е достатъчно да направим изключение за базовите логически закони, всъщност това далеч не е така.  Защо доказваме неща по индукция?  Защото работи.  Дава "верният" резултат.  Нямаме по-добро обяснение.  В основата си математиката е също толкова емпирична колкото и физиката.  Просто експериментите са толкова евтини че дори не ги забелязваме.  Законът за математическа индукция е точно толкова закон колкото и вторият закон на Нютон.

Всъщност, мога да поспоря, че физичните закони са дори повече закони от логическите и математическите.  Можем да формализираме математическият анализ в класическа логика, можем да го формализираме и в интуиционистка, и то по таткъв начин, че двете формализации са несъвместими и си противоречат една на друга, но нито една не е "грешна".  Строгото математическо съдържание на двата вида анализ макар и подобно е несъвместимо.  От друга страна ако ги използваме за физика ще стигнем до едни и същи резултати.  В известен смисъл, естеството на физиката е по-фундаментално дори от това на логиката и математиката.  Накратко: няма грешна логика, но има грешна физика.

 

Обаче безкрайността на множеството от простите числа е окончателно
_доказан_ факт, който не може да бъде опроверган от опита.

Т.е. ако приемем да речем аксиомите на Цермело, в частност ако приемем че е възможно да съществуват безкрайни множества и т.н.  Не всички хора са съгласни с тях (напр. ултра-финитистите).  Нещо повече, този факт _може_ да бъде опроверган от опита.  Не е изключена възможността да докажем (приемайки същата аксиоматика) че множеството от прости числа е крайно, т.е. да стигнем до противоречие.  И тук стигаме до grand finale от маестро Гьодел:  няма как да покажем, че е невъзможно да стигнем до противоречие.  Трябва да приемем на доверие че математиката е непротиворечива.  Тук не знам на какво да се позова освен на опита, който имаме.

> Това сравнение според мен е неуместно, защото тук говорим за неща
> изкуствено създадени.  Физиката е естествена наука.  Тя изучава
> обикалящият ни свят.  Хаскел и C++ са инструменти за изразяване на
> изчислителни процеси.

Езиците за програмиране са не повече изкуствени инструменти, отколкото
са физическите модели.  И едните, и другите са метафори, създадени от
нас за активно възприемане на съответната част от света под определен
ъгъл.

Физичните модели са много повече от метафори.  Те са твърдения за заобикалящият ни свят.  Какво познание за заобикалящият ни свят изразяват Хаскел или C++? 

12 декември 2013, четвъртък, 20:59:04 UTC+1, Slavomir Kaslev написа:

Ако си съгласен с:

"Хаскел и C++ са инструменти за изразяване на изчислителни процеси."

сигурно ще се съгласиш и със:

"Физичните теории са инструменти за изразяване на естествени процеси."

Под "инструменти за изразяване" имах предвид "_инструменти за_ изразяване".  Те са нотация, запис, който можем да използваме за да кажем нещо.  Но самият език не казва нищо.  Трябва да напишеш текст на него, за да кажеш нещо.  Езикът е формална рамка.  За разлика, физичните теории твърдят факти за естествените процеси.  C++ не твърди никакъв такъв факт.  И затова упоменах тезата на Чърч и Тюринг.  Тя изказва твърдение за заобикалящият ни свят.

[Slavomir Kaslev]

Аз съм заел доста по-прагматична позиция на тази тема напоследък. Гледам на всякакъв вид теория

(била математическа, физична теория или нещо друго) като на софтуер. 

Физичните теории пасват най-добре на това сравнение. Целта на всички физични теории е да предскажат

стойността на някакво количество (енергия, заряд, момент, позиция, т.н.) в дадена система. Ограничението 

е че стойността, която теорията предсказва трябва да отговаря на числото, което би измерил ако направиш

съответния ескперимент в реалния свят.  С други думи, теорията описва сметката, която софтуерна

имплементация на теорията трябва да направи, за да пресметне предсказаната от теорията стойност.

Противоречия, винаги е имало между различни теории. Прогреса идва точно от разрешаването на тези противоречия.

Например, Айнщайн с теориите за относителносста бе разрешил противоречието между Нютоновата физика

и уравненията на Максуел за електромагнетизма. Квантовата теория разрешава противоречието между схващанията

дали материята е вълни или частици. Type theory разрешава парадокси от Ръсел-ов тип в класическа теория на множествата.

Противоречията, за които говориш за "бъгове" в теории, които имат нужда от пренаписване или вероятно refactoring.

2013/12/12 cutthroat <silent.c...@gmail.com>

--

You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

Всъщност това "пренаписване" или "рефакторинг" на идеи и теории това, което ме привлече към Homotopy Type Theory (HoTT).

Също, цитат от статията:

"Manin sees the important advances in mathematics coming from programs, not from problems. Problems are usually solved by apply- ing old ideas in new ways. Programs of research are the nurseries where new ideas are born. He sees the Bourbaki program, rewriting the whole of mathematics in a more abstract language, as the source of many of the new ideas of the twentieth century. He sees the Langlands program, unifying number theory with geometry, as a promising source of new ideas for the twenty-first. People who solve famous unsolved problems may win big prizes, but people who start new programs are the real pioneers."

HoTT хората, се опитват да пренапишат фундаменталната математика на нов абстрактен език (Coq, Adga, whatever),

който на всичкото отгоре може да бъде проверен автоматично от компютър. Такъв език може да се използва за

фундамент за написване на всички научни терории в бъдеще. Според мен, целта на физиката на 21 век

е да се създаде и докаже консистентна квантова теория написана на такъв език. Както Веоводски, може да

дефинира тип на Coq и после автоматично да пресметне размера/кардиналност на типа; така може би един

ден, ще може да дефинираш източник на фотони и гранични условия за сцената и системата автоматично

да пресметне според теорията каква амлитудата за фотон с определена честота на определена позиция.

2013/12/12 Slavomir Kaslev <slavomi...@gmail.com>

--
Slavomir Kaslev

[cutthroat]

13 декември 2013, петък, 02:14:33 UTC+1, Slavomir Kaslev написа:

Противоречията, за които говориш за "бъгове" в теории, които имат нужда от пренаписване или вероятно refactoring.

Ах, не.  Говорех за нещо съвсем съвсем друго.  Говорех за формализирането на една и съща физическа теория в две несъвместими математически обвивки.  Физическото съдържание е едно и също, но математическото не.  Но нека дам следният пример.  Във гладкият анализ с безкрайно малки, се взима като основен следният принцип:

Нека D = { d | d^2 = 0 }.

Аксиома.  За всяка функция f: D -> R и всяко d във D съществува _единствено_ b, такова че: f(d) = f(0) + d.b

Ако си мислим, че живеем във света на класическата математика, това води до противоречие.  В класическият свят D = { 0 } и тогава виждаме, че това b от нашият постулат не само не е единствено, но всъщност постулатът е изпълнен за всякo b, в частност за 0 и за 1, понеже f(d) = f(0).

Но ако примем тази аксиома за вярна, можем да докажем следната

Теорема.  Законът за изключеното трето не е общовалиден.

Доказателство.  Ако беше валиден, ще стигнем до противоречие със нашата аксиома.

Но на физиката не й пука от такива работи.  Тя дава резултати независимо дали смята по единият или другият начин.

> HoTT хората, се опитват да пренапишат фундаменталната математика на нов абстрактен език (Coq, Adga, whatever),

> който на всичкото отгоре може да бъде проверен автоматично от компютър.

Класическият език на математиката също може да бъде проверяван автоматично от компютър.  От него също може автоматично да извличаш програми и т.н. Нещо повече, хората и в момента смятат амплитудата на фотони.  Това, което HOTT може да ти даде е алтернативен, по-прост начин на неща, които правиш и в момента.  Евентуално едно такова опростяване може да улесни правенето на нова физика.  Но това което HOTT не може да даде е качествено нова физика.  Физиката си е същата.  Просто й сменяш дрехите.

Както вече казах, един софтуер не твърди нищо за заобикалящият ни свят.  Физичните теории не са просто формули/компютърни програми.  Те съдържат експериментално потвърдено познание за заобикалящият ни свят.  Ако нещата са по-ясни със софтуерни аналогии: физичната теория не е спецификация, а опит да се разбере спецификацията, т.е. обкръжаващият ни свят.

Мисля, че аналогията със програмисткия свят стига прекалено далеч.  HOTT не пренаписва и не рефакторира идеи.  Идеите са си същите.  HOTT ти дава нов формален език, на който да говориш за тях.  От физична гледна точка този език не ти позволява да изкажеш повече.  Дори да приемем, че всичко е формална игра на символи, да се опитваме да сменим правилата за да можем да си разрешим забраненият ход е глупаво.  Просто защото този ход не е забранен.  Но Хилберт отдавна е мъртъв, както и програмата му.

[Krasimir Angelov]

На 13 декември 2013, 02:48, Slavomir Kaslev <slavomi...@gmail.com> написа:
> HoTT хората, се опитват да пренапишат фундаменталната математика на нов
> абстрактен език (Coq, Adga, whatever),
> който на всичкото отгоре може да бъде проверен автоматично от компютър.
> Такъв език може да се използва за
> фундамент за написване на всички научни терории в бъдеще. Според мен, целта
> на физиката на 21 век
> е да се създаде и докаже консистентна квантова теория написана на такъв
> език. Както Веоводски, може да
> дефинира тип на Coq и после автоматично да пресметне размера/кардиналност на
> типа; така може би един
> ден, ще може да дефинираш източник на фотони и гранични условия за сцената и
> системата автоматично
> да пресметне според теорията каква амлитудата за фотон с определена честота
> на определена позиция.

Това ми звучи точно като тази напомпана статия за Воеводски:

http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/

HoTT е яко нещо, но сама по себе си тя не би убедила болшинството
математици да седнат да пишат на Agda или Coq. Повечето от
потребителите на тези системи са други програмисти, а не математици.
Проблема за математиците е че в едно компютърно доказателство всичко
трябва да се обяснява до най-малките детайли, колкото и очевидни да са
те. Много хора работят по-проблема, надеждите са големи, но все още
проблема не е решен. В някои проекти дори се опитват да анализират
директно текстовете от книги по математика и да правят автоматична
проверка на доказателствата.

Това ми напомня за друг проблем. До колко можем да вярваме на
компютърно доказателство? Доказателство на Agda или Coq е компютърна
програма, което се счита за коректно ако компилатора каже, че в
програмата няма типове грешки. Ами ако самият компилатор не работи
коректно? Преди около две години прехвърлих алгоритъма за проверка на
типовете от Agda в софтуерната система която ние разработваме. От
личен опит знам, че подобни системи са извънредно сложни. Историята
също показва че грешки са възможни. В края на краищата компютърно
доказателство може да е също толкова грешно колкото и доказателство на
лист хартия. Единственото успокоение е че може би софтуера е бил
тестван от множество хора и може да му се има повече доверие.

[Boyko Bantchev]

> Напротив, дори формализируемите доказателства на съвременния
> математик са свидетелства, които получаваме от опита. Всяко
> математическо доказателство зависи от базови логически постулати.
> Но такива постулати няма как да са абсолютни.

Изобщо не мога да се съглася с първото изречение, а като съдя по
следващите, мисля че смесваш две различни неща.

Че постулатите не са абсолютни е ясно, но това прави само тях самите
производни на опита. Ясно е също така, че като говорим за формално
математическо доказателство, имаме предвид изводимостта на някакво
твърдение от аксиомите, а не доказване на какъвто и да било абсолютен
смисъл на това твърдение. В миналото тези два смисъла не са били
различавани, но аз неслучайно казах _съвременната_ математика: в нея
такова смесване на смисли няма.

Да обърна внимание и на следното, защото то допълнително подчертава
тезата ми. До 19 век също е ставало дума за аксиоми (по-точно
постулати, както е у Евклид) и за извеждане на твърдения на тяхна
основа, но именно през 19 век се постига качествена промяна в два
аспекта.
1. Вече не се смята, че аксиомите или участващите в тях понятия
трябва да имат някакъв общопризнат смисъл, каквато е била ролята
им дотогава. Понятията се лишават напълно от какъвто и да е
подразбиран извън аксиомите смисъл („правите“ и „точките“ не са
прави и точки, а произволни обекти), а самите аксиоми са напълно
произволни твърдения: дали изглеждат „правдоподобно“ няма
значение и дори няма как да се обсъжда.
2. Правилата за извод, т.е. логиката, също биват формализирани.
С това доказателствата стават проверяеми и изобщо става възможно
да се обсъжда дали даден текст синтактично и семантично е
доказателство.
С оглед на горното вече и съдържанието на доказваните в математиката
твърдения става абстрактно: сега то е вярно или не само в смисъла на
изводимост от аксиомите, извън всякакви други съображения.

И така, доказателството в съвременния строго математически смисъл не
съдържа подразбирания, нито позоваване на опита, а само на аксиомите,
вкл. логическите правила за извод. Физическото „доказателство“ чрез
опит е, както казах, само свидетелство за някаква хипотеза. Едното и
другото са съвсем различни неща.

> Всъщност, мога да поспоря, че физичните закони са дори повече закони

> от логическите и математическите … В известен смисъл, естеството на

> физиката е по-фундаментално дори от това на логиката и математиката.

Може би си прав за това, но – отново – то няма отношение към въпроса
за разликата между математическото доказателство и това във физиката.
Задълбочаваш объркването между формално доказателство и приписван
смисъл на твърдението, за което писах по-горе.

> Не е изключена възможността да докажем (приемайки същата
> аксиоматика) че множеството от прости числа е крайно, т.е. да
> стигнем до противоречие.

Късмет с доказването на ограниченост на простите числа! :)

Всъщност възможността, за която говориш, съществува само в много
отвлечен смисъл и по-точно дори не знаем дали съществува. Да кажем,
че шансовете са против нея. Във всеки случай, опровергаването или
поне изтъкването на доводи за съмнение във физична теория е винаги
много по-лесно, отколкото да се направи подобно нещо спрямо
математическо доказателство, нали?

> Какво познание за заобикалящият ни свят изразяват Хаскел или C++?

Мислех, че е ясно: това за структурата и фо̀рмата на изчислителните
процеси. Езикът е модел, отразяващ представата ни за това как се
извършват пресмятанията. Още повече, ако приемем че пресмятането –
разбира се, имам предвид не непременно с числа, а по-общия термин
computation – не е чисто човешка измислица, а е свойствено и на
природата извън и независимо от нас. Използването на езика показва
доколко той е адекватен като модел и съответно води до уточняване …
но за това вече писах.

Тезисът на Чърч според мен е по-слабо аналогичен с физически модел,
защото не еволюира чрез опита. Едва ли и би могъл, понеже е нещо
доста по-просто по съдържание от теория или модел и няма обособени
„части“, които евентуално да бъдат променяни.

[Slavomir Kaslev]

2013/12/13 cutthroat <silent.c...@gmail.com>

13 декември 2013, петък, 02:14:33 UTC+1, Slavomir Kaslev написа:

Противоречията, за които говориш за "бъгове" в теории, които имат нужда от пренаписване или вероятно refactoring.

Ах, не.  Говорех за нещо съвсем съвсем друго.  Говорех за формализирането на една и съща физическа теория в две несъвместими математически обвивки.  Физическото съдържание е едно и също, но математическото не.  Но нека дам следният пример.  Във гладкият анализ с безкрайно малки, се взима като основен следният принцип:

Нека D = { d | d^2 = 0 }.

Аксиома.  За всяка функция f: D -> R и всяко d във D съществува _единствено_ b, такова че: f(d) = f(0) + d.b

Ако си мислим, че живеем във света на класическата математика, това води до противоречие.  В класическият свят D = { 0 } и тогава виждаме, че това b от нашият постулат не само не е единствено, но всъщност постулатът е изпълнен за всякo b, в частност за 0 и за 1, понеже f(d) = f(0).

Но ако примем тази аксиома за вярна, можем да докажем следната

Теорема.  Законът за изключеното трето не е общовалиден.

Доказателство.  Ако беше валиден, ще стигнем до противоречие със нашата аксиома.

Но на физиката не й пука от такива работи.  Тя дава резултати независимо дали смята по единият или другият начин.

Може да създаваш теории с противоречия, комбинирайки идеи които не работят заедно, цял живот без да постигнеш нищо.

Противоречията, съществуват само в твоята глава и теории. В природата противоречия няма.

Трика е да избереш аксиоматика, свободна от противоречия, но достатъчна, за да може да моделираш и решиш даден проблем.

Примера, който даваш е решен проблем, даже полезен. Такива d-та, не само, че съществуват (d!=0), но можеш да ги напишеш

на C++, Haskell или на нещо друго. По същия начин, по-който i^2=-1 съществува и може да го напишеш на C++ въпреки,

че е "имагинерна" единица.

Тезата беше, че давайки противоречия нищо не постигаш. Произволен интелигентен идиот може да ти генерира математически

противоречия, обаче понякога трябва гений, за да покаже, че "противоречията" са нищо друго освен неразбиране на проблема

и да покаже правилната теория.

Ако се върна на метафората със софтуер, да показваш противоречия е все едно да говориш за "бъгове" в даден софтуер.

Това всеки може да прави. Въпроса е, какво ще направиш после; какво предлагаш; каква е правилната гледна точка; какъв

е фикса? Какъв е твоя принос?

 

> HoTT хората, се опитват да пренапишат фундаменталната математика на нов абстрактен език (Coq, Adga, whatever),

> който на всичкото отгоре може да бъде проверен автоматично от компютър.

Класическият език на математиката също може да бъде проверяван автоматично от компютър.  От него също може автоматично да извличаш програми и т.н. Нещо повече, хората и в момента смятат амплитудата на фотони.  Това, което HOTT може да ти даде е алтернативен, по-прост начин на неща, които правиш и в момента.  Евентуално едно такова опростяване може да улесни правенето на нова физика.  Но това което HOTT не може да даде е качествено нова физика.  Физиката си е същата.  Просто й сменяш дрехите.

Както вече казах, един софтуер не твърди нищо за заобикалящият ни свят.  Физичните теории не са просто формули/компютърни програми.  Те съдържат експериментално потвърдено познание за заобикалящият ни свят.  Ако нещата са по-ясни със софтуерни аналогии: физичната теория не е спецификация, а опит да се разбере спецификацията, т.е. обкръжаващият ни свят.

Мисля, че аналогията със програмисткия свят стига прекалено далеч.  HOTT не пренаписва и не рефакторира идеи.  Идеите са си същите.  HOTT ти дава нов формален език, на който да говориш за тях.  От физична гледна точка този език не ти позволява да изкажеш повече.  Дори да приемем, че всичко е формална игра на символи, да се опитваме да сменим правилата за да можем да си разрешим забраненият ход е глупаво.  Просто защото този ход не е забранен.  Но Хилберт отдавна е мъртъв, както и програмата му.

Твърде бързо си съставил мнение за какво може и какво не може да се постигне или напише в type theory. Красотата на

HoTT, е че може да ни освободи от Вавилона от езици в математиката, физиката и програмирането и да се ползва един

език за цялата наука. Това какво може да се напише и какви идеи могат да се кодират зависи основно от човека зад

клавиатурата. Като така, повечето твой твърдения за това какво не-може да стане ми се струват малко вероятни да са верни.

По принцип, можеш да намериш милиард потенциални причини, защо нещо може да не стане. Това те прави скептик. Исторически,

добра наука не се прави от скептици. Добра наука се прави въпреки скептиците, докато повтарят, че нещо е невъзможно и гледат

отстрани докато "невъзможното" се случва.

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

2013/12/13 cutthroat <silent.c...@gmail.com>

 Физичните теории не са просто формули/компютърни програми.  Те съдържат експериментално потвърдено познание за заобикалящият ни свят. 

Според мен превъзнасяш прекалено какво точно е физическа теория. Ето Файнман на темата: http://www.youtube.com/watch?v=yLZZZxzxwSY .

Ако му вярваш, физика се прави както се прави всяка друга наука. Правиш предположение и го проверяваш. В резултатните

теории няма никаква метафизична причина да са верни или да са свързани с реалността. Теориите са толкова добри,

колкото са точни предположенията на създателите. Почти винаги теориите са дефинирани чрез чисто математически уравнения.

Няма физична магия, просто математика както винаги.

--
Slavomir Kaslev

[cutthroat]

13 декември 2013, петък, 11:09:04 UTC+1, Boyko Bantchev написа:

Че постулатите не са абсолютни е ясно, но това прави само тях самите 
производни на опита.

Абсолютно същото нещо се случва и във физиката.  Да вземем например класическата механика.  В днешно време оригиналните закони на Нютон всъщност са следствия от принципа на най-малкото действие.  Това е нелогически закон и опита ни подсказва че е верен.  По същия начин, закона за математическа индукция е нелогически закон и опита ни подсказва че е верен.  Точно както математиката се гради на някакви базови принципи (индукция, съществуване на граници, и т.н.), така и физиката се гради върху базови принципи (най-малко действие, локалност, крайна енергия и т.н.).  Предричанията на една физическа теория са изцяло следствие от тези базови принципи.  Единствената разлика е доколко сме убедени в тези принципи.

И така, доказателството в съвременния строго математически смисъл не 
съдържа подразбирания, нито позоваване на опита, а само на аксиомите, 
вкл. логическите правила за извод.

 

Т.е. се позовава на метатеорията или метаматематика както я нарича Хилберт.  Защо приемаме доказателство базирано на тези правила за извод?   Защото метатеорията се позовава на опита.  Затова тя е интересна.  Защо никой не работи в логика, в която можеш да докажеш всичко?  Затова Хилберт толкова отчаяно се е опитвал да покаже, че метатеорията е непротиворечива.  Смисъла, в който съществува тази възможност, въобще не е отвлечен, а много конкретен: формален извод на формулата "лъжа".  Не знаем дали метатеорията с която работим е непротиворечива.  Няма как да го докажем.  Има единствено как да покажем обратното, т.е. да изведем "лъжа".  Същото е и с физиката.  Няма как да покажем че дадена теория няма да си противоречи с бъдещ експеримент.  Единствено можем да я оборим като намерим такъв експеримент.

Моето мнение е, че всяко математическо доказателство базирано на някаква метатеория влече със себе си и самата метатеория.  Иначе това доказателство би било изпразнено от съдържание.  Поне за мен математиката не е просто игра на формални символи лишена от смисъл. 

 

> Какво познание за заобикалящият ни свят изразяват Хаскел или C++?

Мислех, че е ясно: това за структурата и фо̀рмата на изчислителните
процеси.  Езикът е модел, отразяващ представата ни за това как се
извършват пресмятанията.

Нека дам и контекста на това изречение:

> Те са твърдения за заобикалящият ни свят.  Какво познание за заобикалящият ни свят изразяват Хаскел или C++? 

Та какво е нещото което Хаскел и C++ твърдят?  Че са адекватен модел?  Не мисля.  Хаскел и C++ сами по себе си не твърдят нищо.  Машината на Тюринг не твърди нищо.  Отделно можем да твърдим, че те са адекватен модел.  Това всъщност е една от двете части на тезата на Чърч и Тюринг i заради това я упоменах.

Тезисът на Чърч според мен е по-слабо аналогичен с физически модел,
защото не еволюира чрез опита.

Физическият модел еволюира с натрупването на нови експериментални резултати.  Просто нямаме резултати, които да го отхвърлят.  Да не забравяме, че хората дълго време са търсели какво всъщност може да бъде изчислено и какво не.  Преди да стигнат до частичните рекурсивни функции са минали през примитивно рекурсивните.  В такава ситуация едно твърдение подобно на тезата на Чърч и Тюринг: всички естествени излислителни процеси са примитивно рекурсивни, би могло да бъде обороено не много по-различно от теория от физиката.

13 декември 2013, петък, 12:58:55 UTC+1, Slavomir Kaslev написа:

 

Може да създаваш теории с противоречия, комбинирайки идеи които не работят заедно, цял живот без да постигнеш нищо.

Противоречията, съществуват само в твоята глава и теории.

Ах, не.  Явно не съм бил достатъчно ясен.  Не говоря за създаване на теории с противоречия.  Говоря за две формализации на физиката в различни основни на математиката.  Тези две различни основи си противоречат, но не и физичните теории развити в тях.  Това което казах е, че двете различни формализации биха имали несъвместимо математическо съдържание, но физическото ще бъде напълно еднакво.  Това е защото за двете неща имаме различно мерило.  За да бъде добра една физична теория не ме интересува дали се формализира в теория на типовете или теория на множествата.  Тя трябва да дава резултати относно експерименти в реалният свят.

 

Примера, който даваш е решен проблем, даже полезен. Такива d-та, не само, че съществуват (d!=0), но можеш да ги напишеш

на C++, Haskell или на нещо друго. По същия начин, по-който i^2=-1 съществува и може да го напишеш на C++ въпреки,

че е "имагинерна" единица.

Това всички много добре го знаем.  Може да прегледаш http://home.imf.au.dk/kock/sdg99.pdf

 

Тезата беше, че давайки противоречия нищо не постигаш. Произволен интелигентен идиот може да ти генерира математически

противоречия, обаче понякога трябва гений, за да покаже, че "противоречията" са нищо друго освен неразбиране на проблема

и да покаже правилната теория.

Въобще не си разбрал какво казвам.  Не само не си разбрал, но и просто повтаряш това което аз казвам:

> Но на физиката не й пука от такива работи.  Тя дава резултати независимо дали смята по единият или другият начин.

 

Твърде бързо си съставил мнение за какво може и какво не може да се постигне или напише в type theory. Красотата на

HoTT, е че може да ни освободи от Вавилона от езици в математиката, физиката и програмирането и да се ползва един

език за цялата наука. Това какво може да се напише и какви идеи могат да се кодират зависи основно от човека зад

клавиатурата. Като така, повечето твой твърдения за това какво не-може да стане ми се струват малко вероятни да са верни.

Мда, отне ми една магистратура по математическа логика.  Математиката няма Вавилон от езици.  Обичайната има един стандартен език: ZFC (теория на множествата).  Общоприетото мнение е, че цялата ни известна математика, освен едни особени метатеоретични изключения, може да бъде формализирана във ZFC или в нейни надстройки.  Понеже харесваш програмистки метафори, проблемът на ZFC е, че за някои модерни математическите цели той е като асемблер.  Изпъстрен с твърде много нерелевантни подробности към самото математическо съдържание.  Затoва хората се насочват към категории или пък към HoTT.  

По принцип, можеш да намериш милиард потенциални причини, защо нещо може да не стане. Това те прави скептик. Исторически,

добра наука не се прави от скептици. Добра наука се прави въпреки скептиците, докато повтарят, че нещо е невъзможно и гледат

отстрани докато "невъзможното" се случва.

Добрата наука се прави от хората, които мислят и работят в дълбочина.  Сами или с чужда помощ.  (Напр. Айнщайн е работил с Хилберт върху общата си теория, понеже не е бил достатъчно добър математик).  Разбира се, трябва ти много въображение, но само с фантазиране не става.  При това не давам причини защо нещо няма да стане.  Давам причини защо и как HoTT може и не може да помогне.  Моето разбиране е, че ако използваш HoTT като основа на математиката, единствено може да ти помогне в по-голямата си ефективност като език.  Почти същите неща ще можеш да покажеш и в ZFC, само че би било изпълнено с твърде много шум.  Съответно имаш много добра причина да ползваш HoTT, но това не е защото там автоматично ще получиш нови идеи.  Идеите са независими от метатеорията която ползваш, най-малкото защото никой не мисли в рамките на дадена метатеория (освен автоматичният доказвач на теореми).

Нищо не превъзнасям  Никога не съм твърдял, че има някаква метафизика тук. Всъщност, с

> Те съдържат експериментално потвърдено познание за заобикалящият ни свят.

казвам точно каквото и ти:

Теориите са толкова добри, колкото са точни предположенията на създателите.

И да, няма никаква метафизична причина тези теории да са свързани с реалността.  Причината е експериментална.  Никъде не твърдя че са общовалидни.  Просто, експериментално потвърденатата теория предвижда проведените експерименти.  Нищо повече.  Това, което твърдя е, че има разлика в предназначението между компютърни програми и физични теории.  Компютърната програма е предназначена за изпълнение от компютър.  Физичната теория няма такова предназначение, дори и да може да бъде изпълнена от компютър.  За теб тази разлика може да е твърде тънка за да се упоменава, но за мен не е.  Не съм съгласен с разсъждението: едното нещо смята, другото нещо смята, значи са едно и също.  Ако беше така нямаше да има разлика между инженер и счетоводител. 

Съгласен съм, че връзката между основите на математиката и изчислимостта и програмирането е очарователна.  Но също така, тя е отдавна добре известна още от време Гьоделово, че и преди това.  Хората са работели адски много върху това: всякаквите разни там изчислими реални функции (Тюринг), reliasability интерпретации (Гьодел, Клини), Curry-Howard-Girard-Reynolds, ефективни топоси (Хайлънд)…  Това става със и без теория на типовете.  Това не са новите концепции които HoTT внася.  Може би новото в HoTT ще направи всичко това практическо.  Много ще се радвам.

[Boyko Bantchev]

> Абсолютно същото нещо се случва и във физиката … Точно както

> математиката се гради на някакви базови принципи (индукция,
> съществуване на граници, и т.н.), така и физиката се гради върху

> базови принципи …

Никак не е „абсолютно същото нещо“. Физиката не е, и доколкото
знам, никой не се опитва да я превърне в аксиоматична наука. Ако
го направят, не би била вече физика, а математика. Но никой не иска
това, защото от такава „физика“ полза едва ли ще има. Нито базовите
принципи във физиката са аксиоми, нито се третират като такива. Та
те са само мъгляви общи положения и не е ясно дори кога са (или може
да се предполага че са, или пък искаме да са) в сила и кога не. Що за
„аксиома“ може да бъде принципът на най-малкото съпротивление? Какво
общо има той с формален извод от аксиоми?

> Защо приемаме доказателство базирано на тези правила за извод?
> Защото метатеорията се позовава на опита.

Само че традиционната логика, сега формализирана, се използва за
аксиоматично изграждане на всякакви математически теории. Веднъж
приета за инструмент, оттам насетне за твърденията в дадена теория е
важно само дали са изводими от аксиомите или не. Никой не проектира
експерименти за потвърждаване на вече доказани факти. Във физиката,
понеже нищо не е окончателно доказано, това се прави.

Приравняването на математическия и физическия методи е голямо насилие
над здравия разум.

> Поне за мен математиката не е просто игра на формални символи лишена
> от смисъл.

Само че това е съвсем друг въпрос. Редно е да правим разлика между
това защо се прави математика, какъв смисъл се придава на нейните
резултати, от една страна, и това как (се стремим да) строим нейните
теории, от друга. Едното се отнася до употребата на науката, а
другото – до стремежа към максимална надеждност на този вид знание.

> Та какво е нещото което Хаскел и C++ твърдят?

Малко досадно ми е, че трябва да го кажа за трети път: езиците за
програмиране са модели. Моделите не „твърдят“, те отразяват представи
за нещата. В случая – представи за това що е то пресмятане.
Представи много по-подробно уточнени от например тезиса на Чърч,
който, ако изобщо трябва да бъде оприличаван на модел, е безинтересен.

[Slavomir Kaslev]

2013/12/13 cutthroat <silent.c...@gmail.com>

13 декември 2013, петък, 12:58:55 UTC+1, Slavomir Kaslev написа:

 

Може да създаваш теории с противоречия, комбинирайки идеи които не работят заедно, цял живот без да постигнеш нищо.

Противоречията, съществуват само в твоята глава и теории.

Ах, не.  Явно не съм бил достатъчно ясен.  Не говоря за създаване на теории с противоречия.  Говоря за две формализации на физиката в различни основни на математиката.  Тези две различни основи си противоречат, но не и физичните теории развити в тях.  Това което казах е, че двете различни формализации биха имали несъвместимо математическо съдържание, но физическото ще бъде напълно еднакво.  Това е защото за двете неща имаме различно мерило.  За да бъде добра една физична теория не ме интересува дали се формализира в теория на типовете или теория на множествата.  Тя трябва да дава резултати относно експерименти в реалният свят.

Опистай се да си по-ясен и кратък. Говориш за "две формализации на физиката", които "две различни основи си противоречат, но не и физичните теории развити в тях". И парадоксът е, че според теб и двете "дава [верни] резултати относно експерименти в реалният свят"

въпреки, че математиката си противоречи.

Първо, не знам откъде знаеш, че сменяйки фундамента на физическа теория, тя още ще работи. Може да е така, може да не е, зависи

от какво си променил. Ако промениш какъв резултат дава a+b може да очакваш всички суми в теорията да дават различен резултат.

Второ, ок съм с "двете различни формализации биха имали несъвместимо математическо съдържание, но физическото ще бъде напълно еднакво". Въпроса ми е, какво от това? Защо това е интересно? (ясно и кратко) 

На мен ми е ясно, че има много грешни отговори. Можеш ли да ми кажеш нещо ново в посока правилния отговор?

 

 

Примера, който даваш е решен проблем, даже полезен. Такива d-та, не само, че съществуват (d!=0), но можеш да ги напишеш

на C++, Haskell или на нещо друго. По същия начин, по-който i^2=-1 съществува и може да го напишеш на C++ въпреки,

че е "имагинерна" единица.

Това всички много добре го знаем.  Може да прегледаш http://home.imf.au.dk/kock/sdg99.pdf

Добре.

 

 

Тезата беше, че давайки противоречия нищо не постигаш. Произволен интелигентен идиот може да ти генерира математически

противоречия, обаче понякога трябва гений, за да покаже, че "противоречията" са нищо друго освен неразбиране на проблема

и да покаже правилната теория.

Въобще не си разбрал какво казвам.  Не само не си разбрал, но и просто повтаряш това което аз казвам:

Значи съм разбрал, щом говорим на един език.

 

> Но на физиката не й пука от такива работи.  Тя дава резултати независимо дали смята по единият или другият начин.

 

Твърде бързо си съставил мнение за какво може и какво не може да се постигне или напише в type theory. Красотата на

HoTT, е че може да ни освободи от Вавилона от езици в математиката, физиката и програмирането и да се ползва един

език за цялата наука. Това какво може да се напише и какви идеи могат да се кодират зависи основно от човека зад

клавиатурата. Като така, повечето твой твърдения за това какво не-може да стане ми се струват малко вероятни да са верни.

Мда, отне ми една магистратура по математическа логика.  Математиката няма Вавилон от езици.  Обичайната има един стандартен език: ZFC (теория на множествата).  Общоприетото мнение е, че цялата ни известна математика, освен едни особени метатеоретични изключения, може да бъде формализирана във ZFC или в нейни надстройки.  Понеже харесваш програмистки метафори, проблемът на ZFC е, че за някои модерни математическите цели той е като асемблер.  Изпъстрен с твърде много нерелевантни подробности към самото математическо съдържание.  Затoва хората се насочват към категории или пък към HoTT.  

Съгласен. И не само, модерни концепции като категории и fiber bundles, които се появяват във физични теории (а и други област), имат

естествена респрезентация в HoTT.

 

По принцип, можеш да намериш милиард потенциални причини, защо нещо може да не стане. Това те прави скептик. Исторически,

добра наука не се прави от скептици. Добра наука се прави въпреки скептиците, докато повтарят, че нещо е невъзможно и гледат

отстрани докато "невъзможното" се случва.

Добрата наука се прави от хората, които мислят и работят в дълбочина.  Сами или с чужда помощ.  (Напр. Айнщайн е работил с Хилберт върху общата си теория, понеже не е бил достатъчно добър математик).  Разбира се, трябва ти много въображение, но само с фантазиране не става.  При това не давам причини защо нещо няма да стане.  Давам причини защо и как HoTT може и не може да помогне.  Моето разбиране е, че ако използваш HoTT като основа на математиката, единствено може да ти помогне в по-голямата си ефективност като език.  Почти същите неща ще можеш да покажеш и в ZFC, само че би било изпълнено с твърде много шум.  Съответно имаш много добра причина да ползваш HoTT, но това не е защото там автоматично ще получиш нови идеи.  Идеите са независими от метатеорията която ползваш, най-малкото защото никой не мисли в рамките на дадена метатеория (освен автоматичният доказвач на теореми).

13 декември 2013, петък, 13:39:58 UTC+1, Slavomir Kaslev написа:

2013/12/13 cutthroat <silent.c...@gmail.com>

 Физичните теории не са просто формули/компютърни програми.  Те съдържат експериментално потвърдено познание за заобикалящият ни свят. 

Според мен превъзнасяш прекалено какво точно е физическа теория. Ето Файнман на темата: http://www.youtube.com/watch?v=yLZZZxzxwSY .

Ако му вярваш, физика се прави както се прави всяка друга наука. Правиш предположение и го проверяваш. В резултатните

теории няма никаква метафизична причина да са верни или да са свързани с реалността. Теориите са толкова добри,

колкото са точни предположенията на създателите. Почти винаги теориите са дефинирани чрез чисто математически уравнения.

Няма физична магия, просто математика както винаги.

Нищо не превъзнасям  Никога не съм твърдял, че има някаква метафизика тук. Всъщност, с

> Те съдържат експериментално потвърдено познание за заобикалящият ни свят.

казвам точно каквото и ти:

Теориите са толкова добри, колкото са точни предположенията на създателите.

И да, няма никаква метафизична причина тези теории да са свързани с реалността.  Причината е експериментална.  Никъде не твърдя че са общовалидни.  Просто, експериментално потвърденатата теория предвижда проведените експерименти.  Нищо повече.  Това, което твърдя е, че има разлика в предназначението между компютърни програми и физични теории.  Компютърната програма е предназначена за изпълнение от компютър.  Физичната теория няма такова предназначение, дори и да може да бъде изпълнена от компютър.  За теб тази разлика може да е твърде тънка за да се упоменава, но за мен не е.  Не съм съгласен с разсъждението: едното нещо смята, другото нещо смята, значи са едно и също.  Ако беше така нямаше да има разлика между инженер и счетоводител. 

Съгласен съм, че връзката между основите на математиката и изчислимостта и програмирането е очарователна.  Но също така, тя е отдавна добре известна още от време Гьоделово, че и преди това.  Хората са работели адски много върху това: всякаквите разни там изчислими реални функции (Тюринг), reliasability интерпретации (Гьодел, Клини), Curry-Howard-Girard-Reynolds, ефективни топоси (Хайлънд)…  Това става със и без теория на типовете.  Това не са новите концепции които HoTT внася.  Може би новото в HoTT ще направи всичко това практическо.  Много ще се радвам.

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

2013/12/13 Boyko Bantchev <boy...@gmail.com>

> Абсолютно същото нещо се случва и във физиката … Точно както

> математиката се гради на някакви базови принципи (индукция,
> съществуване на граници, и т.н.), така и физиката се гради върху

> базови принципи …

Никак не е „абсолютно същото нещо“.  Физиката не е, и доколкото
знам, никой не се опитва да я превърне в аксиоматична наука.  Ако
го направят, не би била вече физика, а математика. Но никой не иска
това, защото от такава „физика“ полза едва ли ще има.  Нито базовите
принципи във физиката са аксиоми, нито се третират като такива.  Та
те са само мъгляви общи положения и не е ясно дори кога са (или може
да се предполага че са, или пък искаме да са) в сила и кога не.  Що за
„аксиома“ може да бъде принципът на най-малкото съпротивление?  Какво
общо има той с формален извод от аксиоми?

Не си прав. Разбира се, че физиците се опитват да намерят каква е 

правилната физична аксиоматика, но още не я знаят и за това ползват

"Babylonian mathematics" по думите на Файнман http://www.youtube.com/watch?v=YaUlqXRPMmY 

 

> Защо приемаме доказателство базирано на тези правила за извод?
> Защото метатеорията се позовава на опита.

Само че традиционната логика, сега формализирана, се използва за
аксиоматично изграждане на всякакви математически теории.  Веднъж
приета за инструмент, оттам насетне за твърденията в дадена теория е
важно само дали са изводими от аксиомите или не.  Никой не проектира
експерименти за потвърждаване на вече доказани факти.  Във физиката,
понеже нищо не е окончателно доказано, това се прави.

Приравняването на математическия и физическия методи е голямо насилие
над здравия разум.

> Поне за мен математиката не е просто игра на формални символи лишена
> от смисъл.

Само че това е съвсем друг въпрос.  Редно е да правим разлика между
това защо се прави математика, какъв смисъл се придава на нейните
резултати, от една страна, и това как (се стремим да) строим нейните
теории, от друга.  Едното се отнася до употребата на науката, а
другото – до стремежа към максимална надеждност на този вид знание.

> Та какво е нещото което Хаскел и C++ твърдят?

Малко досадно ми е, че трябва да го кажа за трети път: езиците за
програмиране са модели.  Моделите не „твърдят“, те отразяват представи
за нещата.  В случая – представи за това що е то пресмятане.
Представи много по-подробно уточнени от например тезиса на Чърч,
който, ако изобщо трябва да бъде оприличаван на модел, е безинтересен.

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

2013/12/13 Krasimir Angelov <kr.an...@gmail.com>

Във всяко вярно доказателство (компютърно или не) трябва всичко да

се обяснява в най-малките детайли. Плюса да ползваш компютър, е

че може да ти помогне да видиш, че не си изпуснал нито един детайл.

 

Това ми напомня за друг проблем. До колко можем да вярваме на
компютърно доказателство? Доказателство на Agda или Coq е компютърна
програма, което се счита за коректно ако компилатора каже, че в
програмата няма типове грешки. Ами ако самият компилатор не работи
коректно? Преди около две години прехвърлих алгоритъма за проверка на
типовете от Agda в софтуерната система която ние разработваме. От
личен опит знам, че подобни системи са извънредно сложни. Историята
също показва че грешки са възможни. В края на краищата компютърно
доказателство може да е също толкова грешно колкото и доказателство на
лист хартия. Единственото успокоение е че може би софтуера е бил
тестван от множество хора и може да му се има повече доверие.

Съгласен. Проблема на какво може да вярваш е съществен, но не

знам добро решение. Както ти си забелязал, единствения начин е brute force, 

нещото да се проверява (и поправя) постоянно по различни начини и от 

различни хора. По същия brute force метод много компании правят добър

софтуер на който (евентуално) може да вярваш, заради многото тестове

и верификация през която е минал. Разбира се, никога не можеш да бъдеш

напълно сигурен, че някой малък детайл не е изпуснат. 

 

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Boyko Bantchev]

2013/12/13 Slavomir Kaslev <slavomi...@gmail.com>:

> Не си прав. Разбира се, че физиците се опитват да намерят каква е
> правилната физична аксиоматика, но още не я знаят и за това ползват
> "Babylonian mathematics" по думите на Файнман
> http://www.youtube.com/watch?v=YaUlqXRPMmY

Припомни ми да се сетя – ти ли беше, дето преди няколко дни изприказва
куп простотии по мой адрес? Как ти хрумна, че горя от желание да си
побъбрим?

[Slavomir Kaslev]

2013/12/13 Boyko Bantchev <boy...@gmail.com>

http://bit.ly/1gXhip3 

Когато говориш глупости, заслужаваш да бъдеш поправен. Може да научиш нещо ново.

--
Slavomir Kaslev

[Boyko Bantchev]

> Когато говориш глупости, заслужаваш да бъдеш поправен. Може да научиш нещо
> ново.

http://natribu.org

[Slavomir Kaslev]

Това ме остави без думи. 

Последвах примера на Стефчо и погледнах нещата, по-които си работил последните 

години на сайта. Трябва да се изивиня публично, намерих няколко нови идеи сред многото

чужди, а също и работещ софтуер, някой от който интересен. 

Особено ми хареса езика за правене на чертежи, html сайта за обучение на ученици,

и това че имаш интерес към продължени дроби. Аз също съм много заинтересуван в 

продължени дроби, заради връзките с монади, възли, Паде апроксимации и итериране

на функции към които имам особена любов напоследък.

Не мисля, че може да се тревожиш, че репутацията ти ще пострада от глупава дискусия

в някоя група. Всичко това е само термичен шум като новините по телевизията. Това, което 

ще остане са публикациите, книгите, и софтуера, които си написал (макар че днешния софтуер

bit rott-ва, както сигурно си забелязал). 

Всеки греши, независимо къде работи и как се казва. Моята единствена препоръка е да

добавиш "Never admit when you're wrong, just keep arguing." към шеговития наръчник за

интернет спорове, който си написал.

--
Slavomir Kaslev

[Boyko Bantchev]

> Трябва да се изивиня публично

Да се извиниш определено е положителна стъпка – така се прави като
сбърка човек. А ти направи грешки в много посоки, ще си позволя да
обърна внимание на това – не за да ти трия сол, а надявайки се да го
разбереш и избягваш да повтаряш същото.
Нападаш лично, а не това, което казвам.
За личните си нападки нямаш и основание – не ме познаваш, нито
работата ми.
Агресията ти е непредизвикана: не съм се държал зле с теб в
никакъв смисъл.
Държиш се крайно грубо, което само̀ по себе си, дори без оглед на
останалото, е неоправдано.
Ако ще коментираш казаното от мен, постарай се без оценки, особено
пък категорични като „не си прав“, „говориш глупости“. Оспорването
става с аргументи.
Избягвай и високомерието. Примерно, може да те е заинтересувала
темата „пораждащи функции“ или „комбинаторно броене“, но защо смяташ,
че за мен (или някой друг) е непозната? Тези неща се развиват вече
около 90 години.

Сега, не става въпрос за репутацията ми, която споменаваш, а за
възможността за общуване, заради която се предполага, че сме тук.
Като се погазят правилата за общуване, то изчезва. А е лесно да се
спазват, защото става дума за най-обикновена почтеност.

Ще ми се да приема извинението ти за искрено – иначе не бих писал
това. Само че ще ми е по-лесно да го повярвам, ако в същото
изречение не беше сложил:

> сред многото чужди [идеи]

Чужди идеи не правя предмет на публикациите си, още по-малко да ги
представям за свои. Цитираното е голословно твърдение, невярно и не
е в посока на нормално общуване. И още веднъж напомням, че не сме
тук, за да обсъждаме мен.

~~~~~~~~~
П.П.:
1. Това, което на английски е continued fractions или chained
fractions, на български е „верижни дроби“. Аз не съм работил по
тях, само съм ги споменал някъде.
2. Учебното пособие, за което казваш, че „bit rott-ва“, работи са̀мо
с IE и SVGView, както е и написано там. (По него време това беше
единствената възможност.)

[cutthroat]

13 декември 2013, петък, 20:05:11 UTC+1, Boyko Bantchev написа:

> Абсолютно същото нещо се случва и във физиката … Точно както 
> математиката се гради на някакви базови принципи (индукция, 
> съществуване на граници, и т.н.), така и физиката се гради върху 
> базови принципи … 

Никак не е „абсолютно същото нещо“.  Физиката не е, и доколкото 
знам, никой не се опитва да я превърне в аксиоматична наука.

Това просто не е така.  Никой не се опитва да я превърне в _изцяло_ аксиоматична наука.  Тогава не би била наука въобще, защото всяка наука е отчасти експериментална.  Това че _някои_ математици се опитват да превърнат математиката в _изцяло_ аксиоматична наука е съвсем друго нещо.  Но нека да кажем нещо и за опитите.  Всъщност акиоматизацията на физиката е номер 6 от Хилбертовите проблеми:

http://de.wikipedia.org/wiki/Hilbertsche_Probleme#Hilberts_sechstes_Problem

Ето нещичко от Айнщайн:

http://egregium.wordpress.com/2009/07/28/einstein-on-axiomatization-of-physics/

А ето и нещо по-ново:

http://en.wikipedia.org/wiki/Axiomatic_quantum_field_theory

Та 
те са само мъгляви общи положения и не е ясно дори кога са (или може 
да се предполага че са, или пък искаме да са) в сила и кога не.  Що за 
„аксиома“ може да бъде принципът на най-малкото съпротивление?  Какво 
общо има той с формален извод от аксиоми? 

Предполагам имаш предвид пътят на най-малкото съпротивление (http://en.wikipedia.org/wiki/Path_of_least_resistance), което както се казва в страницата е folk physics.  Това, което цитирах аз, е принципът на най-малкото действие (http://en.wikipedia.org/wiki/Principle_of_least_action).  Това е строг в математическият смисъл принцип: взимаш функционала и минимизираш, за да получиш треакторията.  Това е фундаментален принцип, който макар и изказан на математически език има физическо съдържание: твърди каква треактория ще поеме дадена система.  Когато научих за него, бях шокиран как почти цялата физика, която знаех от училище, се корени в едно толкова просто твърдение.

 

Само че традиционната логика, сега формализирана, се използва за
аксиоматично изграждане на всякакви математически теории. Веднъж
приета за инструмент, оттам насетне за твърденията в дадена теория е
важно само дали са изводими от аксиомите или не.

Добре, нека я приемем за инструмент.  Но тогава автоматично доказваме твърдения от вида "ако метатеорията е непротиворечива, то това твърдение е вярно в нея".  Както отбелязах, възможност за противоречие има във съвсем точен смисъл.  Но нека кажем, че не се интересуваме от непротиворечивостта на метатеорията.  Нима това не значи, че дори да има противоречие в аритметиката, за нас това не обезмисля математическото съдържание?  Но какво е то тогава?  Не мисля, че то е просто съществуването на формален извод от аксиомите.  Според мен, математическото съдържание е това което прави математиката вид абстрактна физика.

Никой не проектира експерименти за потвърждаване на вече доказани факти.

 

Особено в днешно време хората проектират с години.  Строят проверчици на доказателства, формализират, проверяват.  Хората все още четат стари доказателства, откриват грешки в тях, поправят.  Никога няма напълно вярно доказателство, просто защото идеализираният смисъл на вярност е само това: идеал, който не може да бъде реализиран.  Дори да се надяваме да механизираме тази проверка, никога не отсъства възможността за грешка.  Дори да верифицираме проверчика на доказателства, пак не отсъства възможността за грешка във програмата верификатор.  Макар и да не можем наистина да покажем, че във верификаторът отсъстват грешки, те наистина може да отсъстват.  Дори в този случай обаче, машината която изпълнява самата верификация не е 100% надежна (http://en.wikipedia.org/wiki/Arbiter_(electronics)#Asynchronous_arbiters_and_metastability).  Сега нека напомня:

Във физиката, понеже нищо не е окончателно доказано, това се прави.

Е, и в математиката е така.  Единственото което можем да кажем е, че с голяма вероятност доказателството е вярно.  Това число в математиката е много по-голямо, но все пак то е строго по-малко от единица.

 

Приравняването на математическия и физическия методи е голямо насилие
над здравия разум.

Нима в математиката няма недоказани хипотези?  Нима хората не експериментират с частни случаи?  Чудесен пример за това е теория на числата.  Нима хипотезите на Риман и Голдбах не са експериментално тествани?  На тази страница: http://en.wikipedia.org/wiki/Goldbach's_conjecture#Heuristic_justification дори си говорим за heuristic justification.  Някой може да възрази: теоремата на Ферма вече е доказана, точка.  Но тогава попадаме на: 

http://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof

За какви аксиоми си говорим?  Трябва ли да пренапишем теоремата доказана от Андрю Уайлс на "ако съществуват големи кардинали, то Ферма е прав"?  Ако се окаже, че теоремата на Ферма наистина зависи от големи кардинали, какво правим?  Тук идва един основен проблем.  Вярност и доказуемост от базови аксиоми са две различни неща.  Известната теорема на Гьодел.  Ако просто се интересувахме от формална доказуемост според мен това свежда въпросът до игра на символи.  Обаче, не можем да дадем нещо повече от формална доказуемост.  Просто не всички верни твърдения имат формален извод от аксиомите.  

В крайна сметка, математиката е експериментална наука точно както и физиката.  Понеже логическите методи са непълни, трябва да подплатим доказателството на една теорема със конкретни сметки.  Сметки, на които вярваме.  Например да проверим теоремата на Ферма за няколко милиона примера.  Но обикновено считаме за достатъчно да тестваме само аксиомите.  Например, че математическата индукция работи.  Индукцията е доста интересен принцип, защото всъщност това е аксиомна схема.  Налага ни се да се доверим на безкрайно много аксиоми, при това построени използвайки индукция от метатеорията.  Но добре, доверяваме са на математическата индукция и хоп, изкача друг клас от твърдения, които не можем да докажем но ни се струват верни.  И това въобще не е отвлечено.  Теоремата на Гьодел работи.  Да игнорираме този проблем, значи да действаме по начина: каквото не мога да докажа, приемам за аксиома.  Единственото, което ни остава е да тестваме в живия живот.  Точно каквото прави и физиката.

Нека също отбележа, че няма как да има напълно формална математика.  Това е ограничение на самата формална логика.  Винаги работиш спрямо някаква метатеория.  Опиташ ли се да формализираш, просто обвиваш в друга неформална метатеория.

Представи много по-подробно уточнени от например тезиса на Чърч,
който, ако изобщо трябва да бъде оприличаван на модел, е безинтересен.

Ах, това съвсем не е така.  Машината на Тюринг, моделът от тезата на Чърч и Тюринг, е много по-добре дефиниран от C++ и Haskell.  Особено C++ пък няма добра формална дефиниция.  Подробностите в C++ и Haskell са безинтересни относно това какви изчислителни процеси моделират.  Затова никой, занимаващ се с изчислимост и сложност, не работи със C++ или Haskell, ами използва машини на Тюринг или подобните.

Друг е върпосът за колко добро изразно средство са C++ Haskell, но това няма отношение.  Те или моделират излислителните процеси или не, както физическите теории или моделират физическите процеси или не.  Това е въпросът който касае физиката.  n-те различни математически описания на квантовата физика съжителстват точно както C++ и Haskell.  Теорията обаче си остава същата, предрича едни и същи резултати.  Всичко това беше в контекста на струнната теория и нейните алтернативи.  Те не са различни формулировки, даващи едни и същи резултати. 

[cutthroat]

За съжаление съм твърде многословен.  Ще се опитам да направя резюме.

Не можем просто да приемаме аксиоми за верни.  В редица интересни случаи това просто значи да приемем това, което искаме да докажем.  Много такива случаи са анатемосани като патологични и безинтересни, но аз не съм съгласен.  Причината, заради която не съм съгласен е, че някои от тези случаи касаят понятието изчислимост, а това е нещо, което според мен е свързано директно с реалността.  Мисля, че в нашият свят има един възможен клас от излислими функции, макар и най-вероятно да няма как да узнаем кой е той всъщност.

По теоремата на Гьодел, множествето от естествените числа няма пълна и ефективна (рекурсивно номеруема) аксиоматизация.  Винаги има твърдения верни в структурата на естествените числа, но които няма да можем да изведем формално.  Тези твърдения единствено можем да подложим на експериментална проверка.

Тук ситуацията е съществено различна от евклидовата геометрия, където ако премахнем петият постулат, можем да получим алтернативни геометрии и нито една от тях не е "правилната".  За евклидовата геометрия и нейните алтернативи можем да намерим пълна и рекурсивна аксиоматика, т.е. можем да докажем верните твърдения.  Това няма как да се случи с естествените числа.  За тях не може да има такава аксиоматика.  Нещо повече, теоремата на Тененбаум ни казва, че ако започнем с непълна аксиоматика и строим алтернативи на естествените числа, т.е. нестандартни модели, в тези алтернативи операциите + и * не са изчислими в смисъла на тезата на Чърч и Тюринг.

Всяка математическа теория на числата е непълна, не можем да докажем всичко вярно, оставяйки ескпериментирането (т.е. смятането) като единствена възможност.  Затова съм съгласен с Арнолд, че математиката е тази част от физиката, в която експериментите са евтини (т.е. смятаме вместо да блъскаме частици със скорост близка до тази на светлината).

Някой би възразил, че все пак това което успеем да докажем за естествените числа е вярно, но такова положение при физиката няма.  Това не е така, защото трябва да приемем нелогически аксиоми, като тази за индукцията, за верни.  Не виждам защо това е разрешено в математиката за разлика от физиката.  Имаме две възможности:

1. Декларираме, че математиката се занимава само с това което е изводимо или не, т.е. е формална игра на символи.

2. Приемаме, че понятия като естествените числа, с които смятаме всеки ден, са предмет на математиката.

Ако изберем възможност 2 приемаме че математиката се занимава с вярност, а не с изводимост.  Понеже тя е непълна сме във абсолютно съсщото положение, в което е и физиката.  Е, с изключението на по-евтините експерименти.

Тук виждаме че понятието изчислимост в смисъла на Чърч и Тюринг играе главната роля.  Комбиниранта с теоремата на Гьодел, тя изключва възможността да сведем 2 до 1.  Затова Хилбертовата програма се е провалила.  Можем да се запитаме, какво става ако разширим класа на изчислими функции.  Хората са изледвали засилени дефиниции на изчислимост като машини на Тюринг, които могат да се допитват до оракули.  Тези оракули дават отговори на конкретни (евентуално неразрешими) проблеми.  Оказва се, че тогава просто получаваме нов стоп проблем за тези по-мощни машини с оракули и всичко казано дотук се повтаря отново.

А, за комбинаториката също има нещо интересно: http://cs.nyu.edu/pipermail/fom/2007-June/011665.html

[Boyko Bantchev]

Ще добавя няколко бележки, но нека това не се смята за продължаване
на спора. Според мен някъде по пътя той изглежда доби почти изцяло
мирогледно съдържание, а това е терен, където не е много смислено да
се спори – става дума вече за разлики в понятията. Освен това темата
стана multifurcate :)
Поради инерцията да бъда провокиран от различно мнение все пак ще кажа
част от това, което в момента си мисля, но наистина вече не е заради
спора.

> Никой не се опитва да я превърне в _изцяло_ аксиоматична наука.
> Тогава не би била наука въобще, защото всяка наука е отчасти
> експериментална.

Да, но, както казах, физикът прави експерименти и за уж приети теории,
понеже всъщност никога не са окончателно приети. Математикът
експериментира _преди_ да докаже нещо, докато го търси. След това –
не, защото грамадна част от математическите резултати са фактически
окончателни. Пък и експериментите му имат съвсем друг характер.
Споменаваш хипотезите на Риман и Голдбах и изобщо недоказаното – че
там се експериментира. Да, но именно за недоказаното, а не след това.
„Експерименталността“ на математиката и физиката е различна и не ги
приравнява.

> акиоматизацията на физиката е номер 6 от Хилбертовите проблеми

Понеже цитираш източник на немски, а аз за съжаление не го разбирам,
привеждам текста на №6 от
http://en.wikipedia.org/wiki/Hilbert%27s_sixth_problem .
The investigations on the foundations of geometry suggest the
problem: To treat in the same manner, by means of axioms, those
physical sciences in which already today mathematics plays an
important part; in the first rank are the theory of
probabilities and mechanics.
Ясно се казва, че става дума за онези физически науки, които така или
иначе вече са в голяма степен математизирани. Е, моята теза е такава:
ако една (физическа или друга) наука се математизира и аксиоматизира
достатъчно, тя вече е … математика. Но тогава и престава да си служи
с експеримента така, както физиката. Тя вече не е физика. Другарят
Хилберт ни дава чудесни примери за това. На теорията на вероятностите
тогава явно се е гледало като на физика. Само че междувременно
лицето Колмогоров и „видя сметката“ като физика и я превърна изцяло в
математика. Днес никой не нарича ТВ физична теория. В двата
семестъра, в които я учих (това преди точно 30г.), нито веднъж не се
спомена думата „физика“. Монети също не хвърляхме и цветни топки от
кутия не вадихме. Същата работа е и с т.нар. аналитична механика
(също два семестъра, по точно същото време – много математика, никакви
експерименти). Във факултета по физика няма такива работи.

Впрочем, понеже стана дума кой какво бил казал: много често казаното
се разбира твърде дословно или казалият го е изразил някаква надежда,
но реалността е друга. Прочутата мечта на Лайбниц всичкото знание да
стане на смятане реалистична ли е? Едва ли. Ти преди цитира
известното мнение на Арнолд, че математиката и физиката са две страни
на една наука. Но това е повече афоризъм, отколкото строга концепция,
а и същият Арнолд обича да се шегува с това как физиците практикуват
„математика“ – не изглежда да ги има за колеги. Слави пък цитира
филмирана лекция на Файнман. Само че там човекът говори предимно за
математика и съвсем накрая единствен път употребява думата „аксиома“
във връзка с физиката. Изразява някаква вяра или по-скоро надежда.
Но пак Файнман в съседна лекция
http://www.youtube.com/watch?v=obCjODeoLVw
дава ясна представа за разликата между научния интерес на математѝка
и физѝка: теза, доста близка до моята. Та заради всичко това смятам,
че цитирането дава много малко или дори заблуждаваща информация,
особено като става дума за отделни изречения.

Накрая за отношението между ЕП (като C++ и Хаскел), от една страна,
и тезиса на Чърч от друга. Тук изобщо нямаме общ език. Например
ти казваш

> Подробностите в C++ и Haskell са безинтересни относно това какви
> изчислителни процеси моделират

което аз изцяло не разбирам. Явно под „изчислителни процеси“
разбираме различни неща и моето не е „изчислимост и сложност“.
Някъде нагоре изрично наблегнах на структурата и фо̀рмата на
процесите, но вече няма значение …

Край на спора, поне от мен. Трябва да кажа – и не го правя от
куртоазия – че повечето от него ми достави удоволствие. Благодаря! :)

[Slavomir Kaslev]

2013/12/14 Boyko Bantchev <boy...@gmail.com>

> Трябва да се изивиня публично

Да се извиниш определено е положителна стъпка – така се прави като
сбърка човек.  А ти направи грешки в много посоки, ще си позволя да
обърна внимание на това – не за да ти трия сол, а надявайки се да го
разбереш и избягваш да повтаряш същото.
    Нападаш лично, а не това, което казвам.

    За личните си нападки нямаш и основание – не ме познаваш, нито
работата ми.
    Агресията ти е непредизвикана: не съм се държал зле с теб в
никакъв смисъл.

Да, това е моя грешка. Тогава се обидих от това, че пиша математически

аргументи и сметки, а не получавам математически аргументи обратно

в спора. Аз нямам проблем с моите грешки, ако съм направил някъде

грешка в сметките се радвам когато някой да ме поправи. Но ако

математиката работи, философски аргумент не е достатъчен, за да

се каже, че даден подход е грешен.

 

    Държиш се крайно грубо, което само̀ по себе си, дори без оглед на
останалото, е неоправдано.
    Ако ще коментираш казаното от мен, постарай се без оценки, особено
пък категорични като „не си прав“, „говориш глупости“.  Оспорването
става с аргументи.
    Избягвай и високомерието.  Примерно, може да те е заинтересувала
темата „пораждащи функции“ или „комбинаторно броене“, но защо смяташ,
че за мен (или някой друг) е непозната?  Тези неща се развиват вече
около 90 години.

Простите числа са познати от хиляди години. Знаем какво точно е просто

число, обаче разпределението е все още мистерия. Много неща, са

познати, или ако не са, има информация за тях едно гугъл търсене 

разстояние. Това според мен това не ги прави по-малко интересни.

 

Сега, не става въпрос за репутацията ми, която споменаваш, а за
възможността за общуване, заради която се предполага, че сме тук.
Като се погазят правилата за общуване, то изчезва.  А е лесно да се
спазват, защото става дума за най-обикновена почтеност.

Ще ми се да приема извинението ти за искрено – иначе не бих писал
това.  Само че ще ми е по-лесно да го повярвам, ако в същото
изречение не беше сложил:

> сред многото чужди [идеи]

Чужди идеи не правя предмет на публикациите си, още по-малко да ги
представям за свои.  Цитираното е голословно твърдение, невярно и не
е в посока на нормално общуване.  И още веднъж напомням, че не сме
тук, за да обсъждаме мен.

Напълно съм съгласен.

 

~~~~~~~~~
П.П.:
1. Това, което на английски е continued fractions или chained
   fractions, на български е „верижни дроби“.  Аз не съм работил по
   тях, само съм ги споменал някъде.
2. Учебното пособие, за което казваш, че „bit rott-ва“, работи са̀мо
   с IE и SVGView, както е и написано там.  (По него време това беше
   единствената възможност.)

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Krasimir Angelov]

На 13 декември 2013, 22:05, Slavomir Kaslev <slavomi...@gmail.com> написа:
> 2013/12/13 Krasimir Angelov <kr.an...@gmail.com>

> Във всяко вярно доказателство (компютърно или не) трябва всичко да
> се обяснява в най-малките детайли. Плюса да ползваш компютър, е
> че може да ти помогне да видиш, че не си изпуснал нито един детайл.

Не съвсем. В книгите казват примерно ето сега от формула (1) и (2)
извеждаме (3). Самото извеждане включва прилагането на множество
аксиоматични стъпки като прилагане на комутативност, дистрибутивност и
т.н., но подробностите се пропускат. Единствено в учебниците за
първокласници можеш да видиш тези стъпки в подробности.

[Slavomir Kaslev]

2013/12/14 Krasimir Angelov <kr.an...@gmail.com>

Прав си, матемитиците обичат да изпускат стъпки, докато Coq не позволява.

Аз нямам никакъв опит нито на Coq нито на Adga (някой ден ще ги науча, но

не днес), но от това което съм гледал ми хареса, че ти показват каква е 

следващата цел/цели които трябва да докажеш. Един вид системата те 

асистира в това как ще си проведеш доказателството и ти показва случаи,

които ако смяташ на хартия е вероятно да изпуснеш. 

Според мен е неизбежно, че математиците ще превключат на подобни

инстументи; може би не Coq, но нещо подобно, защо не дори някакъв

визуален Coq. Ако не това поколение от математици, то някое следващо.

Разликата е, като да пишеш компютърни програми в тетрадка или да

използваш компютър където може си тестваш програмите.

Автоматичния превод от книги ми се струва много по-сложен от това

някой да ги пренапише на компютър. Но живеем в свят където съществуват

проекти като Emspripten и не бих се учудил ако дори има определени

успехи в тази насока. Но аз бих пресказал повече успех за пренаписване.

--
Slavomir Kaslev

[cutthroat]

Добре, спорът наистина тръгна да излиза извън контрол.  И аз ще добавя няколко бележки, т.е. моята гледна точка, без да се опитвам да доказвам каквото и да е било.

14 декември 2013, събота, 17:47:51 UTC+1, Boyko Bantchev написа:

Ясно се казва, че става дума за онези физически науки, които така или
иначе вече са в голяма степен математизирани.  Е, моята теза е такава:
ако една (физическа или друга) наука се математизира и аксиоматизира
достатъчно, тя вече е … математика.

За мен, нещо започнато като физика си остава физика.  Почти всичко в математиката има геометрична интерпретация.  За мен геометрията е просто абстрактна физика.  Алгебрата ни дава метод за пресмятане и систематизиране.  Геометрията е съдържанието.  Но и не отричам ползата от чисто формалното доказване, просто за мен то няма особено съдържание.  Същото мисля и за програмирането.  Изчислителен процес, описан чрез компютърна програма, дефинира законите за движение на системата, започвайки от възможните начални състояния.  И под движение, наистина имам предвид движение (в канторово пространство).  Информатиците трябва да изучават динамични системи :)

Преди аксиоматичният подход да стане толкова застъпен в математиката, хората пак са правели математика, чисто неформално, позовавайки се на интуицията.  Ойлер е правел чудеса с безкрайно малките величини.  Гаус дава много интересно топологично доказателство на фундаменталната теорема на алгебрата.  Обаче в доказателството има няколко допускания, които са доказани едва чак през 20-те години на миналият век.  Едно от тези допускания е: ако алгебрична крива влезе в ограничен регион, та задължително го напуска.  Което ми напомня и за известната теорема на Жордан:  всяка непрекъсната и непресичаща се затворена крива разделя равнината на две свързани компоненти.  Били са необходими много години, за да се докаже този очевиден факт, но никой не го е наричал "хипотеза".  Фактите са си факти.

Мисля, че математиката по онова време е била не по-малко математика от днешната, въпреки че не се е базирала на малък брой, добре подбрани аксиоми (и достатъчно големи кардинали).

Само да уточня

Ти преди цитира 
известното мнение на Арнолд, че математиката и физиката са две страни
на една наука.  Но това е повече афоризъм, отколкото строга концепция,

Доколкото съдя от изказа на Арнолд: http://pauli.uni-muenster.de/~munsteg/arnold.html това не ми изглежда въобще като афоризъм. 

В заключение: и аз благодаря за спора!  Накара ме да се замисля и да опиша доста мои схващания.  Мисля, че ги разбрах по-добре.

[Slavomir Kaslev]

14 декември 2013, събота, 17:47:51 UTC+1, Boyko Bantchev написа:

Ясно се казва, че става дума за онези физически науки, които така или
иначе вече са в голяма степен математизирани.  Е, моята теза е такава:
ако една (физическа или друга) наука се математизира и аксиоматизира
достатъчно, тя вече е … математика.

Аз съм съгласен с това. Според мен модерната наука е интер-дисциплинарна

(поради липса на по-добра дума). Това как ние наричаме една или друга

дисциплина е по исторически причини.

Какво ако се "математизира" биологията даден момент в бъдеще? Или химията?

Също ли ще ги наричаме математика или изчислителна биология или нещо друго?

Според мен не е от особено значение как ще ги наричаме.

 

--
Slavomir Kaslev