(P1) Model ve výrokové logice, pravdivostní funkce výroku.
- tu clovek proste nemoze urobit chybu inak je v pici, dokaze to ak si zoberie nejaky pekny priklad a odskusa si to, ukaze ze tomu rozumie
- vo vseobecnosti je funkcia definova ako "f: domain -> range" vieme ze sme vo vyrokovej takze bud to bude platit alebo ne - range. Domain no to je abeceda nad ktorou rozmyslame sme v binarnej teda 0 a 1.
- Model preto bude string 0 a 1, vzavislosti od poctu premennych v danom jazyku
- pravdivostna funkcia same shit
(P2) Sémantické pojmy (pravdivost, lživost, nezávislost, splnitelnost) v logice, vzhledem k teorii.
- tu je to najlepsie popisovat cez modely, to ze je nieco vzhladom k teorii tak len hovori ze cim viac axiomov musi platit, tym menej modelov to bude splnovat, teda vo vseobecnosti M(T)⊆M(φ)
- jazyk L sa nemeni nikdy takze to len tam treba opisat
(P3) Ekvivalence výroků resp. výrokových teorií, T-ekvivalence. (e*x = x*e)
- opat raz teoriu raz len vyrok ...
- ekvivalentne znamena rovnake modely
(P4) Sémantické pojmy o teorii (sporná, bezesporná, kompletní, splnitelná).
- opat je podla mna najlepsie cez modely to urobit
(P5) Extenze teorie (jednoduchá, konzervativní), odpovídající sémantická kritéria.
1. extenze ML(T`) ⊆ ML(T) resp. CsqL(T) ⊆ CsqL`(T`) kde csqLT su vsetky φ ktore musia byt nutne pravdive v danom jazyku pre teoriu T
- Ak mame T={P∨Q,¬P} tak nutne Q musi byt pravdive lebo inak T nemoze byt splnitelne
- Tak isto aj PeanoA ma csq co su vlastne vsetky pravdy ktore vyplyvaju z axiomov - neutralny prvok alebo komutativnost
2.konzExt CsqL(T) = CsqL(T`) = CsqL`(T`) ∩ FmL
- FmL znaci fuck my life resp. vsetky ForMule v L
- hovorime iba o tom ze platilo to co predtym ale rozsirili sme jazyk o nejaku novu picovinku a plati tam to iste a este aj nejaka mala drobnost navyse, ktora nijako nemodifikuje minule pravdy
- mame funkcnu T a pridame tam c=420, zjavne teda plati to iste co predtym ale vieme opat len lepsie refrencovat nejaky fakt
- teoria grup (inverzny, neutralny, asociativita), pridame tam P(x) co bude hovorit ze kazde cislo vieme vynasobit samym sebou a dostaneme ine cislo z grupy - vsetko funguje tak ako predtym len sme schopny lepsie referencovat nejaku novu schopnost
- teda robime nieco ako prefixovy sucet na neklesajucej postupnosti
3.ekvivalence ML(T`) = ML(T) resp T je ext T' ale aj T' je ext T
4.jednoducha ext L'=L
(P6) Tablo z teorie, tablo důkaz.
(P7) Kongruence struktury, faktorstruktura, axiomy rovnosti.
Z7 je faktorstruktura napr, existuje iba 7revirov ktore existuju.
(P8) CNF a DNF, Hornův tvar. Množinová reprezentace CNF formule, splňující ohodnocení.
0. literal value = 0 or 1 pre nejaku premennu p
1. mnozinova reprezentacia je CNF teda empty S je vzdy splnena lebo konjunkcia, kdezto ale empty C je vzdy nesplnena lebo disjunkcia
2. ohodnotenia V:
castocne ohodnotenie - neobsahuje l aj l' zaroven
uplne ohodnotenie - obsahuje l xor l' pre kazde p
ohodnotenie - kazda C ma aspon jeden l ktory v nej zastupuje pravdivost aby CNF C bola true
(P9) Rezoluční pravidlo, (nejobecnější) unifikace, rezoluční důkaz a zamítnutí.
jasne z cvika
(P10) Signatura a jazyk predikátové logiky, struktura daného jazyka.
- Sig: Signatura nam len dava predpis arit tak ako override classa (struktura je specificky objekt implementovanej classy).
- Mame RuF->N lebo arita R moze byt S(r,z,t,p) ale aj R(a,b,c) takze mame 3 aj 4. Funkcie mozu byt iba unarne napriklad, konstantny symbol ma aritu 0, kedze ale arita nema obmedznie zhora moze to byt hocijake cele kladne cislo.
(P11) Atomická formule, formule, sentence, otevřené formule.
- ak je formula otvorena a aj sentence zaroven, termy su konstanty
(P12) Pravdivostní hodnota formule ve struktuře při ohodnocení, platnost formule ve struktuře.
- formula φ=(P∧Q)→P nech ma ohodnotenie v(P)=1,v(Q)=0 zistime ze plati, teda φ je pravdiva strA pri ohodnoteni v.
V predikatovej podobne, majme strA = (A,R^A) v jazyku L={R} kde A={1,2,3} ale R^A={1,3} tak formula φ=R(x) bude zjavne pravdiva pre v(x)=1 a pre v(x)=3 ale nie pre =2
- platnost - spravi sa tabulka s 2^n prvkami a pytame sa ci to plati vsobecne alebo vobec alebo pri nejakych istych predpokladoch, napr (P∧Q)->P je tautologia a plati pre vsetky 4vstupy PQ={01,00,10,11} ale moze existovat formula ktora plati iba ak R je pravdive (nejaka konjunkcia zakladna).
V predikatovej napr usporiadanie kde medzi 2 prvkami existuje dalsi neplati pre Z lebo medzi 2 a 3 nic nieje ale pre Q to plati zoberieme aritmeticky primer a ten konverguje k A=B
(P13) Kompletní teorie v predikátové logice, elementární ekvivalence.
kompletna: T⊢φ or T⊢-φ, DeLO* bez endpointov
ee: rovnake modely
(Q,<) neni izomorfne s (R,<) v T=DeLO* bez endpointov (lebo su inej velkosti spocetne/nespocetne nekonecno nejde spravit bijekcia), ale su ee lebo DeLO* je kompletna T lebo kazdy model DeLO* je izomorfny (Q,<) [je to T11 ]
(P14) Podstruktura, generovaná podstruktura, expanze a redukt struktury.
A=Naturals; f^A(x,y,z)=x+y+z teda napr ((2,3,4),9)∈f lebo ((x,y,z),x+y+z)
ak ale B={0,1,2}⊆N zostanu iba take prvky ktore x,y,z∈B alebo r=x+y+z∈B teda (0,1,1) so sumou 2 zostane v B ale (2,2,2) nezostane lebo 6 je mimo B teda preto ze ste busime urobit restrikciu aby sme nechali funkciu ktora je plne definovana, chceme aby aj inputy aj outputy patrili B
(P15) Definovatelnost ve struktuře.
A=(Z,<) pri φ(x,y):=x<y nam da φ^A={(a,b)∈Z^2 ∣ a<b} teda nejake usporiadane dvojice
b je len parameter ktory nam specifikuje vlastnost, ak by sme mali b=3 tak mame φ^(A,b=3)(x) = {a∈Z∣a<3} teda ista podmnozina Z {2, 1, 0, -1 ...}. Uz to nie su usporiadane dvojice pretoze b je parameter a jedina volna premenna je uz len x.
(P16) Extenze o definice.
- specialny druh konzExt - vieme pekne pinpointnut nejaky fakt napr ked chceme iba parne cisla tak rozsirime jazyk a teoriu o prave tento poznatok. Vsetko co v tej teorii bolo tak tam aj zostane a vsetko co sa dalo odvodit sa dalej bude dat odvodit.
- Rozsirujeme klasicky L aj T o funckne a relacne symboly, relacne to je jednoduche ale pri funkcnych musime zachovat vlastnost funkcie teda sa prida
axiom existencie: kazdy input ma aspon jeden output
axiom jednoznacnosti: output je unikatny pre kazdy input
(P17) Prenexní normální forma, Skolemova varianta.
- tu pozor na dvojindexovanie "ni" a priklad nejaky co tam ma v skriptach je postacujuci asi, toto ma clovek zo zapoctu celkom natrenovane.
- najprv vyjebeme existencny a potom az nahradime fx
(P18) Herbrandův model, srovnání s kanonickým modelem.
KanM: Vetva bezsporna a Tablo dokoncene (expandovane pre kazdy axiom), vieme kazdu premennu p ohodnotit 0/1 podla toho ci sa vyskytuje Fp or Tp
HerbM: cisto syntakticky napis bez semantiky, potrebuje aspon 1 const aby generoval cez funkcne symboly nekonecnu mnozinu symbolov, nekladie ziadne dorazy na Relaacne symboly
(P19) Izomorfismus struktur, ω-kategorická teorie.
0. ω-category je spocetne nekonecne
1. bij h:A->B, strAB, L=<R,F>, h(R&F)
- boolean algebra (strA,∧,v,-) ~= potencna algebra (P(X),∩,∪,\) kde strA= {0,1}^n
- izo cez char vektor po zlozkach union==or, complement==not, intersection==and
- h: P(X) -> {0,1}^n , A |-> χ_A Teda napr 011 zodpoveda mnozine {2,3}.
- izomorfizmus zachovava funkcie a relacie obv
2. I(k,T)=1 #M(T^k bez izo vcetne transf), ω 1sn model)
- Q na intervale [(0,1]) ma spocetne nekonecno prvkov, ale vieme spravit taky mapping, s DeLO, ze tam bude resp nebude max|min zahrnuty, teda mame 4 neizomorfne moznosti pre kazdy mozny interval (0,1), (0,1], [0,1), [0,1]. Ak by ale DeLO* nemalo endpointy tak by zjavne malo iba jeden interval a to (0,1) teda vtedy k=ω=1
- I(ω,DeLO)=4 no I(ω,DeLO∗)=1
(P20) Axiomatizovatelnost, konečná axiomatizovatelnost, otevřená axiomatizovatelnost.
trieda struktur K ⊆ M_L, skumame K pre 3pripady ^
AX: PeanoA alebo DELO bez max pointu - vzdy bude existovat successor
konAx: teoria group (3axiomy) alebo DeLO bez endpointov (5 asi)
openAx: K kde kazda struktura je bez kvantifikatorov
(P21) Rekurzivní axiomatizace, rekurzivní axiomatizovatelnost, rekurzivně spočetná kompletace.
1. ∃algo: φT or not
- tu peanoA nefunguje lebo nevieme rozhodnut ci je formula axiom kvoli induction scheme
- addition only aritmetika je ok
- DeLo bez endpointu tiez ok lebo su len 4axiomy ktore T definuju
2. K⊆ML rekAx <-> K=MLT or T' ekv rekAx)
- z godolovej vety prirodzene cisla N nejsu rekAx
- PeanoA je ok lebo successor, 0, add, multip su 4axiomy, pre induction schemu vieme algoritmicky vygenerovat pre kazdy prvok aj ked je ich nekonecno lebo tolkokrat zobereme successora. Ale "This sentence is not provable in PA." sa ojebava na N
- telesa char 0 su ok lebo vieme opat doradu rekurzivne vygenerovat ake to su aj ked je nekonecno prvocisel
3. az na ekv konjedExt T je rekSpoc resp. ∃algo: (i,j) -> (axiom,ext) (alebo axiom uz neexistuje ak j<i)
(P22) Rozhodnutelná a částečně rozhodnutelná teorie. (∃algo: ∀inp φ) (dobehne a rozhodne T|=φ)(T|=φ dob+ano, T|/=φ nedob|dob+ne)
-hocijaka picovina z cviku je rozhodnutelna
- PeanA je iba ciastocne lebo godolova veta
===============================================
(L1) Množinu modelů nad konečným jazykem lze axiomatizovat výrokem v CNF, výrokem v DNF.
0. ak je mnozina modelov konecna v konecnom jazyku, vie byt axiomatizovana(vyjadrena) v CNF. Medzi CNF a DNF existuje prevod teda vie byt vyjadrena aj v DNF.
1. CNF zakazuje jeden nemodel (SAT solver), DNF jeden model popisuje - CNF je dual DNF lebo modely maju rovnake.
(L2) 2-SAT, Algoritmus implikačního grafu, jeho korektnost.
0. k-cnf & k-sat
1. Kazdu 2-C vieme napisat vo forme implikacii,
jednotkova: l ako [l'->l]
zvysok: l1 or l2 ako [l1' -> l2 and l2' -> l1]
2. urobime graf kde hrany su vsetky implikacie ktore vznikli medzi literalmi a vrcholy vsetky mozne literaly
3. Strongly connected component O(n) - musia byt literaly ohodnotene rovnako vramci komponenty inak to je spor lebo by sme mali 1->0. Ak je vsetko ok tak cykly skontrahujeme
4. Mame nutne Directed Acyclic Graph (DAG), pretoze vsetky cykly boli len v komponentach. DAG vieme prejst topologicky - podla nejakeho pravidla - topologicky sort.
5. Preto vsetky vrcholy do ktorych nevedie hrana (zaciatocne) nastavime na 0 opacnu komponentu nutne teda na 1. Treba poznamenat, ze 1 je vynuteny krok, vo vseobecnosti implikacia neplati iba ak 1->0 teda v nas prospech je mat predpoklad 0 a zaver tiez 0. Nastavovanim veci na 1 by sme dosli do sporu ktory nemusi nutne existovat.
6. treba ukazat scc nema l'l <=> vyrok φ je splnitelny:
=> tym ze komponenta je cyklus tak vsetko musi byt ohodnotene rovnako lebo by sme dospeli k tomu, ze bud 0->1 alebo 1->0 kde druha moznost je fatalna
<= vid vyssie ^
7. toposort je v O(m+n) teda cele to ide linearne
(L3) Horn-SAT, Algoritmus jednotkové propagace, jeho korektnost.
0. mame C napisanu vo forme implikaci s vela predpokladmi a jednym zaverom teda to je ekvivalentne napisane -a, -b, -c ... x kde x je uz pozitivne
1. mame vstup takuto S skladajucu sa z horn C a po dobehnuti informujeme ci to je splnitelne pre dany vyrok alebo ne. Su 3 pripady co mohl inastat:
- exit1.1: mame hned spor vramci S lebo mame 2 rozne C kde jedna ma prave l a druha presny opak (l') a CNF toho bude teda nesplnitelna (mozeme sa pojebat)
- exit1.2: mame nejake C kde v ziadnej nieje vynuteny tah (kazda C ma aspon 2 lit), vtedy si spomeneme ze C je disjunkce literalov a kedze je tam aspon jeden nepravdivy, nastavime ho na 0 v kazdej C a teda sme splnili φ
- iter1.3: urobime jednotkovu propagaciu, z φ sa stane φ^l a redukujeme ten isty problem v mensom
2. v konecnom case skoncime lebo nemame sa kde zacyklit (iter a 2 exit vetvy pokryvaju vsetky mozne stavy kam sa mozeme dostat, kedze mame konecny pocet klauzuli a iter funguje, nic nevznika je to spojita funkcia klesajuca)
(L4) Vlastnosti extenze o definice.
1. ∀L': ∃L: T'|= φ'<->φ (Toto mi povedal sam bulin)
mame funkciu v kode a chceme sa jej zbavit, musime vsetky jej vyskyty nahradit priamo kodom ktory zastresovala ale je treba este premenovat premenne pretoze global and local name sa moze zhodovat.
2. (M(T) exp M(T') &
3. T' konzext T
zjavne ano kedze extenze o definici len pridava pointer na nejaku konkretnu vlastnost teorie (parne cisla napr). Pridame to aj do relacnych a funkcnych symbolov ale neposkodzuje to modely nakolko s tym nic nove dosiahnut nevieme
(L5) Vztah definovatelných množin a automorfismů. (h ∈ Aut(strA), a ∈ D ⇔ A |= φ[e(x/a, y/b)])
hocijaky mapping to nevie pokazit
racionalne cisla and x |-> y^2 and inverse still holds
graf sa mapuje vzdy sam seba a mozno na nieco ine, podla deg(v) a hran...
(K4 bez jednej hrany) je dobry priklad
? (L6) Tablo metoda v jazyce s rovností.
vzdy ked je L= tak sa tam pridaju axiomy rovnosti. Je to nieco celkom ine ako faktorizacia proste len sa povie ze ked a=b tak v reci modelov vieme riesit iba jednu premennu ale v dokazoch nie.
(L7) Věta o kompaktnosti a její aplikace. M(T)<=>M(∀kon cast)
=> zjavne
<= Sporom T |− ⊥ kedze Tnema model. τdukaz ma kon vela ax T, M(T′⊆T) = {}
app: nestandardny model N, pomaly vsetko dopice, telesa char0 aj tie tazke vety vsetky ju vyuzivali
(L8) Věta o korektnosti rezoluce ve výrokové logice.
zamit->nespln, spor: C0..Cn splnitelna, induktivne case1/2 (rezolucne pravidlo P9)
basecase 1: ¬R,¬R => □ (spor teda plati)
induction case 2: (Q∨R),(¬Q∨¬R) => (¬R∨R)
(L9) Věta o korektnosti rezoluce v predikátové logice.
1. CNF S zamit->nespln, sporom: ak model A|=S - ind A|=□ to je spor (same shit ako L8 len tam riesime navyse ohodnotenia a struktury)
2. lemma (indukcny krok): rezolucne pravidlo P9
(L10) Souvislost stromu dosazení a splnitelnosti CNF formule. (S je nesp <=> ∀vetev ma empty C)
lemma:
-1. rezolucia je len specialny pripad tejto mrdky stromovej lebo sa bavime v nekonecne ale pouzivame kompaktnost a pri konecnom mnozstve C vieme trivialne spravit bruteforce s rezoluciou
0. predpokladame V|=S a kedze S sa sklada z C1C2... tak nutne aj kazda C bude musiet byt splnena aby CNF reprezentacia klauzul bola splnena.
0. BUNO lebo sa analogicky da dokazovat l ako l', len pre prehladnost teda
lemma =>
1. ak vyjebeme l z kazdej C nutne zvysok Clauses (moze ich byt menej, ale nutne aspon jedna ma o 1 prvok menej) v S^l bude S splnovat, moze sa stat, ze S bude empty ale to trivialne splnuje lebo CNF je true ked je empty (zakazuje jeden nemodel, ziadny nemodel tam neni takze plati)
lemma <=
toto mi pride super zjavne a intuitivne, proste ked mame nejaky stav tak pridanim noveho l veci nepokazime lebo S^l ho proste nemalo. To l naozaj nemusi pomoct splnit nejaku C ale zjavne teda konecne vela krat to urobime a hotovo
dokaz:
1. indukce |VarS| (vieme ju robit aj z predu aj zozadu)
base: |VarS|=0 yields S={} alebo S={nespln}
step: lemma[S spl <=> S^l or S^l']
2. S je
nekonecna splnitelna - nekonecna vetva v strome dosazeni
nekonecna nesplnitelna - kompaktnost nam najde tu konecnu cast a opakovanim lemmy bude na kazdej vetve eventualne {nespln}
(L11) Nestandardní model přirozených čísel.
0. definuje sa successor a nejaka const c ktora bude v novej teorii navyse T = Th(N) ∪ {n < c | n ∈ N}
1. kompaktnost nam dovoli napchat c niekde do kazdeho konecneho modelu s n prvkami a vzniknu c, c+1 c+2... navyse nestandardne prvky
(L12) Existence spočetného algebraicky uzavřeného tělesa.
0. C same o sebe je alg uzavrete ale nespocetne.
1. alg uzavretost cez vyrok ktory tam zajebe \forall a spravi to sentence pre kazdy polynom stupna n>0.
2. spocetnost cez dosledok LSd1 vety kde: kazda bezsporna nekonecna LTeoria ma spocetne nekonecny model
(L13) Tělesa charakteristiky 0 nejsou konečně axiomatizovatelná.
1. K\ budu netelesa a telesa char !=0, ak teda K je char0 a char p -- nic ine nevie byt
2. pre spor zajebeme ze K\ je axiomatizovatelne, aj ked veta 9.4.6 robi ekvivalenciu K!konAx <=> K ani K\ neni ax.
3. bude teda muset existovat model nejakej teorie S: M(S) = K\ a zaroven platit kompaktnost teda S' = SuT' pre nejake K popisujuce T' (T' == konAx teles char 0)
4. kompaktnost vygeneruje aj teleso char p vacsie nez hocijake p \in T' tvaru -p1=0 (existuje take lebo je nekonecne prvocisel dopice)
5. Tym ze ale kompaktnost zajebala model (strukturu A) [kompaktnutej] teorie S' tak A uspokojuje axiomaticky T' aj S ale M(T')=K a M(S)=K teda mame spor kedze nemozeme mat aj char p aj char 0
(L14) Kritérium otevřené axiomatizovatelnosti. (Ak T otvAx -> ∀pods M(T) je M(T))
0. otvorena T' hovori ze sa pozerame na veci iba lokalne, medzi premennymi. Nemame kavitfikatory takze sa nemozeme pozriet na prvky mimo struktury (skolemizacia nefunguje napr). Preto teda len dokazujeme, ze trieda struktur je uzavreta na heredity property
1. vyrobime T' co je otvorene ax z predpokladu
2. A|=T' z predpokladu & strB⊆strA z definicie
3. ∀φ \in T': strB|=φ (predpoklad T'), teda aj B|=T'
- ciastocne usporiadanie - ref(prvok sam na sebe plati) aj antisymetria + trans plati na existujucich relaciach v strukturach, vieme vybrat len nejake prvky a stale sa pytat ci su ciastocne usporiadane
(L15) Rekurzivně axiomatizovaná teorie je částečně rozhodnutelná, kompletní je rozhodnutelná.
sysT Fφ ak plati - skonci
T kompletna: T|-φ or T|/-φ, 2tab paralelne Fphi Tphi, jedno skonci
(L16) Teorie konečné struktury v konečném jazyce s rovností je rozhodnutelná.
0. rozhodnutelna = Recursively axiomatizable
0. ocislujeme si prvky nech sa nam dobre ukazuje prstom
1. spravime "hash" struktury v danom case (vyslovime vetu (odfotime si kokotiny co obsahuje)) ktora enumeruje prvky [a1..an] aj relacie aj funkcie a vieme ake sentence do THM(A) patria a ake nie.
2. vieme robit queries - dokonca v O(1) lebo sa fotka nikdy nemeni a mame to nacacheovane
3. zapis vo first order logic je trochu iny: (a3,a3,a1)∈/R^A == ¬R(xa3,xa3,xa1) ako aj f(a4,a2)=a17 == f(xa4,xa2)=xa17
(L17) Gödelovy věty o neúplnosti a jejich důsledky (bez důkazů).
1. ∀bezspornu rekAxExtT RobA: ∃sent pravdN ale nedokT
https://youtu.be/zNAvtgBDv8w
https://youtu.be/O4ndIDcDSGc
- vieme zakodovat kazdy existujuci symbol do prvocisiel teda aj napr fermatovu malu vetu vieme zapisat ako unique number ktore sa da dekodovat, nieco ako ascii
- a referencovat sameho seba - "toto tvrdenie nevie byt dokazatelne z axiomov" - paradox je to pravdive ale nevieme to dokazat. Self referencing sa vie rekurzivne mnozit nelinearnej rychlo pretoze vieme robit narny strom v podstate
2. Ak T splnuje predoklad 1GV o neuplnosti a N je modelom T: T neni kompletna:
sporom zistime ze neplati kompletnost a uplnost naraz
3. veta o pevnom bode (T ext RA: kazda formula ma sentence T |- phi(xi) <-> xi)
self-referencing a godolova veta a nerozhodnutelnost v kodovani sameh oseba
4. neexistuje definicia pravdy v ziadnej RA ktore je bezsporne
"nie som pravdivy statement v T"
5. Ak T rekAx RA + N = M(T) => T != kompletna
model robi nespornost teda splnuje predpoklad 1GV a teda neni dokazatelna GV
ak by bola kompletna musela by dokzavoat GV ale to je spor dopice neviem uz sa mi to nechce
6. Th(N) != rekAx
zas to godolova veta kazi pretoze rekAx pre spor + complete => rozhodnutelna Ale to je v spore s godolovou vetou
7. GV2: ∀bezspornu rekAx ExT PeaA: Con_T=bezspornost neni dokazatelna v T
8. Dosledok GV2: v PA ma 0 successor 0 existuje toho dokaz
svedok neni hodnota ziadneho numeralu
9. existuje bezsporna rekAx ExT PeaA: dokazuje svoju spornost v T
10. ZFC v teorii mnozin je to iste ako PA v teorii cisel
===============================================
(T1) Věta o korektnosti tablo metody ve výrokové logice. (shoda M(T) root -> shoda Vi)(τ + ind_i V0⊆..⊆Vn)(V [predlz, Tatomic τ, Taxiom])
0. T⊢φ => M(T)⊆M(φ) -- robime to sporom teda predpokladame ze φ je false resp teda ze model neexistuje lebo je sporna T
1. tympadom sme nuteny konstruovat sporne tablo lebo hned v koreni bude spor a nech opakujeme lemmu kolkokrat chceme, tak aj vetva zodpovedna za model bude sporna a teda model existovat nemoze - spor.
lemma: ukazujeme indukcny krok kde ukazujeme spravnost noveho tabla aj vetvy. Jedine 3pripady co mozu nastat su
1. predlzime vetvu (napr PorQ zmenime na dve vetvy s TP a TF)
2. True axiom - napiseme nieco s cim zaciname PorQ
3. atomicke tablo pre nejaku polozku - opat sa model zhoduje s polozkou, lebo aj s korenom a teda s nejakou vetvous
(T2) Věta o korektnosti tablo metody v predikátové logice. (shoda M(strA)T_L root -> strA expand Lc a shoda Vi)(τ + ind_i V0⊆..⊆Vn)(V [predlz, Tatomic τ, Taxiom], atomic[&||-><->][∀ term][∃ const])
0. same shit ako vyrokova, spor pretoze root ma Fφ v koreni takze kazda vetva bude sporna.
1. treba si dat pozor ze sa tu expanduje jazyk lebo mame funkcne symboly s konstantami.
lemma: opat sa pozerame na indukcny krok a v kazdom pripade sa predlzi tablo aj vetva a este aj struktura A, jazyk automaticky predpokladame ze sa rozsiri o vsetky a, f(a) ffa ...
1. predlzime vetvu
2. pripojime Taxiom
3. atomicke tablo, tu ale mozu nastat 3 dalsie veci:
- True vseobecny a True existencny kvantifikator ktory strA expanduje o novy konst/term. (False pre oba je len obdoba toho co sme definovali)
- Potom este to moze byt klasicka logicka spojka tak ako vo vyrokovej ale tu nepridavame novy symbol do strA lebo nie sme schopny generovat nove symboly
(T3) Věta o úplnosti tablo metody ve výrokové logice. (sporom - sysτ Fφ root neni sporne - kanM, lemma ∀Tax: v|=T, root: v|=/T) (Tφ v(p)=1, Fφ =0, ind Tφ&xi v|= , ind Fφ&xi v|/=)
lemma: kanM sa shoduje s dokoncenou bezspornou vetvou
ind base: Tp bude mat v(p)=1 v modeli a Fp zas 0
ind step: rozjebavaju sa logicke spojky podla predpisov na uz zname fakty z ind base, teda konjunkcia na Tp1 Tp2 v jednej vetve, resp na Fp1 a v sdruhej vetve Fp2... analogicky vsetky.
(staci popisat negaciu konjunkciu a disjunkciu nakolko vsetko ide vyjadrit v nich, teda implikacia a ekvivalencia je len obmena tvrdenia)
veta: sporom, dokoncene systematicke tablo s Fφ v roote je predpoklad. Mali by sme mat spornu vetvu ale kedze ideme sporom, majme ju nespornu, ukazeme ze to je nerealizovatelne.
0. kedze je bezsporna urcite ma model, bud plati jedno alebo druhe.
1. mat model znamena ze nenastal ziadny spor a vetva sa zhoduje so vsetkymi polozkami po ceste k rootu - splnuje vsetky axiomy.
2. zas mame ale ten isty problem co vsade a to je ze root ma Fφ, do roota ide kazda cesta a teda nutne to ten model pokazi v jednom konkretnom axiome z ktoreho vystartujeme a teda nastane spor pre aspon jednu premennu a sporna vetva nema model.
3. tym ze sme uvazovali kanonicky model, hovorime ze sme presli vsetky polozky a urcite nic sme nenechali nahode.
(T4) Věta o úplnosti tablo metody v predikátové logice. (strA model, redukt A' skolm)(l: ind spojky atomic Ta T∀ T∃)
lemma: cele co tu je navyse je:
- Riesime navyse strukturu A co reprezentuje model, ma to trochu inu notaciu
- Vsetky polozky co tu figuruju su vo finale iba relacne symboly (vnutri relacnych su termy na ktore vedia byt aplikovane funkcne)
- kvantifikatory - bud term alebo const podla pravidiel.
- L= alebo bez= - pri= treba robit faktorstrukturu B.
-- Ak by sme mali P,Q,R ale P=Q tak nemame 2^3=8 moznosti ale iba 2^4 lebo napr Q v dejste vobec nebude figurovat, nakolko su zgroupnute v jo faktorstrukture s iba 2prvkami.
-- Ak by sme mali teleso Zp tak vieme modulovat p a teda nutne bude iba p "skatuliek"vo faktorstrukture B, nakolko ziaden z inych pripadov nastat nemoze
Inak herbrandov model je cisto syntakticka zalezitost bez semantiky (neinterpretuju sa logicke suvislosti typu =), tu robime kanonicky teda L= urcite treba zohladnovat
veta: znovu riesime navyse to iste, znovu sporom, iba strA a jazyk navyse:
- uvazujeme A' aj redukt na L pretoze zjavne pri aplikovani funkcnych symbolov na konstanty vznikla nekonecna domena (a, f(a), ff(a)...) a teda to bolo pomocne pri konstrukcii tabla ale pri modelu vetvy nas to uz nezaujima, preto sa redukujeme na povodny jazyk.
(T5) Věta o konečnosti sporu, důsledky o konečnosti a systematičnosti důkazů.
Ak τ zjednotenie vsetkych tabel τ_i je sporne => ∃n ktore τ ohranicuje na konecne sporne
1. Nech S je najvacsia taka mnozina neobsahujucu spor a siaha do hlbky d
2. ak by bola taka mnozina nekonecna - aplikujeme koniggerovo lemma na podstrom v S dostaneme nekonecnu bezspornu vetvu ale to je spor s predpokaldom ze mame sporne tablo
3. to znamena ze v hlbke d+1 stupime do hovna a mame splneny zaver aj predpoklad
Dusledek1: Ak nepredlzujeme spornu V => τ dokaz je konecny
Dusledek3 (systematickost dukazu): Ak T|−φ => sysT je konecnym τ dukazem φ z T
korektnost & uplnost
Dusledek2 (konecnost dukazu): T|−φ => ∃konecny τ dukaz φ z T
Dusledek1 - nepredlzujeme spornu vetvu dopice
(T6) Věta o úplnosti rezoluce ve výrokové logice.
lemma vid L10
veta S nespln -> zamit:
0. urobime si S konecnu cez kompaktnost
1. ind |var(S)| od dola kedy |Var(S)|=0 a aplikujeme lemma ako indukcny krok.
1.1. Pre kazde aplikovanie lemmy vybudujeme strom, T pre (S^p |- □) aj T' pre p'. Lemma hovori ze urcite ma S o premennu menej
2. zo stromu T vygenerujeme rezolucny megastrom T* (S |- -p) obdobne pre T' megastrom T'* a pripojime ich na □ aby sme v poslednom kroku rezolucie ziskali p a -p a tym dostali □.
3. T* konstrukcia: induktivne bottom-up propagaciou p a -p aby sa rezolvli a spravili novy koren s □. musi sa propagovat p aj -p pripisat do kazdeho vrcholu pozdlz cesty
(T7) Věta o úplnosti rezoluce v predikátové logice
Lifting lemma:
0. nezavisle C1 a C2 => groundneme na C1*C2*
1. Ak je C* rezolventou tak aj C je rezolventou povodnych C1 a C2
veta CNF S nespln -> zamit:
0. S je nesplnitelna tak aj S* nespln (T9 - Herbrandova veta)
1. tym ze riesime S* tak sme cisto vo vyrokovej logike a vyuzijeme dokaz z T6^^ dospejeme k S*|−□
2. Lifting Lemma nam dovoli sa vratit do predikatovej tym, ze zobrieme substituciu Cσ=□ a dostaneme S|−C.
3. tym ze substitucia nam iba nahradza premenne za ine termy, nutne musela byt C prazdna predtym a teda C=□ dokazuje zamitnuti S|-□
(T8) Skolemova věta. ∀T:otvKonzExt
1. PNF T'
2. Skolem T'' L'
3. lemma T''L' je ext T'L resp redukt => T'' konzExt T
4. T'' je ax iba "∀" (lebo skolemizacia) teda ked zobereme otvorene jadro => T''' je otvorena T''
5. T''' je ekv s T'' ale ta je konzExt T, teda tranzitivne T''' je otvorena konzExt T
(T9) Herbrandova věta. T Lbez= 1const -> HerbM(T) or !CNF axT
0.0 aspon 1const generuje cez funkcny symbol {a, f(a), f(f(a))...}
0.1 T_ground su prave tieto premenne, je ich nekonecne vela - neskor pouzijeme kompaktnost
0.2 zapodievame sa iba syntaktickym napisom teda = nema ziadny ucel
0.3 sys tablo s F⊥ v roote (lebo je najmenej chaoticke, no rovnako dobre ako hocijake ine tablo)
1 bezohladu na to ako konstrukcia tabla vyjde, redukujeme iba na L bez const, pretoze ich nepotrebujeme, vieme najst tie axiomy ktore su zodpovedne za dany vysledok
2 sysTablo nam bud da:
2.1 (kanonicky)model a teda je to Herbrandov model v T (cisto syntax bez semantiky, checks out s L bez =)
2.2 spornu vetvu a teda T_ground aj T je nesplnitelna. Spor vznikol v konecnom case s konecnym poctom axiomov - kompaktnost. Ak je aspon jeden axiom nepravdivy tak CNF sa nesplni
(T10) Löwenheim-Skolemova věta včetně varianty s rovností, jejich důsledky.
LS spocetny Lbez= -> ∀bezS TL ma snm
sysT F⊥, bezsporne tablo => bezsporna vetva, snm je Lred kanM
- mame slovnik a tym nevieme vyjadrit nekonecny svet
- nevieme popisat nespocetne nekonecno pri realnych cislach lebo mame len spocetny jazyk
LSd1: SpocL= -> ∀ nekonecnej Lstr ∃eesns
existuje tam A, spravime deepcopy nazveme B a plati ze nejsu izo ale popisuju tu istu vec. Navyse do B mozeme podla stanovenych pravidiel Th(A) zajebat este dalsie properties
LS spocetny L= -> ∀bezS TL ma spocetny model (konecny alebo spocetne nekonecny)
-faktorizujeme podla =A, v podstate tym ze mame rovnost a nieco sa navzajom rovna tak to bude stale ukazovat na nejaky jeden objekt danej classy
LSd2: SpocL= -> ∀ nekonecnej Lstr ∃eesns
vieme pre kazde n povedat vetu "for all n, there exist at least n elements" v strA a teda kedze strB je len deepcopy + ma nieco mozno navyse, nebude zjavne popisovat nieco menej ako A. Je to odolne aj voci faktorizacii lebo kazda veta je unique id a popisuje unique element.
Lsd3: ∃spoc alg uzv T
(T11) Vztah izomorfismu a elementární ekvivalence. (A≃B => A≡B ale nie naopak lebo DeLO* nevie spravit bijekciu na R ale na Q ano)
dokaz mam v pici kys
(T12) ω-kategorické kritérium kompletnosti. ωT spocetny L. (Lbez=) or (L= & T nema kon m) => Tkompl
- LSd1 bez=: ∀model prave1 eesnm+izo = kompletnost
- LSd2=: ∀nekM = ee
(T13) Neaxiomatizovatelnost konečných modelů.
T ma konM => aspon 1 nekonM (S = konM neni ax.)
- Lbez= -> kanM pre nejaku bezpornu vetvu s F⊥ v roote (ma model == neni sporne)
- L= ->
T' extended T o {¬ci = cj | i!=j \in N} spocetne vela const
kazda konecna cast T' ma model (tak ako T): najdi max k take ze c_k \in T'
k+1 prvkovy model T + interpretovat ci-1 != ci
kompaktnost == T' ma nekonecny model.
Redukt na L je nekonecny model T
(T14) Věta o konečné axiomatizovatelnosti. (K⊆ML: K konAx <=> K&K' Ax)
=>: konAx == K ax sentces phi1..n K\ xi=~(phi1..n) (M(xi)=K')
<=: zjednotenie a prienik M(T) a M(S) je emptyset lebo su navzajom komplementy.
nulovy prienik aj po kompaktnosti, M(T)⊆M(T') lebo sme si to len zkonecnili
M(S') komplement je M(T'), teda M(T)=M(T')
(T15) Rekurzivně axiomatizovaná teorie s rekurzivně spočetnou kompletací je rozhodnutelná.
0. bud T|-φ alebo sa to pre nejaku kompJedExt Ti dojebe a bude platit opak teda Ti|- ~φ (konkretne strA |=/φ)
1. paralelne teda tablodokaz pre kazdu kompJedExt T_123... ale aj Tφ
2. jedno z tabel je sporne a ked nepredlzujeme spor tak mame konecny dokaz (pouzijeme dovetailing ~BFS lebo tablo je nekonecny ale konecne vetviaci strom pojebany)
