Skip to main content
Process journal of learning by Attila Vajda

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:

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 : Listab : 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 itt b az L bizonyí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.