Ha a testvér azt jelenti hogy "ugyanazok a szüleik" akkor mindenkinek van testvére. Ki?

42: "Ki az a végtelen számú testvéred?"

Hát én!

Legyen U halmaz („univerzum”).

Az U univerzumon pedig

szereti ⊆ U × U bináris reláció, továbbá

babám, én ∈ U elem legyen adva úgy, hogy teljesül rájuk az alábbi két állítás:

∀x szereti(x, babám)

∀y szereti(babám, y) → y = én

Vezesd le a fenti két állításból mint premisszákból a

babám = én

következményt a Gentzen-féle természetes levezetés szerint.

Megoldás:

** 1) lépés **

∀x szereti(x, babám) állításra alkalmazd az univerzális kvantor kiküszöbölésének szabályát az x := babám behelyettesítéssel:

∀x szereti(x, babám)

——— ∀Elim[x:=babám] ———

szereti(babám, babám)

ím megkaptad a szereti(babám, babám) állítást.

** 2) lépés **

∀y szereti(babám, y) → y = én állításra szintén alkalmazd az univerzális kvantor kiküszöbölésének szbályát az y := babám behelyettesítéssel:

∀y szeret(babám, y) → y = én

——— ∀Elim[x:=babám] ———

szereti(babám, babám) → babám = én

ím megkaptad a szereti(babám, babám) → babám = én állítást.

** 3) lépés **

Alkalmazd az implikáció-kiküszöbölési, vagyis a modus ponens levezetési szabályt az 1)-2) lépésben kapott két állításra:

szeret(babám, babám) → babám = én

szeret(babám, babám)

——— →Elim ———

babám = én

A fenti levezetés ábrázolható az elsőrendű predikátumkalkulus nyelvén, ahol

*szereti* legyen relációjel 2-es aritással (kétváltozós predikátumjel)

és *én*, *babám* legyen individuumnév/konstans, azaz függvénykonstans 0-aritással.

Az Agda igazolta:

[link]

de az Agda használatát stabilabban kellene még gyakorolnom.

A babámos feladat után a testvéres feladatot is igazolta az Agda (ehhez valamivel kevesebb eszköz is elég volt, az egyenlőségre való közvetlen hivatkozás kikerülhető volt, és közvetlenül poszulátumokra sem volt szükség):

[link]

40/ A kérdező kommentje:

"Nem értem mit beszélsz, itt nincs személynév"

Ha a képletbe nem lehet a valóságnak megfelelően személyneveket behelyettesíteni, akkor nem stimmel a képlet. :) Másik, hogy látni ugye, hogy képlet van és nincs személynév, viszont írd le behelyettesítve személynevekkel is, hogy látható legyen a realitása.

Ha van két krumpli matematikai összeadása, mondjuk x + y = z, az behelyettesíthető kruplival, vagyis x-krumpli + y-krumpli = z-krumpli. Ha nem használható kimutathathóan a gyakorlatban a képlet, akkor fals. :)

"meg kell határozni mit jelent az a szó hogy testvér,"

Ez már ovodában megtörtént és ott a szótári és egyéb hozzáfűzött értelmezés. Tehát meg van határozva és ez nem valamiféle nehézség, és ne állítsuk be annak. :)

Amit írtál ott alapból már két testvér van és nem egyszem gyerek:

"képlettel: x és y szülei ugyanazok := (anyja(x) = anyja(y)) és/vagy (apja(x) = apja(y))."

Kérdés az, hogy a fentit a gyakorlatban, hogyan érted? Mert nem lehet kivenni, ki kicsoda is, már az is zavaros benne.

x-Feri-gyermek és y-Kati-gyermek szülei ugyanazok? Tehát van két gyermek és a szüleik ugyanazok. Eddig nyilvánvaló, hogy testvérek. És ez kb ennyi is. :)

Vagy a kérdés kiírásnál is ugyanaz, hogy ki kicsoda benne.

Testvér(x, y) := [(Anya(x) = Anya(y)) és/vagy (Apa(x) = Apa(y))]

Ha jól érteni van két testvér, x és y. És mindkettőenk ugyanaz az anyukája és apukája. Hol lenne gond ezzel?

Ez semmi más mint a hétköznapi eset:

Anya + Apa

gyerekeik: x, y

Gyakorlati példa arra, hogy az ,,egybeeső individuumok'' fogalma hasznos lehet:

Lekötözve ül egyszerű priccsén a fogoly a kis cellájában, amit a priccsen kívül semmi más tárgy nincs. Belép az őr, leül mellé a priccsre és gonoszul mondja:

— Adok egy feladatot, ha teljesíted, szabadon elmehetsz. Úgysem fogod tudni teljesíteni. Ülj le valahova, ahova én nem tudok leülni. Ha tényleg nem tudom utánad csinálni elmehetsz. Bár kiváncsi vagyok, hova is tudnál, úgy hogy én ne tudjam ugyanazt, hisz szinte semmi sincs ebben az ócska cellában, és te nehezebben is mozogsz nálam.... Hé, most mit csinálsz? Basszus!!!

x + y = 10, ahol a számjegyek (0,1,2..9) közül kerülhetnek ki az értékek.

A kis egyenlet megoldásaira mondjuk azt, hogy x ,,számjegypárja'' y-nak.

Hány ilyen számjegypár létezik?

Van-e számjegy, amely saját maga párja?