abclinuxu.cz AbcLinuxu.cz itbiz.cz ITBiz.cz HDmag.cz HDmag.cz abcprace.cz AbcPráce.cz
AbcLinuxu hledá autory!
Inzerujte na AbcPráce.cz od 950 Kč
Rozšířené hledání
×

včera 11:00 | Zajímavý software
Na Good Old Games je v rámci aktuálních zimních slev zdarma k dispozici remasterovaná verze klasické point&click adventury Grim Fandango, a to bez DRM a pro mainstreamové OS včetně GNU/Linuxu. Akce trvá do 14. prosince, 15:00 SEČ.
Fluttershy, yay! | Komentářů: 6
včera 07:22 | Pozvánky

Konference InstallFest 2018 proběhne o víkendu 3. a 4. března 2018 v Praze na Karlově náměstí 13. Spuštěno bylo CFP. Přihlásit přednášku nebo workshop lze do 18. ledna 2018.

Ladislav Hagara | Komentářů: 0
12.12. 20:22 | Nová verze

Před měsícem byla vydána Fedora 27 ve dvou edicích: Workstation pro desktopové a Atomic pro cloudové nasazení. Fedora Server byl "vzhledem k náročnosti přechodu na modularitu" vydán pouze v betaverzi. Finální verze byla naplánována na leden 2018. Plán byl zrušen. Fedora 27 Server byl vydán již dnes. Jedná se ale o "klasický" server. Modularita se odkládá.

Ladislav Hagara | Komentářů: 6
12.12. 10:22 | Zajímavý článek

Lukáš Růžička v článku Kuchařka naší Růži aneb vaříme rychlou polévku z Beameru na MojeFedora.cz ukazuje "jak si rychle vytvořit prezentaci v LaTeXu, aniž bychom se přitom pouštěli do jeho bezedných hlubin".

Ladislav Hagara | Komentářů: 13
12.12. 07:22 | Komunita

Od 26. do 29. října proběhla v Bochumi European Coreboot Conference 2017 (ECC'17). Na programu této konference vývojářů a uživatelů corebootu, tj. svobodné náhrady proprietárních BIOSů, byla řada zajímavých přednášek. Jejich videozáznamy jsou postupně uvolňovány na YouTube.

Ladislav Hagara | Komentářů: 0
11.12. 19:22 | Nová verze

Ondřej Filip, výkonný ředitel sdružení CZ.NIC, oznámil vydání verze 2.0.0 open source routovacího démona BIRD (Wikipedie). Přehled novinek v diskusním listu a v aktualizované dokumentaci.

Ladislav Hagara | Komentářů: 0
11.12. 09:22 | Pozvánky

V Praze dnes probíhá Konference e-infrastruktury CESNET. Na programu je řada zajímavých přednášek. Sledovat je lze i online na stránce konference.

Ladislav Hagara | Komentářů: 2
9.12. 20:11 | Nová verze

Byl vydán Debian 9.3, tj. třetí opravná verze Debianu 9 s kódovým názvem Stretch a Debian 8.10, tj. desátá opravná verze Debianu 8 s kódovým názvem Jessie. Řešeny jsou především bezpečnostní problémy, ale také několik vážných chyb. Instalační média Debianu 9 a Debianu 8 lze samozřejmě nadále k instalaci používat. Po instalaci stačí systém aktualizovat.

Ladislav Hagara | Komentářů: 14
9.12. 00:44 | Nová verze

Po 6 měsících vývoje od vydání verze 0.13.0 byla vydána verze 0.14.0 správce balíčků GNU Guix a na něm postavené systémové distribuce GuixSD (Guix System Distribution). Na vývoji se podílelo 88 vývojářů. Přibylo 1 211 nových balíčků. Jejich aktuální počet je 6 668. Aktualizována byla také dokumentace.

Ladislav Hagara | Komentářů: 4
8.12. 21:33 | Nová verze

Po půl roce vývoje od vydání verze 5.9 byla vydána nová stabilní verze 5.10 toolkitu Qt. Přehled novinek na wiki stránce. Současně byla vydána nová verze 4.5.0 integrovaného vývojového prostředí (IDE) Qt Creator nebo verze 1.10 nástroje pro překlad a sestavení programů ze zdrojových kódů Qbs.

Ladislav Hagara | Komentářů: 0
Jak se vás potenciálně dotkne trend odstraňování analogového audio konektoru typu 3,5mm jack z „chytrých telefonů“?
 (8%)
 (1%)
 (1%)
 (1%)
 (75%)
 (14%)
Celkem 979 hlasů
 Komentářů: 45, poslední 1.12. 19:00
    Rozcestník

    Z celého internetu píšu právě sem. Zajímá vás proč?


    Od určité doby jsou všechny texty které zde publikuji verzované na Githubu.

    Pokud najdete chybu, nepište mi do diskuze a rovnou jí opravte. Github má online editor, není to skoro žádná práce a podstatně mi tím usnadníte život. Taky vás čeká věčná sláva v commit logu :)


    Pokud se vám líbilo něco z mé produkce, můžete svou přízeň vyjádřit v kryptoměnách:

    • BTC: 13CS7yKTcqPQUH2hrcuFsqf1AKr4gThZTD

    Ne že bych je nějak potřeboval, ale patří to k věcem, které autory obecně potěší a jasně ukazují, že jsou lidi, kteří ty hodiny času stráveného psaním umí ocenit.


    Víte že můžete odebírat mé blogy pomocí RSS?

    Aktuální zápisy

    Knižní recenze: Gödel's Proof

    21.9. 00:02 | Přečteno: 1149× | Obecné IT | poslední úprava: 21.9. 14:08

    Gödelovy věty o neúplnosti patří k věcem, které podobně jako Turingův stroj, nebo Lambda calculus prostupují celým světem počítačů a narazíte na ně dřív nebo později všude. Písmeno ‚G‘ v GEBu je věnované právě Gödelovi, proto jsem byl už delší dobu zvědavý, na to co vlastně objevil, a o tom právě pojednává kniha Gödel's Proof.

    Gödel v podstatě ukázal, jak je možné i v omezeném setu axiomů a zdánlivě bezkonfliktním systému vytvořit paradoxy referencováním sebe sama. Kniha se věnuje tomu, jak k tomu došel. Nejde do úplných detailů (ty jsou v samotném důkazu), spíš se snaží čtenáři vysvětlit jednotlivé kroky, postupně v jednotlivých kapitolách za sebou.

    Kroky důkazu (a tedy i obsah knihy) postupují ve zkratce asi nějak takto:

    Zkoncentrovaný obsah

    Gödel vyšel z axiomatického systému definovaného v knize Principia mathematica od Whiteheada a Russela, která se snažila nadefinovat a odvodit celou matematiku pomocí logických axiomů.

    V tomto systému vymyslel způsob, jak překládat jednotlivé přípustné symboly axiomů na jejich jednoznačné číselné vyjádření (pomocí násobení prvočísel s exponentem kódujícím daný axiom). Tím je možné převést daný výraz v axiomatickém systému, například „0=0“ na axiomy 2, 6, 2 („2“ kóduje číslo 0, 6 kóduje symbol „=“), které pak převedeme na číslo zmíněným násobením:

    Což se rovná číslu 72900. Z tohoto čísla je pak možné metodou faktorizace prvočísel zpětně jednoznačně dostat původní písemný výraz.

    Gödel poté dokázal, že takhle je možné vyjádřit nejenom teorémy, ale i jejich důkazy. Kódování do čísel bylo důležité, aby se vyhnul chybám, které dělají lidé předpokládáním nějakého chování. Toho dosáhl tím, že se vyjadřoval o „bezvýznamných symbolech“ a umožnil čistě „mechanické“ kontrolování a odvozování podle pravidel axiomatického systému.

    Poté sestrojil výraz, který dokazuje pravdivost čísla enkódujícího teorém G, který má stejné vyjádření, jako svůj vlastní důkaz. Konkrétně:

    „Konkrétní přirozené číslo ‚g‘ není dokazatelné číslo.“

    Pokud však tomuto teorému enkódujícímu konkrétní důkaz předhodíme na vstup sám sebe, tak sám sebe vyvrátí. Jenže když se vyvrátí, tak se nemůže dokázat. Celé to bylo samozřejmě podstatně složitější, ale nemá smysl tady zacházet do detailů, tomu se věnuje zmiňovaná knížka.

    Jakmile měl Gödel první paradox, tak poté mohl zkonstruovat nekonečné množství podobných paradoxů, které vedly na výsledky, jako:

    „Tento teorém, i jeho negace není platným teorémem.“

    Gödel tím dokázal, že axiomatické systémy nemůžou být použity k „vytěžení“ celé matematiky iterací přes platné axiomatické výrazy, protože axiomatické systémy obsahují jednak paradoxy, které jsou nerozhodnutelné, ale také jakési ostrovy platných vět, ke kterým se není možné dostat odvozováním z axiomatických systémů.

    V knize je to samozřejmě popsané celé podstatně detailněji, a čitelněji. Určitě jí můžu jen doporučit. Četla se mi docela dobře i jako laikovi a je poměrně tenká.

    Gödelův důkaz má poměrně velké důsledky také pro sféru computer science, neboť ukazuje, že statická analýza je ze své podstaty nekompletní. To má své důsledky například při dynamické transformaci programů v lispovském stylu, ale také třeba pro analýzu virů, nebo dokázování korektnosti programu.

    Ukázka

    Nedá mi to, abych nevložil citaci několika stran, které se sice přímo netýkají důkazu, ale stejně na mě hodně zapůsobily krásnou analogií:

    It may be useful, by way of illustration, to compare meta-mathematics as a theory of proof with the theory of chess. Chess is played with 32 pieces of specified design on a square board containing 64 square subdivisions, where the pieces may be moved in accordance with fixed rules. The game can obviously be played without assigning any "interpretation" to the pieces or to their various positions on the board, although such an interpretation could be supplied if desired. For example, we could stipulate that a given pawn is to represent a certain regiment in an army, that a given square is to stand for a certain geographical region, and so on. But such stipulations (or interpretations) are not customary; and neither the pieces, or the squares, nor the positions of the pieces on the board signify anything outside the game. In this sense, the pieces and their configurations on the board are "meaningless", Thus the game is analogous to a formalized mathematical calculus.

    The pieces and the squares of the board correspond to the elementary signs of the calculus; the legal positions of pieces on the board, to the formulas of the calculus; the initial positions of pieces on the board, to the axioms or initial formulas of the calculus; the subsequent positions of pieces on the board, to formulas derived from axioms (i.e. to the theorems); and the rules of the game, to the rules of inference (or a derivation) for the calculus.

    The parallelism continues. Although configurations of pieces on the board, like the formulas of the calculus, are "meaningless," statements about these configurations, like meta-mathematical statements about formulas, are quite meaningful. A "meta-chess" statement may assert that there are twenty possible opening move for White, or that, given a certain configurations of pieces on the board with White to move, Black is mate in three moves. Moreover, general "meta-chess" theorems can be established whose proof involves only finite number of permissible configurations on the board. The "meta-chess" theorem about the number of possible opening moves for White can be established in this way; and so can the "meta-chess" theorem that if White has only two Knights and the King, and Black has only a King, it is impossible for White to force a mate against Black.

    These and other "meta-chess" theorems can, in other words, be proved by finitistic methods of reasoning, that is, by examining in turn each of a finite number of configurations that can occur under stated conditions. The aim of Hilbert's theory of proof, similarly, was to demonstrate by such finitistic methods the impossibility of deriving certain formally contradictory formulas in a given mathematical calculus.

    NAGEL, Ernest a James NEWMAN. Gödel's proof. Rev. ed. New York: New York University Press, 2008, s. 34-37. ISBN 9780814758373.

           

    Hodnocení: 100 %

            špatnédobré        

    Tiskni Sdílej: Linkuj Jaggni to Vybrali.sme.sk Google Del.icio.us Facebook

    Komentáře

    Vložit další komentář

    21.9. 08:29 Xerces
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Díky za pěknou upoutávku.
    mirefek avatar 21.9. 11:15 mirefek | skóre: 6 | blog: proc_dalsi_nazev
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Jo, tohle jsem si kdysi taky rozmýšlel, a coby počáteční impuls mi stačil čistě jenom Halting Problem, je to vlastně dost analogické tvrzení, a možná se o tom ani tak moc neví (knížku neznám, ale zdejší ajťáky by to mohlo zajímat).

    Halting Problem říká, že neexistuje algoritmus, který dostane na vstupu algoritmus, a v konečném čase odpoví, jestli algoritmus skončí, nebo ne. Dokazuje se to tak, že se za pomocí takového oracula sestaví algoritmus se sporným chováním -- jistou chytrou sebereferencí (tu teď nevysvětluji podrobně, mohl bych, pokud by byl zájem) se sestrojí algoritmus, který skončí právě tehdy, když o sobě rozhodne, že neskončí.

    A Gödelova věta se pak dá ukázat skoro stejně -- stejným sebereferenčním trikem se sestaví algoritmus, který dělá pouze to, že se snaží najít matematický důkaz, že se on sám nezastaví. A až ho najde, tak se spokojeně ukončí. V opačném případě prostě hledá a hledá napořád. (docela přirozené chování, řekl bych) Tak přesně vznikne výrok V (že se náš algoritmus zastaví), který je ekvivalentní výroku "dá se dokázat negace V".

    A po chvilce hraní je možné ukázat ekvivalenci výroku V s tím, že "formálně lze dokázat spor z ničeho", čímž se dostane slavný výsledek "Matematika je bezesporná právě tehdy, když to o sobě neumí dokázat."
    Bystroushaak avatar 21.9. 11:29 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Halting Problem říká, že neexistuje algoritmus, který dostane na vstupu algoritmus, a v konečném čase odpoví, jestli algoritmus skončí, nebo ne. Dokazuje se to tak, že se za pomocí takového oracula sestaví algoritmus se sporným chováním -- jistou chytrou sebereferencí (tu teď nevysvětluji podrobně, mohl bych, pokud by byl zájem) se sestrojí algoritmus, který skončí právě tehdy, když o sobě rozhodne, že neskončí.
    Jo, je to podobné, ale Göedel jde imho dál, protože rozšlapal bábovičky obecně axiomatickým systémům (kterým je imho i Turingův stroj), ale naopak to afaik neplatí.
    mirefek avatar 21.9. 12:08 mirefek | skóre: 6 | blog: proc_dalsi_nazev
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    To jo, Gödelova práce má rozhodně dalekosáhlejší filosofické důsledky.

    Jenom mi přišlo, že "ten trik" v důkazu je možnost sebereference tam, kde by člověk doufal, že to nepůjde. Jako je jasné, že věta "Tahle věta je nepravdivá" je taková nesmyslná, takže se naštěstí pomocí formálního jazyka nedá ani vyslovit. Proto člověka zarazí, že věta "Dá se dokázat negace téhle věty." vedoucí ke skoro stejným paradoxům už ve formálním jazyce dostat lze. A obzvlášť programátorovi bych to uvedl přes cvičení "Zkuste napsat program, který vypíše svůj zdrojový kód".

    A nemyslím si, že Gödel nějak zásadně "rozšlapal bábovičky", Russelův paradox byl imho pro matematiku o dost větší přůšvih. Gödel spíš akorát poukázal na to, že to jsou opravdu jenom "bábovičky" -- zbořil naivní představy, které nebyly ve skutečnosti ničím podložené. podobně jako byla ve starověku představa, že všechna čísla jsou racionální. Ale je to velký rámus, když padají ideály :-)
    21.9. 13:19 Abraxis
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    https://en.wikipedia.org/wiki/Quine_(computing) :)
    mirefek avatar 21.9. 15:02 mirefek | skóre: 6 | blog: proc_dalsi_nazev
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Díky, dobrý vědět, jak se to jmenuje.
    21.9. 13:33 Ondrej Santiago Zajicek
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Jako je jasné, že věta "Tahle věta je nepravdivá" je taková nesmyslná, takže se naštěstí pomocí formálního jazyka nedá ani vyslovit.
    Ona se neda vyslovit primarne proto, ze formalni jazyk se nezabyva pravdivosti, ale dokazatelnosti.
    Proto člověka zarazí, že věta "Dá se dokázat negace téhle věty." vedoucí ke skoro stejným paradoxům už ve formálním jazyce dostat lze.
    Problem je v tom, ze 'da se dokazat' neznamena presne to same na metaurovni logiky prvniho radu a pri reformulaci jazykem aritmetiky uvnitr logiky prvniho radu.
    A nemyslím si, že Gödel nějak zásadně "rozšlapal bábovičky", Russelův paradox byl imho pro matematiku o dost větší přůšvih.

    On to je obecny vyvoj matematiky smerem k vyssi preciznosti - nejdrive se prijde s nejakym intuitivnimi pristupem, pak se ukaze, ze pri neopatrne praci se clovek poreze, a nasledne se zavede preciznejsi formalizace. Napr. nekonecne mala cisla v analyze a epsilon-delta notace, ci naivni teorie mnozin s paradoxy a axiomatizovana teorie mnozin. Godelova prace ukazuje, ze si clovek musi davat pozor pri rozlisovani jednotlivych metarovin. Skolemuv paradox ukazuje, ze ani kardinalita neni absolutni meritko.
    21.9. 23:45 aaa
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Jako je jasné, že věta "Tahle věta je nepravdivá" je taková nesmyslná, takže se naštěstí pomocí formálního jazyka nedá ani vyslovit.
    Ona se neda vyslovit primarne proto, ze formalni jazyk se nezabyva pravdivosti, ale dokazatelnosti.
    Preco nie? Je to iba viac na strane semantiky. V modeli formule platia, v teorii sa hovori o dokazatelnosti. Ked je formula dokazatelna, tak je plati v kazdom modeli. Obratena implikacia plati vo vyrokovej logike.
    Jendа avatar 21.9. 14:08 Jendа | skóre: 74 | blog: Výlevníček | JO70FB
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Jo, tohle jsem si kdysi taky rozmýšlel, a coby počáteční impuls mi stačil čistě jenom Halting Problem
    Osobně jsem měl na složitosti asi největší WOW z věty, že busy beaver funkce je nevyčíslitelná. Gödelovy věty byly bohužel až na úplně poslední přednášce a nestihly se tak moc probrat (ale jinak Gregor přednášel pěkně).
    Why did the multithreaded chicken cross the road? to To other side. get the
    21.9. 12:46 Ondrej Santiago Zajicek
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Göedel tím dokázal, že axiomatické systémy nemůžou být použity k „vytěžení“ celé matematiky iterací přes platné axiomatické výrazy, protože axiomatické systémy obsahují jednak paradoxy, které jsou nerozhodnutelné, ale také jakési ostrovy platných vět, ke kterým se není možné dostat odvozováním z axiomatických systémů.
    Tady bych byl opatrnejsi. Predstava, ze je 'jedna matematika', kterou postupne objevujeme, a axiomy jsou nejake zjevene pravdy o ni, vzala za sve uz s Lobacevskym. Na matematiku lze pohlizet jako na prostor moznych struktur, ktery pomoci axiomu uchopujeme - vymezujeme si jimi ty struktury, ktere nas zajimaji (a podle toho jsme zvolili axiomy). Axiomaticky system je pak stale mozne pouzit 'k vytezeni' vsech pravdivych ci nepravdivych tvrzeni a dane tride struktur vymezene temi axiomy (to rika Godelova veta o uplnosti), ale jazyk predikatove logiky prvniho radu neni casto dostatecne precizni, abych jim byl schopen presne vymezit ty struktury, ktere me zajimaji (napr 'standardni prirozena cisla') od tech struktur, ktere uz me nezajimaji (napr. prirozena cisla rozsirena o nestandardni prvky).

    Nelze tedy mluvit (v predikatove logice prvniho radu) o 'ostrovech platnych vet, ke kterym se neni mozne dostat odvozovanim'. Pokud se k takove vete nelze dostat dokazovanim, pak neni platna (ve smyslu pravdivosti vety v teorii), nebot v nektere strukture popsane danou teorii ta veta neni pravdiva, prestoze v te strukture, ktera nas zajima, pravdiva je. Jina situace je v jinych formalnich systemech nez predikatova logika prvniho radu, kde nemusi platit Godelova veta o uplnosti. Tam mohou byt 'plne' pravdiva ale nedokazatelna tvrzeni.

    Tady bych jeste zminil mene proflaklou ale nemene zajimavou Lowenheim-Skolemovu vetu, ktera rika, ze i kdyz uz tu tridu struktur popisuji dostatecne presne (pomoci treba nerekurzivni ale spocetne sady axiomu) tak, ze vsechna tvrzeni jsou bud dokazatelna nebo vyvratitelna, stejne ty struktury mohou byt neizomorfni kvuli odlisne kardinalite.
    Göedelův důkaz má poměrně velké důsledky také pro sféru computer science, neboť ukazuje, že statická analýza je ze své podstaty nekompletní.

    Ty dopady mimo oblast matematiky a logiky bych zas tak vyznamne nevidel. Ve staticke analyze nepotrebuji vytvorit uplny system, ale staci mi najit takove (bezesporne) axiomy, ktere jsou dostatecne k dokazani tech tvrzeni, ktere me o kodu zajimaji. V praxi potom systemy na statickou analyzu kodu budou stejne pouzivat slabsi inferencni mechanismy, nebot mezi 'analyza dobehne za 200 let' a 'analyza nedobehne' uz zas takovy rozdil neni.
    Bystroushaak avatar 21.9. 14:11 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    21.9. 13:14 Sten
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Malá jazyková: Gödel nebo Goedel, ale ne Göedel
    Bystroushaak avatar 21.9. 14:07 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Bystroushaak avatar 21.9. 14:09 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Hrozný brain damage tohle. Jakože doslova jsem to nebyl schopný vidět.
    21.9. 13:47 Petr
    Rozbalit Rozbalit vše Re: Knižní recenze: Göedel's Proof
    Já četl toto https://www.levneucebnice.cz/p/neuplnost-dukaz-a-paradox-kurta-godela/, taky se mi to líbilo, je tam i něco o životě K.G., o jeho vztahu k Einsteinovi apod.

    Už je to nějaký pátek, co jsem to četl, ale já si to zapamatoval cca tak, že on dokázal, že každý systém který obsahuje aritmetiku, musí obsahovat i výroky, o nichž víme, že jsou pravdivé, ale nemůžeme je dokázat. Tím rozšlapal bábovičky všem hnutím formalistů, ti již měli mezi matematickými problémy pro 20.století něco jako "dokázat aritmetiku v rámci sama sebe". Dále jako vedlejší produkt dal naději, že člověk nemůže být jen velmi složitý stroj.
    22.9. 13:39 Ivorne | blog: Ivorne
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Tyhle teorie o logických paradoxech jsou tak trochu nesmysl. Je potřeba si dát velký pozor, jak se interpretují a mám pocit, že i velké množství lidí, kteří se jimi teoreticky zabývají (asi včetně Goedela), to často dělají nesprávně. Ty paradoxy nejsou ve skutečnosti v daném axiomatickém systému, ale jsou následkem nekorektního použití těchto axiomatických systémů.

    Je to jako ty výpočty, co se občas objevují na facebooku a podobně, kde na začátku máme jednoduchou rovnici 1=1 a po sekvenci zdánlivě korektních operací vznikne nesmysl jako třeba 1=5 (příklad: https://skullsinthestars.files.wordpress.com/2008/12/neg1equals1.png?w=640). Problém je vždycky v tom, že je tam jeden nekorektní krok, který se jenom těžko odhaluje. Typicky to bývá dělení obou stran rovnice nulou nebo umocňování obou stran rovnice, což je korektní jen za určitých podmínek. Stejně tak je to s těmi logickými paradoxy, ale tam tou nekorektní operací bývá referencování budoucnosti nebo sama sebe.

    Podle toho, co píšeš v blogu, si Goedel byl vědom rizika použití nekorektních operací: "Kódování do čísel bylo důležité, aby se vyhnul chybám, které dělají lidé předpokládáním nějakého chování.". Ale podle mě se mu stejně nepovedlo se tomu vyhnout. On sice zakóduje tvrzení do čísla, ale pak to vypadá, že s ním operuje zase pouze slovně a ne pomocí kódování. Protože kdyby se ten teorém "Konkrétní přirozené číslo ‚g‘ není dokazatelné číslo." pokusil zakódovat sám se sebou na vstupu, tak by se mu to nepovedlo, protože by neznal vstup (zakódovaný teorém) dokud by nedokončil kódování, což by zase nemohl udělat, když by ještě neznal celý vstup do toho kódování. Zkrátka řečeno - selže už jen snaha zakódovat ten teorém do čísla a k verifikaci toho teorému se vůbec nedostaneme. Čili ten teorém není součástí množiny teorémů popsatelných tím axiomatickým systémem. Čili to není paradox. To by bylo jako napsat kód v Javě a pak se divit, že ho nejde spustit pomocí interpreteru Pythonu.

    Napadl mě jednoduchý logický paradox, který ukazuje, jak jsou tyhle paradoxy nesmyslný koncept. Tvrzení je: "Pokud tvrdíš, že toto tvrzení je lež, pak říkám, že tráva je zelená. Pokud ale tvrdíš, že toto tvrzení je pravda, pak říkám, že tráva je současně čistě modrá i čistě červená.". Toto tvrzení je 'paradox', ale ne proto, že by byla nějaká vada v axiomatickém systému, ale proto, že ten text ve skutečnosti neobsahuje celé tvrzení. Nelze definitivně rozhodnout, co to tvrzení vlastně říká, protože je záměrně postaveno tak, že určitá jeho část bude vždy mimo dosah koholiv, kdo se pokusí ho verifikovat. A když nemám během verifikace k dispozici celé tvrzení, které se snažím verifikovat (a ani nemohu mít), tak ho těžko mohu verifikovat. Je to jako pokusit se verifikovat tvrzení "A==1" za situace, kdy neznám A a selhání pak svádět na chybu operace porovnání.

    Poučení, které by si měl člověk vzít z těchto teorií o logických paradoxech je, že lze snadno vytvořit tvrzení, které vypadá jako že vzniklo opakovanou validní aplkací základních axiomů axiomatického systému, ale ve skutečnosti tak vzniknout nemohlo. Exituje už i nějaká teorie o tom, jak se těmto 'paradoxům' vyhnout. Zkráceně řečeno stačí udělat tvrzení tak, že poposuje pouze věci z nižších logických metarovin (~věci v minulosti) a nepopisuje tedy nic ze svojí metaroviny (~věci v přítomnosti) nebo z vyšší metaroviny (~věci z budoucnosti). Bohužel k tomu nemůžu dlouhodobě najít žádné zdroje, takže jestli máte někdo odkaz, tak bych ho ocenil.

    Myslím, že se ty metaroviný dají aplikovat i tak, že řekneme, že tvrzení "Toto tvrzení je lež" je pravdivé v každé druhé metarovině a v těch ostatních je nepravdivé (je to prostě na střídačku vždycky pravda a lež). Prostě řekneme, že tvrzení označované výrazem 'toto tvrzení' ve skutečnosti označuje stejně formulované tvrzení v o jedna nižší metarovině a verifikace potom rozhoduje o tom, ve kterých všech metarovinách je tvrzení pravdivé a ve kterých ne.
    22.9. 15:13 Ondrej Santiago Zajicek
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Tyhle teorie o logických paradoxech jsou tak trochu nesmysl. Je potřeba si dát velký pozor, jak se interpretují a mám pocit, že i velké množství lidí, kteří se jimi teoreticky zabývají (asi včetně Goedela), to často dělají nesprávně. Ty paradoxy nejsou ve skutečnosti v daném axiomatickém systému, ale jsou následkem nekorektního použití těchto axiomatických systémů.

    To je castecne pravda pro ruzne 'verbalni' paradoxy a pro ruznou snahu vysvetlit ty paradoxy laikum pomoci prosteho textu (ktery byva nedostatecne precizni pro tyto ucely) a pripadne pro uvahy o ruznych 'filosofickych presazich' tech paradoxu, nicmene existuji korektni logicke a matematicke paradoxy a ty odmitnout nejde.

    V podstate jde o dva typy paradoxu: 'Prave' paradoxy, antimonie, ktere ukazuji na zasadni chybu v teorii nebo v metode inference (napr. znamy Russelluv paradox a Kleene–Rosseruv paradox), a pak 'neprave' paradoxy, paradoxni stav veci, kde je teorie, logika i odvozeni v poradku, ale (spravny) vysledek je ve vyraznem rozporu s nasim intuitivnim chapanim a casto vede k presnejsi konceptualizaci dane problematiky. To je priklad treba Banach-Tarskeho paradoxu ci Skolemova paradoxu, nebo prave Godelovych vet.
    Bystroushaak avatar 22.9. 16:27 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Podle toho, co píšeš v blogu, si Goedel byl vědom rizika použití nekorektních operací: "Kódování do čísel bylo důležité, aby se vyhnul chybám, které dělají lidé předpokládáním nějakého chování.". Ale podle mě se mu stejně nepovedlo se tomu vyhnout. On sice zakóduje tvrzení do čísla, ale pak to vypadá, že s ním operuje zase pouze slovně a ne pomocí kódování. Protože kdyby se ten teorém "Konkrétní přirozené číslo ‚g‘ není dokazatelné číslo." pokusil zakódovat sám se sebou na vstupu, tak by se mu to nepovedlo, protože by neznal vstup (zakódovaný teorém) dokud by nedokončil kódování, což by zase nemohl udělat, když by ještě neznal celý vstup do toho kódování. Zkrátka řečeno - selže už jen snaha zakódovat ten teorém do čísla a k verifikaci toho teorému se vůbec nedostaneme. Čili ten teorém není součástí množiny teorémů popsatelných tím axiomatickým systémem. Čili to není paradox. To by bylo jako napsat kód v Javě a pak se divit, že ho nejde spustit pomocí interpreteru Pythonu.
    Tady děláš klasickou internetovou chybu, a to je že se snažíš odvodit smysluplnost či pravdivost na základě popisu, místo věci samotné. Celé jsem to samozřejmě tisíckrát zjednodušil, samotný důkaz je podstatně rigoróznější, než to co jsem napsal já. Fakt doporučuji si tu knížku přečíst, nebo přímo důkaz samotný. Ostatně, Gödel o tom přesvědčoval matematiky, včetně samotných tvůrců Principie Mathematiky, tak je ten jeh důkaz na jiné úrovni. Já jsem v matematice jen laik.
    22.9. 20:39 Ivorne | blog: Ivorne
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Jsem tušil, že mi tohle vytkneš. Ale na mojí pointě to nic nemění. Vyznám se spíš v halting problému. O tomhle zobecnění na všechny výpočetní modely jsem ale taky už dřív slyšel a nevidím v pointě těch důkazů velký rozdíl.

    Vem si třeba právě ten halting problém. Tam se v podstatě říká, že existuje aspoň jeden program u něhož nelze určit, zda skončí nebo ne. Důkaz toho tvrzení spočívá v tom, že se popíše ten neurčitý program. Ale vem si, že ten program se nedá reálně sestrojit. To, že existuje nějaký popis toho programu přece neznamená, že ten program existuje nebo že jde napsat. Ten popis toho programu pouze působí dojmem, že se dá vyrobit malou úpravou jiného existujícího programu (programu, který určí, zda program na vstupu někdy skončí). Ale reálně se sestrojit nedá. Ta malá úprava ve skutečnosti do celého procesu sestavení toho programu zavádí nutnost znát budoucnost (nutnost znát podobu programu ještě dřív než ho sestavíš). Takže se ve skutečně nejedná o zas tak malou úpravu.

    Takže sice nejde napsat program, který pro každý program na vstupu určí, zda ten program skončí nebo ne. Ale jde napsat program, který pro každý napsatelný program určí, zda skončí, nebo ne. A protože množina nenapsatelných programů, o kterých by tě zajímalo, zda skončí nebo ne, je nejspíš prázdná, tak je důkaz neurčitosti halting problému celkem k ničemu.
    Bystroushaak avatar 22.9. 22:08 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    O tomhle zobecnění na všechny výpočetní modely jsem ale taky už dřív slyšel a nevidím v pointě těch důkazů velký rozdíl.
    Jo, já o tom taky slyšel, jenže co tak chápu, tak to co jsi napsal stejně není řešení všech paradoxů. Spíš mi šlo o to, abys moc nespoléhal na to co jsem psal, protože jak to funguje vím asi měsíc a nikdy dřív jsem to nestudoval.
    Vem si třeba právě ten halting problém. Tam se v podstatě říká, že existuje aspoň jeden program u něhož nelze určit, zda skončí nebo ne. Důkaz toho tvrzení spočívá v tom, že se popíše ten neurčitý program. Ale vem si, že ten program se nedá reálně sestrojit. Ale vem si, že ten program se nedá reálně sestrojit. To, že existuje nějaký popis toho programu přece neznamená, že ten program existuje nebo že jde napsat.
    Proč by se nedal reálně sestrojit? V tomhle tvůj argument úplně nechápu.
    mirefek avatar 23.9. 00:14 mirefek | skóre: 6 | blog: proc_dalsi_nazev
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Takže sice nejde napsat program, který pro každý program na vstupu určí, zda ten program skončí nebo ne. Ale jde napsat program, který pro každý napsatelný program určí, zda skončí, nebo ne. A protože množina nenapsatelných programů, o kterých by tě zajímalo, zda skončí nebo ne, je nejspíš prázdná, tak je důkaz neurčitosti halting problému celkem k ničemu.
    To teda těžko, leda že by ten program, co "jde napsat", byl nenapsatelný :-D

    Jinak by mě zajímalo spousta programů, jestli skončí, nebo ne. Třeba takový program, který hledá sudé číslo větší než dva, které se nedá rozložit na součet dvou prvočísel, a skončí, až ho najde.
    mirefek avatar 23.9. 01:13 mirefek | skóre: 6 | blog: proc_dalsi_nazev
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Tady je když tak kód toho programu, který mě zajímá, napsaný v Pythonu, abych demonstroval, že je napsatelný. Netvrdím, že se jedná o nerozhodnutelný problém (kdybych to věděl, tak bych musel mimo jiné vědět, že ten program neskončí, což se u nerozhodnutelných problémů dělá těžko). Ale dost pochybuji, že by takový kód šel předložit nějakému existujícímu automatu, a ten mi dal odpověď. Nejnadějnější by mohly být dokazovací automaty (když nebude vadit mrtě velký výpočetní čas), ale jak je patrné právě z Gödelovy věty, ani ty nejsou dokonalé.
    def is_prime(n):
        if n < 2: return False
        for d in range(2, n):
            if n%d == 0: return False
        return True
    
    def is_decomposable(n):
        for n1 in range(1, n):
            n2 = n - n1
            if is_prime(n1) and is_prime(n2):
                print("{} = {}+{}".format(n, n1, n2))
                return True
        return False
    
    n = 4
    while is_decomposable(n): n += 2
    print("{} is not decomposable".format(n))
    
    Jendа avatar 23.9. 02:24 Jendа | skóre: 74 | blog: Výlevníček | JO70FB
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Ale jde napsat program, který pro každý napsatelný program určí, zda skončí, nebo ne.
    Ale když máš takový program, volání podprogramů a podmíněný skok (což jsou IMHO featury, bez kterých by tvůj výpočetní model byl nepoužitelně slabý), tak můžeš sestrojit přesně ten program, o kterém jsi před chvílí napsal, že reálně sestrojit nejde:
    def trolling(program):
      if willHalt(program, program):
        while True:
          pass
    
    (což je napsatelný program, protože jsem ho právě napsal :), a o programu volajícím trolling(trolling) nelze říct, jestli se zastaví, nebo ne)
    Why did the multithreaded chicken cross the road? to To other side. get the
    23.9. 08:32 zvol
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Tam se v podstatě říká, že existuje aspoň jeden program u něhož nelze určit, zda skončí nebo ne.
    To se tam ale právě neříká.
    23.9. 13:19 deda.jabko | skóre: 23 | blog: blog co se jmenuje "každý den jinak" | za new york city dvakrát doleva a pak už se doptáte
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    A protože množina nenapsatelných programů, o kterých by tě zajímalo, zda skončí nebo ne, je nejspíš prázdná
    To je prave chybny predpoklad. Testovat programy, o kterych vis, ze skonci, by bylo asi stejne prinosne, jako divat se na fotbalovy zapas, o kterem vis, jak dopadne.

    Nechci rozjizdet dalsi flame, ale halting problem mi prijde takovy precenovany. Je to proste takove to popularni tema, ke kteremu se da jednoduse vyjadrovat i po patem pivu. Pricemz ve vycislitelnosti jsou podle me mnohem hezci a praktictejsich veci. Napada me treba kombinator pevneho bodu v lambda kalkulu, churchovo kodovani cisel, a kdyz jsme u toho i nerozhodnutelnost, zda jsou dva lambda vyrazy ekvivalentni. Cimz se obratem dostavame k problemum typu zastaveni, pricemz tato formulace muze vypadat uzitecneji, nez problem zastaveni.
    Asi před rokem se dostali hackeři na servry Debianu a ukradli jim zdrojové kódy.
    23.9. 00:10 NaN
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Liško Bystrouško, zmizela ti adresa etherea. Proč ? Já bych spíš čekal, vzhledem k událostem, že ti zmizí adresa bitcoinu.
    Bystroushaak avatar 23.9. 00:38 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Dal jsem jí pryč protože tam nikdy nikdo nic neposlal. A taky protože jsem zapomněl heslo, a šestihodinový BruteForce složený z mých běžný hesel nepomohl :S Ještě štěstí že tam nic nebylo.
    23.9. 15:09 NaN
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Chápu, investoval jsi ale přece do etherea ne ? Jak vidíš jeho budoucnost ? Respektive jaký máš celkově názor na vývoj technologie blockchainu? Jaký bude podle tebe svět za 10 let ?
    Bystroushaak avatar 23.9. 15:57 Bystroushaak | skóre: 32 | blog: Bystroushaakův blog | Praha
    Rozbalit Rozbalit vše Re: Knižní recenze: Gödel's Proof
    Investoval jsem do všeho možného, ne jenom Etherea. Momentálně jsem investoval například do Sia coinu a Dao (do obojího ale jen pár tisíc). Z Etherea jsem měl vyšší desítky tisíc, ale prodal jsem ho moc brzo. Kdybych s tím počkal půl roku tak jsem si za to mohl koupit například byt. Tohle je obecně problém krypto-měn, že nikdy nevíš jestli už je to na vrcholu, nebo to bude dál stoupat. Zrovna Ether v té době padl na docela málo, a čtvrt půl roku byl relativně nízko, a mě už fakt nebavilo to sledovat a řešit, tak jsem se ho zbavil.

    Blokchain má samozřejmě budoucnost, včetně etherea. Myslím že Ethereum je momentálně ze všeho nejperspektivnější co do technologie, myšlenky, provedení a skupiny lidí, co za ním stojí. Pomalu se ale vynořují i další krypto-měny založené na myšlenkách podobných chytrým kontraktům. Například ten Sia. Podle mě se brzké době objeví hodně různých vyrovnávacích měn, které budou nabízet výměnu například výpočetního výkonu za coin, který později můžeš vyměnit zpět za výpočetní výkon, nebo třeba za úložný prostor, nebo louskání captchi. To je docela praktická věc, proto si myslím, že jich bude všude kopec. Peníze podložené reálnou věcí, jako je třeba gigabajt prostoru na hodinu, které získáš když nabídneš gigabajt prostoru na hodinu, a můžeš si vyzvednout, když nabídneš patřičný coin. Stará dobrá směnná jednotka, asi jako když byly dřív peníze podložené zlatem a fakt jsi mohl přijít do banky a nechat si za ně vyplatit to zlato. Taky to bude mít výhodu, že nebudeš zbytečně pálit výkon, jako v případě bitcoinu.

    Myslím že Ethereum bude dlouhodobě sloužit jako technická platforma pro realizaci, a to i v daleké budoucnosti, i když samotné zas tak zajímavé není a vzniknou zajímavější nápady a realizace. Jedna z těch původních myšlenek totiž byla, aby se na tom daly stavět různé další nápady, bez toho abys musel řešit všechny možné technické detaily, jako je například navazování spojení v P2P sítí, nebo ověřování jednotlivých klientů. Z Etherea se tak může časem stát něco podobného, jako TCP/IP; takový základní podkladový protokol pro stavbu zajímavějších uživatelských nápadů.

    Já už celou tu scénu zas tak moc nesleduju, což je nejspíš moje vlastní škoda. Jenže to žere tak moc času, že mě to nebaví. Dostal jsem se ale omylem do docela divné pozice, kde platím za experta na krypto-měny, takže mi píšou lidi na email s různými doporučeními, nebo žádostmi o radu. Například jsem takhle radil nějaké ženské co má napsat do bakalářky. Taky mě překvapilo kolik lidí mě referencuje v různých pracích, když jsem si hodil URL do google. Přitom to není tak že bych měl nějaké extra znalosti, všechno co vím si může načíst každý během pár týdnu čtení.

    Moje představa budoucnosti je trochu rozebraná v blogu Vytváření prostorů otevíráním dimenzí. Specificky v té koncové části. Ethereum má podle mě slušnou šanci se stát podkladovou jednoticí platformou pro IoT. Mluvil jsem o tom s několika různými lidmi, například s Vladem Kahounem z broadapi, nebo na pohovoru s Nordic Telecomem, kde se tvářili, jako že je to fakt hodně zajíma, a že by na tom chtěli stavět produkty.

    Sám nad tím momentálně nic nestavím, protože nemám čas. Práce mi žere většinu produktivního času. Ten zbytek věnuju programování věcí, které jsou pro mě momentálně zajímavější, a psaní (ať už blogů, nebo knížky, nebo věcí které jsem zatím nepublikoval a publikovat nehodlám). Rád bych dneska publikoval blog s detaily.

    Mimochodem tenhle příspěvek byl z velké části nadiktována na iPhonu, v rámci experimentování s různými divnými uživatelským rozhraními.

    Založit nové vláknoNahoru

    ISSN 1214-1267   www.czech-server.cz
    © 1999-2015 Nitemedia s. r. o. Všechna práva vyhrazena.