Mathesis universalis

Text-only Preview

Mathesis universalis
automatizovat poznavaniea tvorivy proces
vziat tvrdenie (prepisat ho formalne) rozbehnut mechanicky kalkul
a rozhodnut jeho pravdivost
takto postupne rozhodovat co ma byt dalsi bit basne a celu ju najst
okrem neuplnosti dostatocne silnych konzistentnychfragmentov matematiky je
ale problematicka uz i formalizacia beznychtvrdeni, nie je jasne ako
definovat konceptyako inovativnost boh apod
obideme tieto problemy tym ze ostaneme v prirodzenom jazyku zakodovanomdo
binarnych postupnosti a budeme s nim operovat v kalkulevyrokovej logiky
ktora je uplna
popiseme tento proces preciznejsie
zafixujme akekolvek standardne kodovanieprirodzeneho jazyka do
binarnych postupnosti
napr”a” je 0001, ”b”0010, ”” 0000 atd, text”ba a” je p otom ”0010000100000001”
vlastnost (resp tvrdenie o) binarnej postupnosti xmozme vyjadrit ako tvrdenie D(x)
pomocou vhodneho obvodu Dpozostavajuceho z logickych spojok AND (), OR ()
a NOT (¬):
J
J
J
J
x1

 

x2... 

xn
J
J
J
J
B
B
B
B
B
B
@
@
@




¬...
... ...


JJ
J
vystup
napr (x1x2)(¬x1∨¬x2) tvrdi ze v p ostupnosti x1,x2je prave jedna 1
1
podobne mozme vyjadrit vlastnosti premennych Cayako:
”ak Ckoduje obvod tak ten na vstupe ydava 1”, v skratkeC(y)=1
(Cje tu skratka pre c1,..., cm, podobne y=y1, ..., yn)
specialne nas budu zaujimat tvrdenia typu:
”ak (uzivatel) Ttvrdi/odmieta xpotom C(T, x)=1/0”,kde Cje znova
kodovane akoneznamy obvod
napr ”ak ykoduje axiom ci znamu teoremu ZFC1tak C(y)= 1 a C(¬y) = 0”
”ak Ttvrdi ze Invocation of l aughter je/nie je invencna basen
tak C(T, Invocation of laughter)=1/0”
po dost velkom mnozstve takychtoaxiom sa C”nauci” ako reagovat, najmensie C
splnujuce vsetky axiomy dane predoslymi skusenostami mozme interpretovatako
ich najefektivnejsie vysvetlenie
vysvetlenie Cje neznamy objekt a je problem ho najst
v skutocnosti ho ale najst nepotrebujeme, hoci ide o neznamy objekt
mozme s nim kalkulovat
a staci ak pouzitim jeho vlastnosti odvodime tvrdenia ktore nas zaujimaju
napr ”ak obvod Csplna C(b)=1/0 pre basne bpodla konkretneho navrhu
poetickeho kanonu (a kazdemensie Cnesplna niektoru z tychto axiom)
tak C(Ariel) = 1?”
”ak Csplna axiomy a zname teoremy ZFC (a mensie Cv tom zlyhavaju)
tak C(HypotezaK ontinua) = 1?”
korektne usudit tvrdenie A(x) z tvrdeni B1(x),..., Bi(x) mozme ak
kazde xsplnujuce B1(x) az Bi(x) splnujetiez A(x)
prikladom korektneho odvodzovacieho pravidlaje mo dus ponens:
ak mame B(x) a B(x)A(x) mozme odvodit A(x)
konecna mnozina takych pravidiel tvoridokazovy system ak
pomocou nich mozme odvodit kazde pravdive tvrdenie (platne pre kazdex)
napr modus ponens, axiomy (ktore mozme vidiet ako pravidla):
A(BA)
(A(BC)) ((AB)(AC))
(¬A→ ¬B)(BA)
a pravidla I,II ilustrovane nizsie tvoriataky system
1ZFC je teoria v ktorej sa da robit prakticky vsetkoco sa b ezne v matematikemoze
2
I. umoznuje nahradit dva identicke podobvody jednym
II. umoznuje rozdvojit podobvod pouzity na dvoch roznych miestach
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J



c
c
A B
A=B
−→
←−
I
II
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J
J



A
(pozn.: asa daju definovat pomocou a¬)
tj vsetko co mozme vydedukovatmozme vydedukovat uz pomocou modus ponens
a par zmienenych pravidiel, specialne mozme nimi simulovatvsetky ostatne
odvodzovacie pravidla
ak je ale odvodenie tvrdenia exponencialne dlhe je prakticky nerealizovatelne
ako rychlo mozme dedukovatpravdive tvrdenia?
mozme pravidlami uvedenymi vyssie odvodit kazdepravdive tvrdenie ktore
pozostava z nsymbolov dokazomktory ma symbolov nanajvys 10n2?
3