kenyérpuding - v0.2 logika 📘🌱
ilyen mintákat látok meg, mióta a matematikával, logikával foglalkozom
az is hasonló mintának tűnik, hogy nemtudom, hogy ez logika, vagy pedig absztrakt matematika
talán megtudom mutatni, hogyan:
Kenyérpuding. ("the proof is in the pudding", a puding próbája az evés)
Sokáig nem értettem a próba lényegét, a bizonyításra gondolok. Aztán azthiszem elkezdtem valamennyire megérteni, és kisebb megvilágosodás volt, hogy a bizonyítást lehet útként nézni.
A szemléljük szépnek tűnik, a tekintsük számomra most furcsán hat! [1]
Azthiszem minnél többet tudunk egy dologról, vagy talán minél több perspektívából, megfogalmazásban, oldalról felfedezzük, annál jobb képet kapunk róla.
Út annyit tesz: // nemtudom hol olvastam ilyeneket, talán Hamvas Bélától)
A ⟶ B
a nyílnak nevet is adhatunk:
f: A ⟶ B
vagy:
$A \xrightarrow{f} B$
// így írható: $A \xrightarrow{f} B$
Azthiszem azért is használják nyomtatásban az f: A→B jelölést, mert könyebb (volt?) megjeleníteni mint $A \xrightarrow{f} B$
vagy:
- Hom A B
- A → B ≡ Π (_ : A), B
ezt még nem értem, de érdekesnek tűnik
Exercise 0.21 Találj ki új szimbólumot az "út" fogalmára.
Azthiszem lehet mindent nyilakkal formálisan ábrázolni, például
A: A ⟶ A
≡ $A \xrightarrow{A} A$
≡ $\xrightarrow{A}$
Ez is egy ráébredés volt a számomra, hogy az 𝑥 is lehet út:
𝑥 : 𝑥 → 𝑥
≡ $x \xrightarrow{x} x$
≡ $\xrightarrow{x}$
theorem id (. ) : A → A := fun x => x
Mi a tétel? axióma → lemma → tétel
A lemma kisebb tétel.
A kalkulusban a d egy nagyon kicsi valami, az ∫ pedig összeg.
d ⊣ ∫, ez egy érdekes minta szerintem,
lokális ⊣ globális
belégzés ⊣ kilégzés
kérdés ⊣ válasz
falevelek ⊣ törzs
yin ⊣ yang
⊣ az adjoint jele
↗ inhale (arch spine) ⇄ exhale (curl spine) ↘ ⟺ adjoint pair
🐱 ⊣ 🐮
macska tehén? Adho mukhasana
Marjaryasana–Bitilasana!
मार्जर्यासन–बिटिलासन
IPA: /mɑːrd͡ʒərjɑːsən bɪtɪlɑːsən/
मार्जर्य mārjarya = macska
आसन āsana = póz / ülés
बिटिल biṭila = tehén
आसन āsana = póz
macska–tehén póz 🐈↔️🐄
∃⊣∀
+⊣×
∑⊣Π
∨⊣∧
join ⊣ meet
…
Exercise 0.22 Vegyél észre lokális⊣globális mintákat a világban.
A próbához visszatérve:
∃f : Γ ⟶ ∆
van út az egyik kontextusból a másikba
f
∃ Γ ---> ∆
Ha tudsz mutatni vagy építeni egy útat a premisszákból a konklúzióba, akkor "megmutattad", bebizonyítottad, ▮,🍋🖌, □🖊.
Még nemtudom, hogy ez csak a konstruktív logikában van-e így, vagy minden logikában. Megkérdezem a számítógépet, hátha ad valami útmutatást.
A formális szó a dolgok szerkezetére utal [Szendrei Ágnes], és ez nekem nagyon tetszett, amikor tanultam, még most is örömmel tölt el erre gondolni! Az is jó, sokszor megmosolyogtat, hogy ilyen dolgoknak tudok örülni. A formális számomra valami olyasmit jelentett, mint a formális öltözködés, valami merev, hivatalos, ilyesmi, de a matematikában más a jelentése. Sokszor van ez így a matematika tanulásban, nálam, hogy egy szó jelentése átalakul. Azthiszem ez egy képesség, aminek a mindennapi életben nagy hasznát veszem, talán mert megtanulok mindenféle dolgokat más perspektívákból nézni.
Egy mondat formalizálása, nem csak önmagában érdekes, hanem talán mert más mintákat, helyzeteket hasonlóképpen lehet formalizálni.
A kenyérpudingot 🥯 lehet recept szerint készíteni "As if handed down from the Heavens" , de ha nincs otthon briós, vagy másnéven
búzaliszt, cukor, margarin [finomított növényi zsírok változó arányban (kókusz, pálma),
ivóvíz, finomított növényi olajok változó arányban (napraforgó, pálma, repce),
emulgeálószer: zsírsavak mono- és digliceridjei; étkezési só, tartósítószerek:
szorbinsav, kálium-szorbát; savanyúságot szabályozó anyag: citromsav; aroma, színezék:
karotinok], ivóvíz, tojáslé (tojás, étkezési sav: citromsav; tartósítószer: kálium-szorbát),
sütőszer [nedvesítőszer: szorbitok; tejsavópor, búzaliszt, emulgeálószerek:
zsírsavak mono- és digliceridjei, nátrium-sztearoil-2-laktilát; tojássárgája-por, búzaglutén,
tojásfehérje-por, burgonyapehely, aroma, búzakovász (ivóvíz, búzaliszt, kovászmag /búzaliszt,
ivóvíz, baktériumtenyészet/), szőlőcukor, maltodextrin, színezék: karotinok; savanyúságot
szabályozó anyag: citromsav; stabilizátorok: nátrium-karboxi-metil-cellulóz; guargumi;
lisztkezelő szer: aszkorbinsav; enzimek], élesztő, tejkészítmény (sovány tej, édes
tejsavópor), tojáskészítmény (tojáspor, zsíros tejpor), étkezési só.
Szója, diófélék és szezámmag
Hű ez egy jó példának tűnik!
Nézd, itt a brióst, briós: A → B kinyitottuk, expanded it.
Programozásban ugyanez van:
def briós {
búzaliszt, cukor, margarin …
}
és ezt így betudod csukni, mint valami origami , vagy térkép🗺, fern🌿?
def briós {…}
és aztán meghívhatod: briós.
persze van bemenete, kimenete
def briós (be) {
… (ki)
}
és szerintem a logikában is így működnek a dolgok, mint a mákos kenyérpuddinggal! ☝️
def f (beút) {
… (kiút)
}
def út (név, be, ki) {
return név: be → ki
}
-- például:
print( út(A,B) ) -- kiírja: f: A → B
út = bizonyítás = recept = program.
Bátyjám mákos kenyérpudingot szeretett volna készíteni, mert szeret kenyérpudingot sütni, és a mákos guba hasonló étel, szóval gondolta lehetne variálni. Sajnos csak briósnak álcázott lista volt otthon hozzá, úgyhogy nem készült el.
Jaj mindig eszembe jut valami... 😭😉:
briós : Lista
Lean4-ban (Bármit megtudsz tanulni a Lean4-t is)
így írhatod a brióst, mint Lista típusú dolgot,
pl a:A, a egy A típusú dolog,
p : Prop , p itt propozíció,
variable (p q : Prop)
#check p ∧ q
#check p → q
Írd be ebbe az online fordítóba, és lefut:
kiírja p ∧ q, és p → q is propozíciók
A logika alapépítőkockáiból konstruálhatsz magadnak és másoknak saját matematikai világokat!
Azt kéne szerintem valahogy írni, hogy itt a briós : Lista, de csak akkor ehető, ha briós briós : Étel, ennek a bizonyítását az olvasóra bízzuk.
Nemtudtam hogyan kapcsoljam a logikát, és kezdek kicsit fáradni, de
talán így:
briós : Lista,
≈ b : L
≈ Lb
briós : Étel,
≈ b : É
≈ Éb
A matematikában ilyen átmenetek vannak, hogy
briós : Lista → b : L → Lb
átváltozott a kifejezés, lean4 típus perspektívából predikátumlogikába.
Nemtudom mennyire formális ez, vagy mennyire pontosan látom, de én egyelőre valahogy így látom.
Remark: Azthiszem ha
briós : Lista,b : L, akkor ittbazLbizonyítása!
A lényeg talán, hogy sokszor ezek analóg dolgok és észre lehet venni közös mintákat, "overarching themes", "underlying patterns", 🍋→🍊→🍍, ha megnézzük az absztraktabb, általánosabb mintákat, formalizálunk (?).
Például ha megérted 🐱 ⊣ 🐮, akkor talán hasonló minta ∨⊣∧, ∃⊣∀, d ⊣ ∫, 🌿⊣🌳,... és így könyebb, érdekesebb megérteni a dolgokat. Több legyet üthetsz egy csapásra! 🪰⊣🏸.
Talán ezért is hívják a matematikát az analógia elméletének, vagy a minták tudományának.
- Previous: v0.1 logika 📘🌱