taky skuskovy priklad

Mam problem s jednym skuskovym prikladom a neviem ci som ho dobre vyriesil.
Ak ma niekto vyhrady k mojmu rieseniu tak kludne piste:)

Zadanie: Dokazte: VyVxB <-> VxVyB

Riesenie:

Najprv pouzijeme vetu o konstantach a vsetky volne premenne v B nahradime konstantami c1..cn, a nech sa tato formula vola A
Podla vety o kostantach je B <-> A.

Zoberme si formulu VyVxA.
Nech n,m su premenne. Podla vety o variantach mozem zamenit viazane premenne v A (v B sme zamenili vsetky premenne konstantami)
Potom VyVxA <-> VnVmA[m,n] (x sme nahradili m a y n) podla vety o variantach
Dalej VnVmA[m,n] <-> (VnVmA[m,n])[x,y] (n nahradime x a m nahradime y)
cize (VnVmA[m,n])[x,y] <-> VxVyA tym je veta dokazana.

Ja som to robil takto:

|-(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?

laliebijard: jojo, napadlo me to samy... a nenapada me co tomu vytknout :twisted:

miso02: nevim jestli jsem to tvoje reseni pochopil spravne, ale neudelas nahodou toto:
VxVy(x<y) prevedes na VyVx(y<x) tedy na to same....?

Ano mas pravdu asi to bude tak..

laliebijard wrote:Ja som to robil takto:

|-(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?

Chvíli mi trvalo, než jsem se v tom zorientoval, ale ano, myslím, že je to dobře. Snad jen pro orientaci 1. a 2. formule nejsou ekvivalenty, ale 2 různé formule. Každopádně další rada jak napomoci překonat páteční písemku :-)

A nemate niekto navod na nieco taketo:
Dokazte Cons(Cons(T))=Cons(T).

Este by som sa chcel spytat na tuto ulohu. Ci je moj postup spravny. Ci som pouzil jednotlive vety korektne..

Zadanie: Dokazte: ( VxA V VxB ) -> Vx(A v B)

Riesenie? :
Pouzijeme vetu o konstantach a premenne vo formuly nahradime konstantami c1..cn
Potom ak dokazeme upravenu formulu tak plati aj ta povodna.

Dalej pouzijeme vetu o dokaze rozborom pripadov:
Najprv ukazeme VxA |- Vx(A v B) :
|-A -> (A v B) (monotoia disjunkcie)
|-VxA -> Vx(A v B) (distributivita kvantifikatorov)
VxA |- Vx(A v B) (VD)
podobne : VxB |- Vx(A v B)

Teraz podla vety o dokeze rozborom pripadov plati:
( VxA v VxB ) |- Vx(A v B)
|- ( VxA v VxB ) -> Vx(A v B) (VD)

A to by mal byt koniec..

To miso02: myslím, že by to mělo být korektní.

dik;)

Dan wrote:A nemate niekto navod na nieco taketo:
Dokazte Cons(Cons(T))=Cons(T).

Myslim, ze sa to da robit pomocou def. dokazu
"=>"
musis dokazat, ze pre vsetky A plati Cons(T)|-A => T|-A
Ak A0,...,An=A je dokaz formule A z predp. Cons(T)
potom pre kazde i Ai je bud axiom, to nam nevadi
alebo Ai patri do Cons(T), t.j. T|-Ai, v tom pripade Ai nahradime jej dokazom z T
alebo je odvodena pomocou modus ponens (predpokladame, ze z uz upravenych formuli)
no a mame dokaz formule A z T

a implikacia opacna je este jednoduchsia, lebo
Ai <- T, ale potom aj Ai <- Cons(T), lebo kazda formula z T patri do jej taut. dosledkov.
A mame dokaz Ai v Cons(T).

Teda, ja za spravnost nerucim, neviem, ci to je dobre...

Cau,
mohl byste se nekdo podivat na tyhle priklady a kdyztak dat nejaky
hint na reseni? Jsem asi uplne neschopnej, ale nemuzu s tim hnout

Která z následujících formulí je dokazatelna? Dokazte syntakticky:
(A->C)->[(B->C)->((A & B)->C)]
(C->(A v C))->(A->C)

Rekl bych ze dokazatelna je prvni a druha ne, ale dokazat to neumim :(.

Zostrojte Skolemovu normálnu formu A_s formule:
(Ey)B <-> ((Vy)B&(Vz)C)
Každá formula obsahuje voľnú iba tú premennú, ktorá je tesne pred ňou
kvantifikovaná.
Pozn.: Neviem, či som dobre opísal zátvorky :(

O Skolemove NF nemam moc poneti - nejaky hint jak se to prevadi?

Odpovím jen na první půlku...
Ta druhá není dokazatelná to máš pravdu, a to se nejlíp dokazuje tak, že najdeš protipříklad. Třeba A=1, C=0
Tu druhou jsem dokázal pomocí VD a převedení (A & B)->C pomocí V5 a pravidel na nonC->(A->nonB).

Takže asi takhle:

(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

Snad je to dobře.

K tej Skolemovej variante.

Nuz ja som to pochopil tak, ze zostrojis prenexny tvar formule, oznacme ho A. Potom pre kazdy existencny kvantifikator zavedies novy funkcny symbol a ak A je v tvare (Vx1)...(Vxm)(Ey)B tak ju nahradis (Vx1)...(Vxm)By[f(x1,...xn)], kde n je pocet volnych premennych v B. Postup opakujes, kym sa vo formuli vyskytuje existencny kvantifikator. Dostanes formulu oznacme ju As.

A potom podla lemmy ma platit |- As -> (povodna formula)

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 :D.

Takze ta Skolemova NF bude vypadat nejak takhle?

(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?

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

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.

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 :twisted: ]

Tuetschek wrote:

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 :D.

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 wrote: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.

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 :twisted: ]

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:

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)))

:?: :?: :?: :?: :?: :?:

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

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

Dawe wrote: Takže asi takhle:

(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

(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)

laliebijard wrote:Ja som to robil takto:

|-(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)?

twoflower wrote: 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.

laliebijard wrote:

twoflower wrote: 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:

(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)

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

qwyxyo wrote:

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?

twoflower wrote:

qwyxyo wrote:

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...

twoflower wrote: 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

Ahaa, diky, uz to chapu :)