Par dotazu pred zkouskou

Medved_

Par dotazu pred zkouskou

Příspěvek od Medved_ »

Tak mam v utery zkousku, pomalu se ucim, tak budu postupne klast otazky, neva? :)

Dokazte:

(A->B) -> [ (B->C) -> (A->C) ]

Muj "dukaz"
1) Prepisu dle Vety o dedukci
A->B,B->C,A |- C

2) Vim, ze dle Modus Ponens muzu nahradit A,A->B za B, udelam to v predpokladech 1)
B,B->C |-C

3) Opet dle MP muzu nahradit B,B->C za C, udelam v predpokladech 2)
C |- C

4) Upravim dle vety o dedukci, a dostanu vetu 1 VL
|- C->C

Otazka? Je toto KOREKTNI dukaz na plny pocet bodu? Umim timto stylem dokazat temer vsechno z VL, ale kdyz by po me chtel nekdo dukaz dle definice (tzn. pouze axiomy, zname vety a modus ponens), tak to nedokazu. Ono to totiz obratit tak jednoduse nejde. Treba z 3ky 2ku nedostanu (opacny modus ponens neni nikde zminen)

Dik, postupne to tady bude pribyvat, byl bych rad kdyby i ostatni nahodoli sve problemy a poznatky :)
Osiris
Supermatfyz(ák|ačka)
Příspěvky: 403
Registrován: 11. 11. 2006 14:10
Typ studia: Informatika Mgr.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Osiris »

Medved_ píše:...
Osobně si myslím, že by ti to nevzali. Nicméně když máš větu výrokové logiky, tak si můžeš na levou stranu před dokazovátkem naházet cokoliv.

Zde je korektní důkaz:

A, A->B |- B (MP)
B, B->C |- C (MP)

A, A->B, B->C |- B (MP)
A, A->B, B->C |- C (MP)
A->B, B->C |- A->C (VD)
A->B |- (B->C) -> (A->C) (VD)
|-(A->B) -> [(B->C) -> (A->C)] (VD)
Osiris
Medved_

Re: Par dotazu pred zkouskou

Příspěvek od Medved_ »

Uz to trochu chapu, diky...
Jenom v tom nevidim ten korektni dukaz, ten prece musi zacinat bud axiomem nebo vetou VL.
Osiris
Supermatfyz(ák|ačka)
Příspěvky: 403
Registrován: 11. 11. 2006 14:10
Typ studia: Informatika Mgr.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Osiris »

Medved_ píše:Uz to trochu chapu, diky...
Jenom v tom nevidim ten korektni dukaz, ten prece musi zacinat bud axiomem nebo vetou VL.
Modus ponens je víceméně axiom. Jen se tomu neříká axiom, ale odvozovací pravidlo.
Osiris
Triebenekl
Matfyz(ák|ačka) level I
Příspěvky: 10
Registrován: 5. 2. 2007 20:55
Typ studia: Informatika Bc.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Triebenekl »

Myslim, ze to, co napsal Medved taky neni k zahozeni - je to vlastne takova priprava na formalni dukaz.

Z Medvedova bodu 1) se dozvime, ze pro zacatek dukazu vezmeme teorii T={A->B,B->C,A} a budem z ni chtit dokazat C,
nakonec pouzijeme trikrat vetu o dedukci opacnym smerem.

Formalni dukaz (prakticky to same, co napsal Osiris):
1) A->B,B->C,A |- A
(pozn.: Dokazovani A|-A je z definice dukazu z predpokladu.)
2) A->B,B->C,A |- A->B
(2: podobne jako 1)

pomoci MP z 1) a 2) odvodim:
3) A->B,B->C,A |- B
4) A->B,B->C,A |- B->C
(4: podobne jako 1)

pomoci MP z 3) a 4) odvodim:
5) A->B,B->C,A |- C

a ted uz jen pouziji trikrat Vetu o dedukci a dostavam:
6) |- (A->B) -> [ (B->C) -> (A->C) ]


(Kdyby tam byla chyba, tak me opravte - taky jdu v utery na zkousku...)
Medved_

Re: Par dotazu pred zkouskou

Příspěvek od Medved_ »

Jasny, uz to chapu.

Jen teda by se tam sluselo dopsat, treba k tomu bodu jedna, ze:

|- A->A (V1)
A |- A (VD)
A->B,B->C,A |- A (Pridame predpoklady, coz muze protoze dusledek za vetou o kompaktnosti)

Podobne ty ostatni body a zbytek je korektni, ted je to 100% dukaz dle definice a jsem spokojen :)


Dalsi vec... Muzu kdekoliv v dokazovani nahradit "preprocesorove" vyskyt non non B za B? Treba ve formuli A->B->non nonB -> D? Kdyz jo, tak proc? :)
Triebenekl
Matfyz(ák|ačka) level I
Příspěvky: 10
Registrován: 5. 2. 2007 20:55
Typ studia: Informatika Bc.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Triebenekl »

nahrazeni non non B za B:
O tom je cela Veta o Ekvivalenci.

Takze pred tim, nez dokazes vetu o ekvivalenci to nemuzes delat primo (musis pouzit napr. (v3) nebo (v4) + MP).
Kdyz si dokazes vetu o ekvivalenci, tak uz muzes nahrazovat kdekoliv cokoliv.
Medved_

Re: Par dotazu pred zkouskou

Příspěvek od Medved_ »

Jasny, jsem to blbec ...

Kdybysis nahodou delal ta cviceni za kapitolama a chtel se podelit o vysledky, nebo vedel, kde uz to je vyresene, tak bych byl moc rad :)
Triebenekl
Matfyz(ák|ačka) level I
Příspěvky: 10
Registrován: 5. 2. 2007 20:55
Typ studia: Informatika Bc.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Triebenekl »

Medved_ píše: Jen teda by se tam sluselo dopsat, treba k tomu bodu jedna, ze:
|- A->A (V1)
A |- A (VD)
Myslim, ze to s (v1) tady neni potreba.

Vtip je v tom, ze pri dukazu (definice) je kazdy krok bud axiom nebo odvozeni z minulych pomoci MP.
Pri dukazu z predpokladu T (definice) je kazdy krok bud axiom nebo formule z T nebo odvozeni z minulych pomoci MP.
Takze v nasem pripade je A formule z predpokladu a da se to napsat rovnou.

Ale jinak v tom taky docela plavu - je toho z logiky hodne.
Medved_

Re: Par dotazu pred zkouskou

Příspěvek od Medved_ »

Tak a ted jeden dotaz k PL. Mam vetu o dedukci, ta rika, ze kdyz je formule A uzavrena, tak T |- A->B prave kdyz T,A |-B.

Jenze mi A s volnymi promennymi vubec nevadi, protoze si udelam A' jeji uzaver, vim z vety o uzaveru, ze |-A prave kdyz |-A' a ted pouziju vetu o ekvivalenci a do vety o dedukci jakoby dosadim A'...

Je mi jasne, ze ta uvaha je spatne, kdyz se to musi resit pres vetu o konstantach (kterou taky moc nechapu), jen nevim, kde je spatne.
Medved%

Re: Par dotazu pred zkouskou

Příspěvek od Medved% »

Jeste takovy trapny dotaz: odkud jste se ucili treba dokazovani v Peanove aritmetice? Ja ve skriptech snad ani nenasel axiomy, natoz tak nejake navody na to, jak dokazovat...
ivan
Matfyz(ák|ačka) level I
Příspěvky: 10
Registrován: 15. 6. 2007 00:32

Re: Par dotazu pred zkouskou

Příspěvek od ivan »

Medved% píše:Jeste takovy trapny dotaz: odkud jste se ucili treba dokazovani v Peanove aritmetice? Ja ve skriptech snad ani nenasel axiomy, natoz tak nejake navody na to, jak dokazovat...
To bych taky chtel vedet. Stravil jsem pulku dne na googlu a nic moc tam neni... Navic, kazdy tam ma jine axiomy, takze jsem uz hodne nastvany :evil:
Osiris
Supermatfyz(ák|ačka)
Příspěvky: 403
Registrován: 11. 11. 2006 14:10
Typ studia: Informatika Mgr.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Osiris »

ivan píše:
Medved% píše:Jeste takovy trapny dotaz: odkud jste se ucili treba dokazovani v Peanove aritmetice? Ja ve skriptech snad ani nenasel axiomy, natoz tak nejake navody na to, jak dokazovat...
To bych taky chtel vedet. Stravil jsem pulku dne na googlu a nic moc tam neni... Navic, kazdy tam ma jine axiomy, takze jsem uz hodne nastvany :evil:
Ve skriptech axiomy jsou, pokud vím. Někde vzadu.
Osiris
Osiris
Supermatfyz(ák|ačka)
Příspěvky: 403
Registrován: 11. 11. 2006 14:10
Typ studia: Informatika Mgr.
Bydliště: Praha
Kontaktovat uživatele:

Re: Par dotazu pred zkouskou

Příspěvek od Osiris »

Medved% píše:Jeste takovy trapny dotaz: odkud jste se ucili treba dokazovani v Peanove aritmetice? Ja ve skriptech snad ani nenasel axiomy, natoz tak nejake navody na to, jak dokazovat...
Kdyby byly návody jak dokazovat, tak jsou dokázány takové věci jako například otázka P = NP a podobné věci :roll:
Osiris
Medved_

Re: Par dotazu pred zkouskou

Příspěvek od Medved_ »

Jasne, myslel jsem to spis tak, ze treba k VL mame dokazanych asi 10 vet + nejake pokrocilejsi nastroje pro dokazovani, takze se pomoci toho da uz leccos vymyslet, navic na tech dukazech vidis zhruba tu techniku, jak na to. Kdezto v Peanove aritmetice toho moc nedokazes, kdyz ti neukazi jak na to. Proste me tenhle predmet sere, tak jsem chtel vyjadrit svoji frustraci, no :D:D

To je jak, kdyby ti v analyze dali axiomy realnejch cisel a chteli po tobe pocitat limity :X
Odpovědět

Zpět na „2007“