prirodna dedukcija

prirodna dedukcija 11.03.2016. u 12:41 · pre 129 meseci #1

Uradio sam na nekoliko nacina ali ispada da nije dobar ni jedan.

- Solver je dao skoro 120 linija
- Ja isao sa pretpostavkam

(((p<=> q) <=>r) & (q<=> r)) => p is valid.
1. ~ (((p<=> q) <=>r) & (q<=> r)) => p (~ negacija)
2. (((p<=> q) <=>r) & (q<=> r)) (1)
3. ~ p (1)
4. ((p<=> q) <=>r) (&E,2)
5. q<=> r (&E,2)
6. q (5)
7. r (5)
8. ~q (5)
9. ~ r (5)
10. (p<=> q) (4)
11. r (4)
12. ~ (p<=> q) (4)
13. ~ r (4)
14. p (10)
15. q (10)
16. ~ p (10)
17. ~q (10)
18. (p q) (4)
19. r (4)
20. (p<=> q) (4)
21. r (4)
22. p (20)
23. q (20)
24. ~ p (20)
25. ~ q (20)

ali nisam siguran da su pravila izvodjenja iskoriscena kako treba

Evo sta sam poslednje probao, ali nisam siguran idem li u dobrom pravcu i kako bi izgledalo bez pretpostavki

1. ~ ((((p⟺q)⟺r) & (q⟺r))⇒p )
2. (((p⟺q)⟺r) & (q⟺r))
3. ~ p - assume
4. (p⟺q⟺r) & (q⟺r) from 2
5. (p⟺q⟺r) &E,4
6. (q⟺r) &E,4
7.p=>(q<=>r) from 4
8.(q<=>r) => p from 4
9.p(=>E 6,8)

Re: prirodna dedukcija 15.03.2016. u 20:04 · pre 129 meseci #2

Mislim da ne može bez pretpostavki. Zbog ekvivalencije q<=>r imaš dva slučaja: q, r i ~q, ~r.

Potpis

Nije bitno koji su zaključci izvučeni, već kako se do njih došlo.

Re: prirodna dedukcija 15.03.2016. u 20:14 · pre 129 meseci #3

Hvala. ja sam nesto uspeo koristeci pravila i aksiome.
Dosao sam do p na kraju, ali nisam siguran da je OK. Cim nadjem vremena okacicu da proveris.

Srdacan pozdrav

Kakav si sa ovim u prilogu. Ako mozes da spicis pa da castim za ovoliku pomoc. Pozdrav

Zadatak.jpg58.27k

Re: prirodna dedukcija 16.03.2016. u 15:34 · pre 129 meseci #4

(a) (i) $(\forall x)(\forall y)x\approx y$ .
(a) (ii) $(\exists x)(\exists y)\lnot\,x\approx y$ .
(a) (iii) $(\forall x)(\forall y)(\forall z)(x\approx y\,\lor\,x\approx z\,\lor\,y\approx z)$ .

(b) Modeli ove vrste su izomorfni ako i samo ako imaju domene iste kardinalnosti. Stoga su svi modeli sa $m$ elemenata izomorfni. Medju svim ovakvim modelima sa najviše $n$ elemenata ima tačno $n$ neizomorfnih, odnosno ima ih konačno mnogo. Neka su ${\cal M}_1,\dots,{\cal M}_n$ svi takvi neizomorfni modeli. Recimo da ${\cal M}_k$ ima tačno $k$ elemenata. Dokazaćemo da je ova klasa modela kompaktna na osnovu toga što ima samo konačno mnogo neizomorfnih modela.

Recimo da nije kompaktna i izvedimo kontradikciju. Neka je $\Gamma$ skup formula koji nije zadovoljiv u $\Theta$ , ali čiji je svaki konačan podskup zadovoljiv u $\Theta$ . Obzirom da skup $\Gamma$ nije zadovoljen ni u jednom od od modela ${\cal M}_1,\dots,{\cal M}_n$ , za svako $k\in\{1,\dots,n\}$ postoji neko $\varphi_k\in\Gamma$ takvo da ${\cal M}_k\not\models\varphi_k$ . Skup $\{\varphi_1,\dots,\varphi_n\}$ je konačan podskup od $\Gamma$ koji nije zadovoljen ni u jednom od modela iz $\Theta$ jer je svaki od modela iz $\Theta$ izomorfan sa nekim od ${\cal M}_1,\dots,{\cal M}_n$ , što je suprotno pretpostavci da je svaki konačan podskup od $\Gamma$ zadovoljiv u $\Theta$ .

(c) Neka je $\varphi_n$ formula $(\exists x_1)\cdots(\exists x_n)\bigwedge_{i=1}^{n-1}\bigwedge_{j=i+1}^n\lnot\,x_i\approx x_j$ , gde je $n\geqslant 2$ . Ona je zadovoljena upravo u onim ovakvim modelima koji imaju barem $n$ elemenata.

Skup $\Gamma=\{\varphi_n\,|\,n\geq 2\}$ nije zadovoljiv ni u jednom konachnom modelu, ali svaki njegov konachan podskup jeste. Stoga klasa svih konačnih modela nije kompaktna.

Potpis

Nije bitno koji su zaključci izvučeni, već kako se do njih došlo.

Re: prirodna dedukcija 16.03.2016. u 16:27 · pre 129 meseci #5

Ti si genije . Moram da te vodim na pice i klopu, a posto cu imati neke zadatke daj da ti ih saljem na mejl, a ti kazi da li mozes da ih radis i za koje pare. Juce je lik davao 150$( od toga bi tvoje bilo 90$ - 60% pripada tutoru,a ostatak uzima portal.) za neke zadatke iz ekonomske matematike, mada meni ono lici na differencijalne, ali za neke ekonomske velicine. Niko da uzme posto je sutra rok da se urade.

Ajd eako ti nije mrsko baci pogled na 3.7 koji je isto ovo sto si radio.

Ja sam poslao ovom studentu, ali ima neka podpitanja. (je... ti 10 $ za 2 zadatka kada mecku rodim,a nije mi oblast)

Mozes li za 3.8 b i c da mi kazes koje teoreme bi trebale posto mora na engleskom pa cisto da ne prevodim nego da iskontrolisem.

Ne znam odakle si, ali ako je Sumadija ili BG vidimo se uskoro.

Pozdrav

Zadatak.docx761.46k

Re: prirodna dedukcija 16.03.2016. u 19:35 · pre 129 meseci #6

Nikakve posebne teoreme ne trebaju.

Između takvih modela je izomorfizam isto što i bijekcija, jer se interpretacija binarnog relacijskog znaka svodi na jednakost, a jednakost i različitost su bijekcijom očuvani.

Izomorfni modeli zadovoljavaju iste rečenice, ako je to neka teorema. Mislim, ima dokaz indukcijom po složenosti formule, ali se mora malo preformlisati tako da se odnosi na sve formule, a ne samo rečenice. Koristi se prelaz od valuacije jednog modela na valuaciju drugog modela preko te bijekcije. Naravno, treba prvo dokazati odnos između vrednosti termova pri valuacijama u odnosu na tu bijekciju. U ovom slučaju su jedini termi promenljive.

Neka imamo dva modela istog jezika ${\cal M}_1=(D_1,I_1)$ i ${\cal M}_2=(D_2,I_2)$ , gde su $D_1$ i $D_2$ domeni, a $I_1$ i $I_2$ interpretacije simbola jezika i neka je $f:D_1\longrightarrow D_2$ izomorfizam. Neka je $v_1$ valuacija nad prvim domenom i $v_2$ valuacija nad drugim domenom definisana sa

$v_2(x)=f(v_1(x))$ .

Za vrednosti termova pri valuacijama važi:

$I_2^{v_2}[t]=f(I_1^{v_1}[t])$ .

Dokaz:

Za promenljive važi

$I_2^{v_2}[x]=v_2(x)=f(v_1(x))=f(I_1^{v_1}[x])$ .

Prvi prelaz je na osnovu definicije vrednosti terma, drugi na osnovu definicije valuacije $v_2$ i treći na osnovu definicije vrednosti terma.
na osnovu izbora valuacije $v_2$ .

Za simbole konstanti je

$I_2^{v_2}(c)=I_2(c)=f(I_1(c))=f(I_1^{v_1}(c))$ .

Prvi prelaz je po definiciji vrednosti terma, drugi po definiciji izomorfizma i treći po definiciji vrednosti terma.

Za operacijske simbole je

$I_2^{v_2}[g(t_1,\dots,t_n)]=I_2(g)(v_2[t_1],\dots,v_2[t_n])=I_2(g)(f(v_1[t_1]),\dots,f(v_1[t_n]))=f(I_1(g)(v_1[t_1],\dots,v_1[t_n]))=f(I_1^{v_1}[g(t_1,\dots,t_n)])$

Prvi prelaz je na osnovu definicije vrednosti terma, drugi na osnovu induktivne pretpostavke da tvrđenje važi za jednostavnije terme, treći na osnovu definicije izomorfizma i četvrti na osnovu definicije vrednosti terma.

Za formule važi:

${\cal M}_1\models_{v_1}\varphi\,\,\,\Leftrightarrow\,\,\,{\cal M}_1\models_{v_1}\varphi$ .

Dokaz:

Jednakost:

${\cal M}_1\models_{v_1}t_1=t_2\,\,\,\Leftrightarrow\,\,\,I_1^{v_1}[t_1]=I_1^{v_1}[t_2]\,\,\,\Leftrightarrow\,\,\,f(I_1^{v_1}[t_1])=f(I_1^{v_1}[t_2])\,\,\,\Leftrightarrow\,\,\,I_2^{v_2}[t_1]=I_2^{v_2}[t_2]\,\,\,\Leftrightarrow\,\,\,{\cal M}_2\models_{v_2}t_1=t_2$ .

Prvi prelaz je na osnovu definicije relacije zadovoljenja, drugi na osnovu injektivnosti izomorfizma, treći na osnovu prethodnoog stava i četvrti na osnovu definicije relacije zadovoljenja.

Relacijske formule

${\cal M}_2\models_{v_2}R(t_1,\dots,t_n)\,\,\,\Leftrightarrow\,\,\,I_2(R)(I_2^{v_2}[t_1],\dots,I_2^{v_2}[t_n])\,\,\,\Leftrightarrow\,\,\,I_2(R)(f(I_1^{v_1}[t_1]),\dots,f(I_1^{v_1}[t_n]))\,\,\,\Leftrightarrow\,\,\,I_1(R)(I_1^{v_1}[t_1],\dots,I_1^{v_1}[t_n])\,\,\,\Leftrightarrow\,\,\,{\cal M}_1\models_{v_1}R(t_1,\dots,t_n)$ .

Prvi prelaz je po definiciji relacije zadovoljenja, drugi po definiciji valuacije $v_2$ , treći po definiciji izomorfizma i četvrti po definiciji relacije zadovoljenja.

Negacija:

${\cal M}_2\models_{v_2}\lnot\varphi\,\,\,\Leftrightarrow\,\,\,{\cal M}_2\not\models_{v_2}\varphi\,\,\,\Leftrightarrow\,\,\,{\cal M}_1\not\models_{v_1}\varphi\,\,\,\Leftrightarrow\,\,\,{\cal M}_1\models_{v_1}\lnot\varphi$ .

Prvi prelaz je po definiciji relacije zadovoljenja, drugi po induktivnoj pretpostavci da tvrđenje važi na jednostavnijim formulama, treći po definiciji relacije zadovoljenja.

Konjunkcija:

${\cal M}_2\models_{v_2}\varphi\land\psi\,\,\,\Leftrightarrow\,\,\,({\cal M}_2\models_{v_2}\varphi)\land({\cal M}_2\models_{v_2}\psi)\,\,\,\Leftrightarrow\,\,\,({\cal M}_1\models_{v_1}\varphi)\land({\cal M}_1\models_{v_1}\psi)\,\,\,\Leftrightarrow\,\,\,{\cal M}_1\models_{v_1}\varphi\land\psi$ .

Prvi prelaz je po definiciji relacije zadovoljenja, drugi po induktivnoj pretpostavci da tvrđenje važi na prostijim formulama i treći po definiciji relacije zadovoljenja. Naravno, korišćena je konjunkcija i na metanivou.

Sa ostalim veznicima se postupa slično.

Univerzalni kvantifikator:

${\cal M}_1\models_{v_1}(\forall x)\varphi\,\,\,\Leftrightarrow\,\,\,(\forall a\in D_1)({\cal M}_1\models_{v_1/(x=a)}\varphi)\,\,\,\Leftrightarrow\,\,\,(\forall a\in D_1)({\cal M}_2\models_{v_2/(x=f(a))}\varphi)\,\,\,\Leftrightarrow\,\,\,(\forall b\in D_2)({\cal M}_2\models_{v_2/(x=b)}\varphi)\,\,\,\Leftrightarrow\,\,\,{\cal M}_2\models_{v_2}(\forall x)\varphi$ .

Prvi prelaz je na osnovu definicije relacije zadovoljenja, drugi po induktivnoj pretpostavci da tvđenje važi na jednostavnijim formulama i po definiciji prelaza sa valuacije nad $D_1$ na valuaciju nad $D_2$ , treći po surjektivnosti izomorfizma i četvrti po definiciji relacije zadovoljenja. Naravno, koristi se univerzalna kvantifikacija na metanivou, a $v/(x=a)$ označava valuaciju $v'$ takvu da je $v'(x)=a$ i $v'(y)=v(y)$ za sve promenljive $y$ koje nisu promenljiva $x$ .

Istinitosna vrednost formule u modelu ista za sve valuacije koje na isti način slikaju slobodne promenljive. To se takođe dokazuje indukcijom po složenosti formule, a najpre za vrednosti termova i tehnika je slična kao malopre. Odatle slei da istinitosna vrednost rečenica ne zavisi od valuacije, pa je

${\cal M}_1\models\varphi\,\,\,\Leftrightarrow\,\,\,{\cal M}_2\models\varphi$ .

Potpis

Nije bitno koji su zaključci izvučeni, već kako se do njih došlo.

Re: prirodna dedukcija 16.03.2016. u 21:46 · pre 129 meseci #7

Da ne budem bezobrazan, ali moram da te pitam kako da te castim ili da ti jednostavno uplatim bar 1000 dinara( to je ovo sto cu uzeti za ove zadatke).
Prethodni post se ceo odnosi na vec uradjen zadatak 3.8 ili na 3.7
Ako imas vremena samo mi kazi ako si bacio pogled smem li da odgovorim onako na 3.7
Da to spakujem na engleskom.

Jesi li raspolozen za neku dalju saradnju.
Ja bi preuzimao i zadatke koje ne znam i prosledjivao tebi.
Ako odlucis da zelis da radis ti definises cifru i onda ispregovaram i cim okacim zadatke pare su rezervisane. Dobijam ih na pocetku svakog meseca za prethodni.
Tako bi prosledjivao i tebi.

Pozdrav

Re: prirodna dedukcija 17.03.2016. u 02:51 · pre 129 meseci #8

Prihvatljivo je rešenje koje si priložio.

Potpis

Nije bitno koji su zaključci izvučeni, već kako se do njih došlo.

Re: prirodna dedukcija 17.03.2016. u 08:28 · pre 129 meseci #9

Hvala.

Poslacu ti zavrsenu verziju da mi kazes da li je to to.
Javi kako da se organizujemo za ovo cascavanje, a i eventualnu saradnju.

Srdacan pozdrav

Forum kao aplikacija na telefonu

Srodne teme