Kód: Vybrat vše
Příklad:
Vx Vy Ez Vr (p(z)...
převedeme na
Vx Vy Ez Vr (p(f(x,y))...
Doufam že to je srozumitelný a správný, kdyžtak mojí vizi někdo opravte [pokud možno do zítřka ]
Kód: Vybrat vše
Příklad:
Vx Vy Ez Vr (p(z)...
převedeme na
Vx Vy Ez Vr (p(f(x,y))...
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š.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 .
Doufal jsem že to někoho bude trápit a napadne to, ale očividně ne, tak se zeptám sám: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.
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.Kód: Vybrat vše
Příklad: Vx Vy Ez Vr (p(z)... převedeme na Vx Vy Ez Vr (p(f(x,y))...
Doufam že to je srozumitelný a správný, kdyžtak mojí vizi někdo opravte [pokud možno do zítřka ]
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)))
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
Proc tak slozite?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
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)
Slo by nahradit pravidlo zavedeni V pravidlem generalizace (taktez dvakrat pouzitym)?laliebijard píše:Ja som to robil takto:
co myslite?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)
Ne, myslel jsem to takhle:laliebijard píše:Myslis v tom tretom riadku? No to by si dostal V pred celu formulu.twoflower píše: Slo by nahradit pravidlo zavedeni V pravidlem generalizace (taktez dvakrat pouzitym)?
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)
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.B --> (Vx) B (pravidlo generalizace)
Pravidlo generalizace tvrdi, ze z B odvodim (Vx) B pro libovolnou promennou z B, tak proc by to neslo?qwyxyo píše: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.B --> (Vx) B (pravidlo generalizace)
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
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...twoflower píše:Pravidlo generalizace tvrdi, ze z B odvodim (Vx) B pro libovolnou promennou z B, tak proc by to neslo?qwyxyo píše: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.B --> (Vx) B (pravidlo generalizace)
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
Ze z niecoho nieco odvodis znamenatwoflower píše: Pravidlo generalizace tvrdi, ze z B odvodim (Vx) B pro libovolnou promennou z B, tak proc by to neslo?