Formalizácia ultrafinitizmu

zmysel slov je dany ich pouzitim

  pravidla pouzitia slov mozme nasledovat vzdy viacerymi nekonzistentnymi sposobmi

    zmysel pravidiel ktory nakoniec pouzivame je ten najkrajsi. tym je urcene co je krasne ci efektivne


svet je totalita faktov

  svet nasu skusenost mozme pouzit ako jazyk verejny a objektivny
    ak hovorime o niecom co nejde vyjadrit vyjadrujeme presne to co hovorime
      vyznam slov nieco nevyjadritelne neukazatelna skusenost bolest ktoru nik iny neciti.. je presne dany ich pouzivanim a nic viac neznamena

  kazdu skusenost mozno nazvat jedinecnym slovom
    slova pouzivane v suvislostiach v akych vystupuju korespondujuce skusenosti znamenaju to co tieto skusenosti


kazdy jazyk v ktorom dokazeme hovorit o pojmoch ako nekonecno je konecny. slova su prepisatelne do binarnych. tvrdeni je v kazdom okamihu konecne mnoho a su konecnej dlzky

  objekt je konecny ak vieme prejst krok za krokom vsetky jeho prvky
    ak by sme to dokazali zo skusenosti nekonecne krat vyznam slova konecne by sa zmenil

  nasa skusenost s neustalym sa vynaranim novych veci je vyjadrena v pravidlach ako "pre kazde x existuje x+1". tie urcuju vyznam nekonecna
    nemozeme prejst krok za krokom vsetky prvky nekonecna. ak by to boh dokazal porusil by logiku/pouzitie toho pojmu

  mozme tvrdit ze existuje nekonecno ci nieco nevyjadritelne ale nebude to znamenat nic viac nez to co je dane konecnym mnozstvom konecnych vyjadreni


totalita faktov vsak neni len konecna je dosiahnutelna

  tvrdit ze pre kazde x plati Tx znamena ze pre kazde x s ktorym mame skusenost plati Tx
    ak napr nemame algoritmus pre nejaku ulohu tak (realne) neexistuje aj ked ho mozme zajtra najst

  v matematike pouzivame kvantifikacie inak aj ked nieco realne neexistuje netvrdime ze to neexistuje kym to nevyvratime
    kladieme doraz na minimalitu axiom kvoli (uspokojivejsiemu) vysvetleniu faktov (a jasnejsiemu vymedzeniu tych ktore sa zajtra zmenia)


je efektivne rozhodnutelne v akych suvislostiach su fakty pouzite napr kedy tvrdime ze su pravdive

  aj ked je realne vsetko jasne hladame nove veci ako napr vysvetlenie faktov z minimalnych axiom

  kazdy algoritmus rozhodujuci pravdivost tvrdenia v beznej mat teorii sa myli na istom explicitne danom vstupe ak je ta teoria konzistentna
    mozme ale (efektivne) nachadzat dosiahnutelne dokazy tvrdeni?

    existuje (efektivny) algoritmus ktory pre dane (efektivne overitelne) kriteria dokaze skonstruovat text ktory ich splnuje (ak taky text existuje)?


ukazat ze je problem lahky ma skutocne zmysel len konstrukciou algoritmu ktory ho riesi. teda dokaz existencie algoritmu ma skutocne zmysel len v teorii kde je dokaz existencie vzdy dosvedceny konstrukciou. v dosiahnutelnej matematike (fm)

  ukazat obtiaznost problemu ma zmysel len konstrukciou algoritmu (efektivne) dosvedcujuceho chyby kazdeho potencialneho algoritmu pre tento problem
   inak v skutocnosti nie sme schopni rozpoznat ze dany algoritmus nefunguje a prakticky tak moze byt problem lahky


fm pozostava z dokazov v akejkolvek formalizacii matematiky (zfc a rozsirenia) tz pre kazde dokazane tvrdenie typu existuje y A(x,y) existuje efektivna funkcia f tz A(x,f(x,n)) kde n je dlzka dokazu

  ak v fm nejde vysvetlit neexistenciu algoritmu pre nejaky problem a realne taky algoritmus nemame je prirodzene prijmut to ako zakon
  ak ale nejde vysvetlit neexistenciu takeho algoritmu v ziadnej konzistentnej teorii potom taky algoritmus existuje