Fórum studentů MFF UK

od **twoflower** » 18. 6. 2006 23:34

Ahaa, diky, uz to chapu

od **laliebijard** » 18. 6. 2006 23:28

twoflower píše: Pravidlo generalizace tvrdi, ze z B odvodim (Vx) B pro libovolnou promennou z B, tak proc by to neslo?

Ze z niecoho nieco odvodis znamena
|-B => |-(Vx)B

co nie je to iste ako
|-B -> (Vx)B

To prve znamena, ze ak je dokazatalne B, tak potom je dokazatelne (Vx)B (toto je pravidlo generalizacie)

To druhe je, ze je dokazatelne: z B vyplyva (Vx)B

od **qwyxyo** » 18. 6. 2006 23:15

twoflower píše:
qwyxyo píše:
B --> (Vx) B (pravidlo generalizace)
No ja v tomto ziadne pravidlo generalizace nevidim. Toto sa da nazvat iba ako zavedenie obecneho kvantifikatoru, co je vlastne spojenie pravidla generalizace s pravidlom preskoku, ale aj to za predpokladu ze B neobsahuje volne x, co zjavne neplati.
Prve dva riadky mas dobre. Ked tie implikacie zlozis a zavedies vyssie zmienene obecne kvatifikatory tak to mas hotove...

Tz. zavedenie V nejde nahradit pravidlem generalizace, lebo zavedenie V = generalizace + preskok
Pravidlo generalizace tvrdi, ze z B odvodim (Vx) B pro libovolnou promennou z B, tak proc by to neslo?

Tak to si trosku zle pochopil. To odvodenie neznamena implikacia B -> (Vx)B. Nemozes si len tak zobrat nejaku cast formule a zaviest si tam kvantifikator. Zober si za B: x<10 v realizacii prirodzenych cisel. B->B plati ale B->(Vx)B zrejme nie. Alebo ano?

Naopak, ak pouzijes pravidlo generalizace, tak vznikne formula (Vx)(B->B). co zrejme plati, ak sa nemylim...

od **twoflower** » 18. 6. 2006 22:51

qwyxyo píše:
B --> (Vx) B (pravidlo generalizace)
No ja v tomto ziadne pravidlo generalizace nevidim. Toto sa da nazvat iba ako zavedenie obecneho kvantifikatoru, co je vlastne spojenie pravidla generalizace s pravidlom preskoku, ale aj to za predpokladu ze B neobsahuje volne x, co zjavne neplati.
Prve dva riadky mas dobre. Ked tie implikacie zlozis a zavedies vyssie zmienene obecne kvatifikatory tak to mas hotove...

Tz. zavedenie V nejde nahradit pravidlem generalizace, lebo zavedenie V = generalizace + preskok

Pravidlo generalizace tvrdi, ze z B odvodim (Vx) B pro libovolnou promennou z B, tak proc by to neslo?

od **qwyxyo** » 18. 6. 2006 22:21

B --> (Vx) B (pravidlo generalizace)

No ja v tomto ziadne pravidlo generalizace nevidim. Toto sa da nazvat iba ako zavedenie obecneho kvantifikatoru, co je vlastne spojenie pravidla generalizace s pravidlom preskoku, ale aj to za predpokladu ze B neobsahuje volne x, co zjavne neplati.
Prve dva riadky mas dobre. Ked tie implikacie zlozis a zavedies vyssie zmienene obecne kvatifikatory tak to mas hotove...

Tz. zavedenie V nejde nahradit pravidlem generalizace, lebo zavedenie V = generalizace + preskok

od **twoflower** » 18. 6. 2006 21:48

laliebijard píše:
twoflower píše: Slo by nahradit pravidlo zavedeni V pravidlem generalizace (taktez dvakrat pouzitym)?
Myslis v tom tretom riadku? No to by si dostal V pred celu formulu.

Ne, myslel jsem to takhle:

Kód: Vybrat vše

(Vx)(Vy) B --> (Vy) B       (schema specifikace)
(Vy) B     -->  B           (schema specifikace)
 B         --> (Vx) B       (pravidlo generalizace)
(Vx) B     --> (Vy)(Vx) B   (pravidlo generalizace)
(Vx)(Vy) B --> (Vy)(Vx) B   (slozeni implikaci)

od **laliebijard** » 18. 6. 2006 18:57

twoflower píše: Slo by nahradit pravidlo zavedeni V pravidlem generalizace (taktez dvakrat pouzitym)?

Myslis v tom tretom riadku? No to by si dostal V pred celu formulu.

od **twoflower** » 18. 6. 2006 18:49

laliebijard píše:Ja som to robil takto:

Kód: Vybrat vše

|-(Vx)A -> Ax[x]             (axiom specifikacie)
|-(Vy)(Vx)A -> (Vx)Ay[y] (=(Vx)A)      (axiom specifikacie)
|-(Vy)(Vx)A -> A          (zlozenie implikacii)
|-(Vy)(Vx)A -> (Vx)(Vy)A         (dva krat pravidlo zavedenia V)

co myslite?

Slo by nahradit pravidlo zavedeni V pravidlem generalizace (taktez dvakrat pouzitym)?

od **dr.Bik** » 16. 6. 2006 10:09

Dawe píše: Takže asi takhle:

Kód: Vybrat vše

(A & B)->C 
nonC -> non(A & B) (V5)
nonC -> (nonA v nonB) 
nonC -> (nonnonA -> nonB) (V3)
nonC -> (A -> nonB)

Dál 

(A->C) -> ((B->C) -> (nonC -> (A->nonB)))
(A->C) -> ((nonC->nonB) -> (nonC -> (A->nonB))) (V5)
(A->C) |- ((nonC->nonB) -> (nonC -> (A->nonB))) (VD)
(A->C),(nonC->nonB) |- (nonC -> (A->nonB)) (VD)
(A->C),(nonC->nonB),nonC |- (A->nonB) (VD)
(A->C),(nonC->nonB),nonC,A |- nonB (VD)
pomocí nonC a nonC->nonB přes MP |-nonB

Proc tak slozite?

Nejde proste

Kód: Vybrat vše

(A & B) |- A (LEMMA)
A, A->C |- C (MP)
A->C, B->C, (A & B) |- C (pridam si B->C, to nemuze nikomu ublizit)
|- (A->C)->((B->C)->((A & B)->C))) (3xVOD)

od **Cermm** » 15. 6. 2006 22:28

Podla mna to bude ta prva varianta, kde sa premenne viazane E neberu do uvahy:

Kód: Vybrat vše

Toto
Vx Vy Ez Es Vr (p(z).. p(s))

sa prevedie  na:
Vx Vy Vr (p(f(x,y)).. p(g(x,y))

! tie E kvantifikatory sa uz v upravenej forme nevyskytuju

od **Dolda** » 15. 6. 2006 21:54

Dolda píše:Nám Vomlelová říkala, že počet parametrů funkce (která nahrazuje danou proměnnou) je počet kvantifikátorů před tím existenčním.
Kód: Vybrat vše
Příklad:
Vx Vy Ez Vr (p(z)...

převedeme na
Vx Vy Ez Vr (p(f(x,y))...
Což je taky odpověď na otázku argumentů - funkci zavádim úplně novou, ale argumenty dostane všechny ty, který stojí před existenčním kvantifikátorem, kterej převádim.

Doufam že to je srozumitelný a správný, kdyžtak mojí vizi někdo opravte [pokud možno do zítřka ]

Doufal jsem že to někoho bude trápit a napadne to, ale očividně ne, tak se zeptám sám:
Ta moje vize jak to má (podle Vomlelový) fungovat má menší nejasnost: Co udělat, kdy jsou 2 Existenční kvantifikátory po sobě? Neboli:

Kód: Vybrat vše

Tohle:
Vx Vy Ez Es Vr (p(z).. p(s)

se má převýst na:
Vx Vy Ez Es Vr (p(f(x,y)).. p(g(x,y))

nebo na:
Vx Vy Ez Es Vr (p(f(x,y)).. p(g(x,y,f(x,y)))

od **Dawe** » 15. 6. 2006 20:32

Tuetschek píše:
Koukam ze jsem poradne nepochopil podstatu dukazu ... to znamena ze kdyz zacnes u ty formule a dojdes k necemu, co uz je zrejmy tak mas dukaz? Ja se pokousel od instance nejakyho axiomu nebo neceho co plati dojit k ty formuli ... neslo .

No já to pochopil stejně, ale když jsem projížděl slidy, tak tam to má taky několikrát timhle směrem, na druhou stranu, ty operace mají svůj inverz a tak se to vždy dá obrátit a dojít tam kam potřebuješ.

od **Dolda** » 15. 6. 2006 20:08

Nám Vomlelová říkala, že počet parametrů funkce (která nahrazuje danou proměnnou) je počet kvantifikátorů před tím existenčním.

Kód: Vybrat vše

Příklad:
Vx Vy Ez Vr (p(z)...

převedeme na
Vx Vy Ez Vr (p(f(x,y))...

Což je taky odpověď na otázku argumentů - funkci zavádim úplně novou, ale argumenty dostane všechny ty, který stojí před existenčním kvantifikátorem, kterej převádim.

Doufam že to je srozumitelný a správný, kdyžtak mojí vizi někdo opravte [pokud možno do zítřka

]

od **laliebijard** » 15. 6. 2006 20:00

Ja by som tam napisal f(x1,...,xn) atd a k tomu, ze n je pocet volnych premennych v danej formuli.

od **Tuetschek** » 15. 6. 2006 19:08

Diky obema

Koukam ze jsem poradne nepochopil podstatu dukazu ... to znamena ze kdyz zacnes u ty formule a dojdes k necemu, co uz je zrejmy tak mas dukaz? Ja se pokousel od instance nejakyho axiomu nebo neceho co plati dojit k ty formuli ... neslo

.

Takze ta Skolemova NF bude vypadat nejak takhle?

Kód: Vybrat vše

(Ey)B <-> ((Vy)B & (Vz) C )

prevod na prenexni formu (nektery mezikroky vynechavam, C_z[q] je substituce q za z v C apod.): 

((Ey) B -> ((Vy)B & (Vz) C)) & (((Vy)B & (Vz) C ) -> (Ey)B)
((Vy)(Vu)(Vz)( B -> (B_y[u] & C)) & ((Ep)(Ew)(Eq)((B_y[w] & C_z[q]) -> B_y[p]))

prenexni forma :

(Vy)(Vu)(Vz)(Ep)(Ew)(Eq) (( B -> (B_y[u] & C))((B_y[w] & C_z[q]) -> B_y[p]))

zavedu nove fcni symboly f, g, h, 
Skolemova NF: 

(Vy)(Vu)(Vz) (( B -> (B_y[u] & C))((B_y[f] & C_z[g]) -> B_y[h]))

A pro operandy tech fcnich symbolu plati nejake omezeni, nebo si muzu proste vzit nejake nove volne promenne?

Fórum studentů MFF UK

taky skuskovy priklad

Odeslat odpověď

Rozšířit náhled Přehled tématu: taky skuskovy priklad