Ex(x) A <-> Vs(x) A

kaktus64

Ex(x) A <-> Vs(x) A

Příspěvek od kaktus64 »

Zdravim,
podarilo sa mi dokazat, ze existencny a vseobecny kvantifikator su ekvivalentne :) a neviem kde tam mam chybu...

|- non Vs(x) non A <-> non Vs(x) non A // A <-> A
|- Ex(x) A <-> non non A // veta o ekvivalencii + specifikace x za x "Vs(x) non A -> non A" + generalizace "non A -> Vs(x) non A"
|- Ex(x) A <-> A // veta o ekvivalencii + "non non A <-> A"
|- Ex(x) A <-> Vs(x) A // veta o ekvivalencii + "Vs(x) A <-> A"

Chyba bude bud strasne zaludna alebo strasne zjavna pls help
Uživatelský avatar
czestmyr
Matfyz(ák|ačka) level I
Příspěvky: 6
Registrován: 2. 6. 2008 21:57
Typ studia: Informatika Bc.

Re: Ex(x) A <-> Vs(x) A

Příspěvek od czestmyr »

Myslim, ze problem bude s casti 'specifikace x za x "Vs(x) non A -> non A" '
Protoze schema specifikace je jenom implikace a ty tady vsude mas ekvivalenci. Zkus si to poradne rozepsat a myslim, ze ti to nevyjde ;)
Ja to jeste taky zkusim a kdyztak to sem postnu.

edit:
Takze vezmi si jenom implikaci zleva doprava:
|- Obrázek (Obrázekx) Obrázek A Obrázek Obrázek (Obrázekx) Obrázek A
Vezmeme instanci axiomu specifikace:
|- (Obrázekx) Obrázek A Obrázek Obrázek A
Jenomze problem je ted v tom, ze ty z toho vyvodis tohle, coz neplati (plati obracena implikace podle axiomu (A3)):
|- Obrázek (Obrázekx) Obrázek A Obrázek Obrázek Obrázek A

Proste - nemuzes vzit A -> B a udelat z toho Obrázek A -> Obrázek B
kaktus64

Re: Ex(x) A <-> Vs(x) A

Příspěvek od kaktus64 »

Skusal som si to rozpisat na male kroky a stale nechapem, kde je chyba. V kazdom riadku pouzivam len poznatky z riadkov skor uvedenych. V ktorom riadku mam chybnu uvahu ?

1. formule "non Vs(x) non A" splna definiciu formule
2. formule "non non A" vznikne z formule "non Vs(x) non A" nahradenim vyskytu formule "Vs(x) non A" za formuli "non A" //pojem nahradit z vety o ekvivalencii
3. formule "Vs(x) B -> B" je axiom specifikace a je platna pre lubovolnu formuli napriklad non A
4. "Vs(x) non A -> non A" je platna formule podla 3.
5. formule "B -> Vs(x) B" je dokazatelna pomocou pravidla generalizace a je platna pre lubovolnu formuli napriklad non A
6. "non A -> Vs(x) non A" je platna podla 5.
7. podla jedneho lemmatka plati "C -> D -> (C & D)" pre lubovolne formule napriklad C rovno "Vs(x) non A -> non A" a D rovno "non A -> Vs(x) non A"
8. podla 7. plati "(Vs(x) non A -> non A) & (non A -> Vs(x) non A)" co je skratka za "Vs(x) non A <-> non A"
9. body 2. a 8. vezmeme ako predpoklady vety o ekvivalencii a dostaneme "non non A <-> non Vs(x) non A"
10. "non non A <-> A" podla V3 a V4 z vyrokovej logiky + lemma z bodu 7.
11. z 10. a 9. podla vety o ekvivalencii "A <-> non Vs(x) non A"
12. kedze "non Vs(x) non A" je z definicie skratka za "Ex(x) A" dostavame "A <-> Ex(x) A"
13. podla bodov 3. 5. a 7. dostavame "A <-> Vs(x) A"
14. podla 12. 13. a vety o ekvivalencii dostavame "Vs(x) <-> Ex(x) A"

Mne osobne pride divne to miesto kde zmizne vseobecny kvantifikator z" non Vs(x) non A" a dostaneme "non non A" ale je to zdovodnene bodmi 3. a 9. v ktorych nenachadzam chybu.... pls help
Uživatelský avatar
czestmyr
Matfyz(ák|ačka) level I
Příspěvky: 6
Registrován: 2. 6. 2008 21:57
Typ studia: Informatika Bc.

Re: Ex(x) A <-> Vs(x) A

Příspěvek od czestmyr »

Zda se mi podezrelej bod 5.
Protoze pravidlo generalizace rika "A |- Vs(x) A" a ne "|- A -> Vs(x) A". Aby jsi to takhle mohl prevest podle vety o dedukci, tak by A musela byt uzavrena formule a v tom pripade si myslim, ze existencni a vseobecnej kvantifikator skutecne budou ekvivalentni, protoze ti to ohodnoceni v uzavreny formuli uz nezmeni.
Uživatelský avatar
czestmyr
Matfyz(ák|ačka) level I
Příspěvky: 6
Registrován: 2. 6. 2008 21:57
Typ studia: Informatika Bc.

Re: Ex(x) A <-> Vs(x) A

Příspěvek od czestmyr »

Pripadne pouzit pravidlo zavedeni vseobecnyho kvantifikatoru, ale to ma predpoklad, ze x nema v A volnej vyskyt, takze to je prast jak uhod.
kaktus64

Re: Ex(x) A <-> Vs(x) A

Příspěvek od kaktus64 »

No jasne to bude ono. Tu implikaciu "A -> Vs(x) A" som si hlbsie nerozoberal prislo mi to samozrejme ale veta o dedukci je tam fakt obmedzena. Ale je to vobec zaujimave, ked mozem z "A" odvodit "Vs(x) A" ale implikacia "A -> Vs(x) A" uz neplati :shock: ...asi mi usli nejake suvislosti. No nic, dik za pomoc... 8)
Uživatelský avatar
czestmyr
Matfyz(ák|ačka) level I
Příspěvky: 6
Registrován: 2. 6. 2008 21:57
Typ studia: Informatika Bc.

Re: Ex(x) A <-> Vs(x) A

Příspěvek od czestmyr »

Taky jdes zitra na zkousku? :D
kaktus64
Matfyz(ák|ačka) level I
Příspěvky: 22
Registrován: 3. 6. 2008 10:42
Typ studia: Informatika Mgr.

Re: Ex(x) A <-> Vs(x) A

Příspěvek od kaktus64 »

Ano idem a vzhladom na overenu linearnu zavislost narocnosti skusky od jej poradoveho cisla a to s dost vysokym koeficintom umernosti, by som ju rad dal :D
Odpovědět

Zpět na „2007“