Posted By: Earl (Earl) on 'CZscience'
Title:     Re: Pocitacove dokazovani
Date:      Wed Sep  3 12:45:35 1997


 HI.

> > problem vytvorit celou axiomatiku iterovanim nejakych pravidel na jeji
> > axiomy. Kazda veta neodpovidajici formalnimu dukazu neni dokazatelna.

> To je sice lakava idea, ale asi nikdy nebude mozne, aby pocitace touto
> hrubou iterativni silou hledaly nove zajimave vety. 

 Ano, pocitac nepozna, jestli je veta zajimava ci nikoliv. Ale vygeneruje
je UPLNE vsechny. Vsechny mozne. Fakt je snad jen ten, ze se bude jedna
a tataz veta opakovat v mnoha obmenach (napr. vetu-implikaci lze vyjadrit
jako disjunkci, typy kvantifikatoru lze prevadet jeden na druhy, ...).

 Takze jediny problem je ten, ze by pak musel nekdo nad tu spoustu sednout
a spravne ji interpretovat. Pokud si da praci, objevi NOVE ZAJIMAVE VETY.
Vznikle ciste iterativni cestou.

 Historicka poznamka. Lobacevskij sam priznava, ze pri budovani sve axiomatiky
pracoval naprosto systematicky, presne a automaticky. Ale jeho dilo jsem
necetl, takze no more comment :)

> Je to podobne, jako 
> kdybys pocitac nechal vypisovat postupne vsechny stopismenne texty 
> "aaaaaa....aaa", "aaaaa....aab"... a cekal, az ti z toho vypadne Romeo a 
> Julie. 

 Tak tady se rozejdeme velice radikalne. Veta "aaaaa...aaaa" nedava smysl
a neda se skoro vubec (neco mozna ano) interpretovat, kdezto vety 
generovane 'axiomatickou dedukci' nejenom splnuji gramatiku jazyka, 
ale maji vsechny pravdivostni hodnotu TRUE.

---

 Ja zase zacinam verit, ze matematicka logika podobne jako sachy neni
intelektualni zalezitosti, protoze existuji exaktni pravidla, ktera ji
generuje, tudiz je programovatelna. Nekteri lide maji 'hardwarovou podporu',
nebo vidi do Akasicke knihovni, sekce 'Math', nebo jeste neco jineho, cehoz
dusledkem je, ze matiku zvladaji lepe jak ostatni.

 Tento fakt se mi navic jevi jen a pouze jako dusledek vysoke schopnosti
abstrakce. Matematika je schopnost abstrakce. Vsechny ostatni obory se
zabyvaji uz jen datarinou. Matika se zabyva generovanim nejen dat, ale 
i algoritmu na generovani, algoritmu, ktere generuji algoritmy, ktere
generuji, ...

 Neni to fantas-magorie?

E.L.
                                                          Earl.