taky skuskovy priklad

Dolda · Příspěvek 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

]

Dawe · Příspěvek 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š.

Dolda · Příspěvek 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)))

Cermm · Příspěvek 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

dr.Bik · Příspěvek 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)

twoflower · Příspěvek 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)?

laliebijard · Příspěvek 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.

twoflower · Příspěvek 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)

qwyxyo · Příspěvek 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

twoflower · Příspěvek 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?

qwyxyo · Příspěvek 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...

laliebijard · Příspěvek 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

twoflower · Příspěvek od **twoflower** » 18. 6. 2006 23:34

Ahaa, diky, uz to chapu