Ex(x) A <-> Vs(x) A
Ex(x) A <-> Vs(x) A
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
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
- czestmyr
- Matfyz(ák|ačka) level I
- Příspěvky: 6
- Registrován: 2. 6. 2008 21:57
- Typ studia: Informatika Bc.
- Login do SIS: housc6am
Re: Ex(x) A <-> Vs(x) A
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:
|- (x) A (x) A
Vezmeme instanci axiomu specifikace:
|- (x) A A
Jenomze problem je ted v tom, ze ty z toho vyvodis tohle, coz neplati (plati obracena implikace podle axiomu (A3)):
|- (x) A A
Proste - nemuzes vzit A -> B a udelat z toho A -> B
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:
|- (x) A (x) A
Vezmeme instanci axiomu specifikace:
|- (x) A A
Jenomze problem je ted v tom, ze ty z toho vyvodis tohle, coz neplati (plati obracena implikace podle axiomu (A3)):
|- (x) A A
Proste - nemuzes vzit A -> B a udelat z toho A -> B
Re: Ex(x) A <-> Vs(x) A
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
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
- czestmyr
- Matfyz(ák|ačka) level I
- Příspěvky: 6
- Registrován: 2. 6. 2008 21:57
- Typ studia: Informatika Bc.
- Login do SIS: housc6am
Re: Ex(x) A <-> Vs(x) A
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.
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.
- czestmyr
- Matfyz(ák|ačka) level I
- Příspěvky: 6
- Registrován: 2. 6. 2008 21:57
- Typ studia: Informatika Bc.
- Login do SIS: housc6am
Re: Ex(x) A <-> Vs(x) A
Pripadne pouzit pravidlo zavedeni vseobecnyho kvantifikatoru, ale to ma predpoklad, ze x nema v A volnej vyskyt, takze to je prast jak uhod.
Re: Ex(x) A <-> Vs(x) A
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 ...asi mi usli nejake suvislosti. No nic, dik za pomoc...
- czestmyr
- Matfyz(ák|ačka) level I
- Příspěvky: 6
- Registrován: 2. 6. 2008 21:57
- Typ studia: Informatika Bc.
- Login do SIS: housc6am
Re: Ex(x) A <-> Vs(x) A
Taky jdes zitra na zkousku?
-
- 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
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