HELP: Dokaz

qwyxyo · Příspěvek od **qwyxyo** » 4. 6. 2006 15:22

Najde sa nejaky logik, ktory je ochotny pomoct s dokazom formule

|= (∀x)[A(x,y) & B(x,y)] -> [(∀x)A(x,y) & (∀x)B(x,y)]

Ja som to nejak spraskal, ale v niektorych krokoch si nie som isty, resp. urcite nie su logicky ciste...

dr.Bik · Příspěvek od **dr.Bik** » 4. 6. 2006 19:03

A(x, y) znamena, ze ve formuli se vyskytuji jen promenne x a y?

Jestli jo, tak bych dokazal

Kód: Vybrat vše

(Vx)(A(x) & B(x)) -> ((Vx)A(x) & (Vx)B(x))

(V je vseobecny kvantifikator)

a potom bych pouzil vetu o konstantach:

Necht T je mnozina formuli jazyka L a A je formule tohoto jazyka.
Necht x_{1}, x_{2}, ..., x_{n} jsou vsechny jeji promenne

Necht jazyk L' vznikne z L pridanim konstant c_{1}, c_{2}, ..., c_{n}

Potom
v jazyku L': T |- A_{x_{1}, x_{2}, ..., x_{n}}[c_{1}, c_{2}, ..., c_{n}]

prave kdyz

v jazyku L: T |- A

qwyxyo · Příspěvek od **qwyxyo** » 4. 6. 2006 19:23

dr.Bik píše:A(x, y) znamena, ze ve formuli se vyskytuji jen promenne x a y?

Jestli jo, tak bych dokazal
Kód: Vybrat vše
(Vx)(A(x) & B(x)) -> ((Vx)A(x) & (Vx)B(x))
(V je vseobecny kvantifikator)

a potom bych pouzil vetu o konstantach:

Necht T je mnozina formuli jazyka L a A je formule tohoto jazyka.
Necht x_{1}, x_{2}, ..., x_{n} jsou vsechny jeji promenne

Necht jazyk L' vznikne z L pridanim konstant c_{1}, c_{2}, ..., c_{n}

Potom
v jazyku L': T |- A_{x_{1}, x_{2}, ..., x_{n}}[c_{1}, c_{2}, ..., c_{n}]

prave kdyz

v jazyku L: T |- A

No to beriem. Tak som to aj ja premyslel. Ale praveze chcem vidiet ako sa to dokaze...

dr.Bik · Příspěvek od **dr.Bik** » 4. 6. 2006 20:35

Tak tady:

Podle scemata specifikace

Kód: Vybrat vše

|- (Vx)(A&B) -> A&B

(je to specialni pripad, kdy jako substituujici term je substituovana promenna)

(Vx)(A&B) je uzavrena, takze lze pouzit vetu o dedukci

Kód: Vybrat vše

(Vx)(A&B) |- A&B

Z vyrokove logiky vime, ze

Kód: Vybrat vše

|-(A&B) -> A, B

je veta VL, tedy i PL. Pouzitim MP dostanu

Kód: Vybrat vše

(Vx)(A&B)|-A, B

Podle vety o uzaveru: pokud je formule dokazatelna, tak je dokazatelny i jeji uzaver

Kód: Vybrat vše

(Vx)(A&B)|-(Vx)A, (Vx)B

Podle vyrokove logiky plati, ze ze dvou formuli dokazu jejich konjunkci

Kód: Vybrat vše

(Vx)(A&B)|-(Vx)A & (Vx)B

No a nakonec jednou veta o dedukci (tu muzu pouzit, protoze formule je uzavrena)

qwyxyo · Příspěvek od **qwyxyo** » 4. 6. 2006 20:43

dr.Bik píše:Tak tady:

Podle scemata specifikace
Kód: Vybrat vše
|- (Vx)(A&B) -> A&B
(je to specialni pripad, kdy jako substituujici term je substituovana promenna)

(Vx)(A&B) je uzavrena, takze lze pouzit vetu o dedukci
Kód: Vybrat vše
(Vx)(A&B) |- A&B
Z vyrokove logiky vime, ze
Kód: Vybrat vše
|-(A&B) -> A, B
je veta VL, tedy i PL. Pouzitim MP dostanu
Kód: Vybrat vše
(Vx)(A&B)|-A, B
Podle vety o uzaveru: pokud je formule dokazatelna, tak je dokazatelny i jeji uzaver
Kód: Vybrat vše
(Vx)(A&B)|-(Vx)A, (Vx)B
Podle vyrokove logiky plati, ze ze dvou formuli dokazu jejich konjunkci
Kód: Vybrat vše
(Vx)(A&B)|-(Vx)A & (Vx)B
No a nakonec jednou veta o dedukci (tu muzu pouzit, protoze formule je uzavrena)

Tak som to prave na dialku prediskutoval s mojim cviciacim. Cely cas som na to isiel zle, lebo mi nedoslo, ze tu konjukciu na pravej strane nemam za kazdu cenu menit na implikaciu, ale ze to staci dokazat rozborom pripadov. Podarilo sa mi to z opacnej strany ako tebe. A inak diky. Oba sposoby su zrejme dobre...