Több fajta formulával is tálkozhattunk: polinomok, racionális kifejezések, logikai kifejezések. Ezek azonban közösen tárgyalhatók.
A formulák építmények. Egyszerű formulákból épülnek fel bizonyos jelek segítségével. Ezek a műveleti jelek bizonyos számú formulát képesek összefűzni, egy bonyolultabb formulává összeolvasztani.
Definíció: Egy gyökereztetett fa egy fa egy kitüntetett csúccsal, úgy nevezett gyökérrel.
Minden nem gyökér x csúcshoz hozzá lehet rendelni egy apát, ami az x-ből a gyökérhez vezető egyetlen út x utáni y csúcsa. Azt mondjuk, hogy y az x apja, x az y csúcs egy gyereke, fia. Minden összekötött csúcspár között apa-fiú viszony van és az apa, illetve fiú szerep kiosztása közöttük egyértelmű: A gyökérhez közelebbi csúcs az apa és a másik a fiú. Ezt a viszonyt fánk éleinek egy irányításával írhajuk le. Két természetes lehetőség van: (1) Minden élt irányítsunk úgy, hogy apa-végpontjából mutasson a fiú-végpontjájoz. Egy x csúcs leszármazottja egy olyan v csúcs, amelyre a fenti irányítás mellett van xv irányított út. (2) Minden élt irányítsunk úgy, hogy fiú-végpontjából mutasson az apa-végpontjájoz. Ekkor az irányított utak a gyökérbe folytathatók.
Be lehet vezetni minden csúcs generációs indexét, ami a csúcsból a gyökérbe vezető egyetlen út hossza. A gyökér generációs indexe 0, egy csúcs apjának generációs indexe a csúcs indexénél 1-gyel kisebb. Az azonos, i generációs indexszel rendelkező csúcsok alkotják az i-edik generációt. Ha két generáció sorszáma szomszédos a természetes számok között, akkor a generációkat is szomszédosaknak nevezzük. Minden él két végpontja szomszédos generációkhoz tartozik.
A gyökereztetett fák lerajzolása a következő módon szokásos. Egy generáció csúcsait egy vízszintes vonalra rajzoljuk fel. Az egyes generációk vízszintes vonalai sorszámuk szerint csökkennek (tehát a 0-adik generáció egyetlen csúcsa, a gyökér van a legfelső szinten). Minden generáción belül a csúcsok blokkokban következnek. Egy blokkot alkotnak az azonos apával rendelkező csúcsok. A blokkok sorrendje követi az előző generációban lévő apák sorrendjét.
Azokat a csúcsokat, amelyeknek nincs fia a gyökereztett fa leveleinek nevezzük. Ez az elnevezés eltér a gráfelméleti levél fogalmától, ami az 1 fokú csúcsokat jelöli. Ha a gyökérnek egyetlen leszármazottja van, akkor gráfelméleti értelmeben a gyökér levélnek számít (foka 1), míg gyökereztett fa értelemben ez a gyökér nem levél (van leszármazottja). A gyökereztett fa értelemben vett gyökerek gráfelméleti értelemben is gyökerek lesznek, kivéve azt az esetet, amikor fánk egyetlen csúcsból áll (természetesen ekkor ennek kell a gyökérnek lenni).
Egy T gyökereztetett fa minden x csúcsára az x csúcs és leszármazottjai a köztük lévő élekkel és az x csúcs kitüntetésével egy rész-gyökereztetett fát alkotnak.
Definíció: Egy gyökereztetett síkfa egy gyökereztett fa, amely minden csúcsára adott leszármazottjainak egy sorrendje.
A sík jelző onnan ered, hogy a leszármazottak sorrendjét a lerajzolás geometriájával írjuk le. Egy szülő leszármazottjait szintükön (egy vízszintes egyenesen) a sorrendjüket követve tűntetjük fel balról jobbra.
Ezen természetes gráfelméleti fogalmak bevezetése után megadhatjuk a formula definícióját.
Definíció: Formulák definíciójához le kell rögzítenünk egy változó/határozatlan halmazt V-t és műveleti jelek egy J halmazát egy a: J -> N aritás függvénnyel. Definiálnunk kell az elemi formulákat. Ez általában V elemei, azaz a változók, de gyakran úgy nevezett konstansok is azok lesznek. A formula ezekután egy bináris síkfa, amely minden csúcsához hozzárendelünk valamit. Levélcsúcsokhoz hozzárendelt objektum egy elemi formula. Nem levél csúcsokhoz hozzárendelt objektum egy műveleti jel, amelytől megkívánjuk, hogy aritása egyezzen meg a csúcs gyerekeinek számával.
Megjegyzés: A definicióban szerepel a konstans fogalom. Ezeket szokás a jelek halmazába belefoglalni. A jelek segítségével rakunk össze egyszerűbb formulákból egy bonyolultabbat. Az aritás mondja meg, hogy egy jel hány formula összefűzésére használható. Ha a konstansokat jeleknek fogjuk fel, akkor ezek 0 aritású jelek lesznek.
Formuláknak néhány természetes paramétere van. Az első az alap gyökereztetett fa csúcsainak száma. Egy másik természets paraméter a levelek száma. Végül megemlítjük a mélységet, ami a leghosszabb levél-gyökér út hossza.
Minden csúcs definiál egy rész-gyökereztetett fát, ami egy formula. Ezeket a formulákat nevezzük eredeti formulánk részformuláinak. A gyökér leszármazottjai mind egy-egy részformulának felel meg. A teljes formula ezeket a részformulákat fűzi össze egy formuláva a gyökérhez írt műveleti jel segítségével. Ennek az ``összefűzési folyamatnak'' a teljes, szemléletes leírása a fent definiált fogalom.
Példa: Példa egy logikai formulára. Vegyük a következő logikai jelhalmazt: J={¬,^,V}, ahol ¬ a negáció/tagadás/nem/NOT jele, ^ a konjunkció/és/AND jele, V pedig a diszjunkció/vagy/OR logikai jel. A negáció aritása 1, az konjukció és diszjunkció aritása 2.
Példa: Példa egy aritmetikai formulára. Vegyük a következő aritmetikai jelhalmazt: J={-,+,.,/} ahol - az ellentett képzés jele, +,/ és . a szokásos alapműveleti jelek. Az ellentett képzés aritása 1, az alapműveletek aritása 2.
Példa: Példa egy elemi függvényre, mint analízibeli formulára. Vegyük a következő analízisben használatos jelhalmazt: J={+,.,sin,exp}. Az aritások értelemszerűek.
A formulák klasszikus leírása egy jelsorozatként történik. Ezt a szemléletet is formalizáljuk.
Definíció: Formulák definíciójához le kell rögzítenünk egy változó/határozatlan halmazt V-t és műveleti jelek egy J halmazát egy a: J -> N aritás függvénnyel. A formulák a J U V U {(,),,} ábc feletti véges jelsorozatok/szavak F halmazát alkotják. Erről a halmazról a következő tulajdonságokat elvárjuk:
Megjegyzés: Definíciónk első két elvárása azt mondja, hogy bizonyos jelsorozatok automatikusan formulák is egyben. Ezeket elemi formuláknak nevezzük. A további tulajdonságok olyan képzési formákat írnak le, amelyek formulákból formulákat gyártanak. Definíciónk utolsó kitételét úgy is megfogalmazhatjuk, hogy csak az elemi formulákból a definícióban leírt módon gyártott jelsorozatok lesznek formulák. Azaz minden formulához tartozik egy ``gyártási folyamat''.
Definíció: Legyen ƒ0=V U J0. Ha ƒk jelsorozatok egy halmazát definiáltuk, akkor ƒk+1-et definiáljuk úgy, hogy ƒk elemei mellé bevesszük a j(f) jelsorozatokat, ahol j egy 1 aritásu eleme J-nek, f pedig ƒk egy eleme, továbbá bevesszük az (f)j(g) alakú jelsorozatokat, ahol j egy 2 aritású eleme J-nek f ésg pedig ƒk-ból való, továbbá bevesszük a j(f1, f2, ..., fk) jelsorozatokat is, ahol f1, f2,..., fk jelsorozatok ƒk elemei, míg j egy k aritásu eleme J-nek. Legyen ƒ az összes ƒi (i=1,2,3,...) uniója.
Könnyen ellenőizhető, hogy a ƒ halmazt minden a formulák definiációjában szereplő tulajdonságokkal rendelkező halmaz tartalmaz, sőt ő maga is rendelkezik az elvárt tulajdonságokkal. Így ƒ=F. Ha f a ƒ=F halmaz egy eleme, akkor valamely i természetes számra f a ƒi halmazhoz tartozik. Ekkor azt mondhatjuk, hogy f i lépésben legyártható.
A definícióban nagyon lényegesek a zárójelek. Ha kihagynánk azokat, akkor formulánk olvasata nem lenne egyértelmű. Mit értünk ez alatt? Egy formulát olvasva, akkor értjük meg igazán, ha a mögöttes gyártási folyamatot is látjuk. Ezt a zárójeles kódolás során visszafejhetjük. A zárójel nélküli kódolás esetén ez nem tehető meg. Ennek ellenére zárójelekkel lehet és szokásos is spórolni. Megállapodásokkal csökkenthetjük a szükséges zárójelek számát. Ennek az szab határt, hogy az ``olvashatósághoz'' ragaszkodnunk kell. Létezik egy úgy nevezett lengyel jelölés, amley teljesen kiküszöböli (az egyértemű olvashatóság mellett) a zárójelek használatát. A jelölés nem terjedt el, a hagyományos zárójeles kódolást megtanulók számára természetellenes. Azaz formulák olvasása azt jelenti, hogy az előző fákkal történő kódolásra át lehet térni. Fordított irányban ez triviális. Ha egy fa-diagrammal írunk le egy formulát, akkor klasszikus előállítása nagyon egyszerű. A programozást szerető hallgatók írhatnak programot a kétféle leírás közötti konverziókra.
Az előző megjegyzés rendkívül fontos. A formulák klasszikus leírása esetén az olvashatóság/a gyártási folyamat visszafejthetősége sok évi matematikai munka tapasztalata. Eddigi munkánk során nem merült fel, hogy ezt a tényt megkérdőjelezzük, bizonyítani próbáljuk. Logika előadásunk első ténykezdése ennek a fenti megjegyzésnek a bizonyítása. Ehhez jelsorozatunkból kiemeljük a zárójelek részsorozatát. Megnézzük milyen zárójel-sorozatokat kaphatunk meg így és az egyes nyitó-csukó zárójel-párok hogyan azonosíthatók.
Definíció: Egy sorozatban x,x',y és y' négy elem. Azt mondjuk, hogy az xx' pár keresztezi az yy' párt, ha y és y' közül pontosan egy van a sorozat x és x' közötti
Megjegyzés: Egy sorozat két eleme definiál egy intervallumot. A nem kereszteződés éppen azt jelenti, hogy a két intervallum diszjunkt, vagy egyik tartalmazza a másikat.
Lemma: Legyen s egy zárójel-sorozat. A következők ekvivalensek:
Definíció: Egy zárójelsorozatot szabályosnak nevezzük, ha a fenti lemma egyik/bármelyik tulajdonságával rendelkezik.
Lemma: Ha egy klasszikusan kódolt formula jelsorozatából kiemeljük a zárójelek részsorozatát, akkor szabályos zárójelsorozatot kapunk.
Bizonyítás: A lemmában szereplő első tulajdonságot ellenőrizzük a formula előállítása szerinti indukcióval. Az elemi formulákban nem szerepel zárójel, azaz zárójel-sorozata üres, az üres zárójel-sorozat pedig szabályos. Ha f egyszerűbb formulákból van összerakva, akkor feltesszük, hogy az egyszerűbb formulákban szereplő zárójeleket párosíthatjuk. j(f), (f)j(G), illetve j(f1,f2,...,fk)-ban szereplő zárójelek párosításánál az összetevőkön belüli árokat meghagyjuk, míg az új (a fenti leírásban látható) zárójeleket természetes módon pároítjuk. Így egy jó pároiátást kapunk. j(f) zárójel
Lemma: Legyen z egy szabályos zárójelsorozat. Ekkor az előző lemma első pontjában szereplő párosítás egyértelmű.