Elsőrendű logika

Nulladrendű állítás

• Konkrét elemről konkrét állítást mond ki
• Egyszerű kijelentő mondatok elegendőek
• Egyértelműen eldőnthető hogy igaz vagy hamis

Egyedekkel is jelölhető, ezek Paraméteres Állítások

Elsődrendű állítás

• Akkor elsőrendű, ha az alanyunk egy halmaz
• Az állítás az összes elemére egyidejüleg fennáló megállíptás vagy a halmaz bizonyos elemeire fenálló megállapítás
• Leírásukhoz kvantorokat ($ \forall ,\exist $) használjuk.

Elsődrendű állítás - Példa

• \(\forall x : E(x)\)
  • Mindem eleme...
• \(\exist x : P(x)\)
  • Létezik olyan...

Matematikai struktúra

A matematikai struktúra egy \(\left<U,R,M,K\right>\) halmaznégyes, ahol:

• U: Értelmezési tartomány
  • Nem üres halmaz (\(\neq\empty\))
  • Ha U egyfajtájú elemekből áll
• R: Alaprelációk halmaza
  • az U-n - értelmezett n-változós (\(n=1,2,\dots,k\)) logikai függvények halmaza
• M: Alapműveletek
  • az U-n értelmezett n változós (\(n=1,2,\dots,k\)) matematikai függvények halmaza
• K: az U megjelölt elemeinek egy (esetleg üres) részhalmaza ($ U \subseteq K$)

Struktúra szignatúrája: (\(v_1, v_2, v_3\) egész értékű fgv. együttes) megadja a kifejetés (az alaprelációk és alapműveletek) aritását, és annak \(K\) elemszámát.

Matematikai struktúra leírónyelve

• R alaprelációk nevei
• M alapműveletek nevei
• K elemek nevei

Ezekkel a nevekkel már lehet egyszerű nulladrendű és paraméteres állításokat leírni.

(R,M,K \(\rightarrow\) Logikán kívűli részek)

Logikai szimbólumok

• Individuumváltozók (a, b)
• Unér és binér logikai műveletek
  • \(\neg\)
  • \(\land\)
  • \(\lor\)
  • \(\supset\)
• kvantor $ \forall,\exists $
• elválasztó jelek $\left(\space\right) $

Struktúra szignatúra

alaprelációk és alapműveletek árításai (paraméter-számosság)

Felsorolásával:

Utalás a program függvényeinek monadikus, diadikus és poliadikus jellegére

Formalizálás - Példa

$ x \leq y =_{def} \space \exists z((x+z)=y)$

\(R: U_p \cup U_e \cup U_s\)

Struktúra: \(\left<U_p \cup U_e \cup U_s, R, M, K \right>\)

Struktúra szignatúra - Felépítés

• \(Pr\) Predikátumszimbólumok
  • \(v_1\): \(P \in Pr\)-re megadja \(P\) aritását ( k )
• \(Fn\) függvényszimbólumok halmaza
  • \(v_2: f \in Fn\)-re megadja f aritását (\(k\))
• \(Cnst\): konstansszimbólumok halamaza
  • \(v_3\): megadja a konstansok számát

Több fajtájú univerzum esetén: \(\left< Srt, Pr, Fn, Cnts \right>\)

• \(Srt\): nem üres halmaz, melynek \(\pi_j\) elemei fajtákat szimpolizálnak
• \(Pr: P \in Pr\)-re megadja \(P\) aritását ( k ) és hogy milyen fajtájuak az egyes argumentumok (\(\pi_1, \pi_2, \dots, \pi_k\))
• \(Fn\) függvényszimbólumok halmaza és hogy milyen fajtájúak az egyes argumentumok, valamit a függvény értéke. \(\left(\pi_1, \pi_2, \dots, \pi_k \right)\)
• \(Cnts\): Konstansszimbólumok halmaza
  • \(v_{3}\) megadja minden fajtához a konstansok számát

Nyelv kifejezései

Informális kifejezés

• termek:
  • Matematikai leképzéseket szimoblizálják
• formulák:
  • Logikai leképezéseket szimbolizálják

Olyan leképzés aminek eredménye univerzum beli elem

Termek

Egyfajtájú eset

\(ℒ V_{v}\)

• Alaplépés
  • Minden individuumváltozó és konstans szimbólum természetes
• Rekurzív lépés
  • Ha az $ f \in F_n \space k$ -változós függvényszimbólum és \(t_1, t_2,...,t_k\) termek, akkor \(f(t_1, t_2,...,t_k)\) is terem
• Minden terem az 1, 2 szabályok véges sokszori alkalmazásával áll elő

példa elsőrendű formulára: \(\forall z \space (P( \overline{a} ) \supset Q(x,y))\)

Többfajtájú eset

\(ℒ_{t} V_{v}\)

• Alaplépés
  • Minden \(\pi \in Srt\) fajtájú individuumváltozó és konstans szimbólum \(\pi\) fajtájú term
• Rekurzív lépés
  • Ha az $ f \in F_n \space k$ -változós függvényszimbólum és \(t_1, t_2,...,t_k\) termek, akkor \(f(t_1, t_2,...,t_k)\) is terem
• Minden terem az 1, 2 szabályok véges sokszori alkalmazásával áll elő

Kapcsolódó fogalmak

Priorítási sorrend \(\forall, \exists, \neg, \land, \lor, \supset\)

Definiált:

• Zárójelelhagyás
• Műveletek és kvantorok hatásköre
• Komponens és prímkomponens fogalma
• Egy formula fő műveleti jele

A prímkomponesek alapján eldőnthető a teljes formula

\(\underline{\forall x P(x)} \supset (\underline{Q(y)} \land \underline{\forall z (P(z)\lor Q(z))})\)
\(i \supset (h \land i) = i \supset h = h\)

Közvetlen részterm

Konstansnak és individuumváltozónak nincs közvetlen résztermje

Közvetlen részformula

Prímkomponensek

Term szerkezeti fája

Egy t term szerkezeti fája ehy olyan véges fa, meyre teljesül, hogy:

• a gyökérhez a t term van rendelve
• ha valamelyik csúcsához egy t' term van rendeve akkor az adott csúcs gyerekeihez a t' formula közvetlen résztermjei vannak rendelve
• Leveleihez individuumváltozók vagy konstansok vannak rendelve

Formula szerkezeti fája

• A gyökeréhez az F formula van rendelve
• Ha valamelyik csúcsához az F' formula van rendeve akkor az adott csúcs gyerekeihez az F' formula közvetlen részformulái vannak rendelve
• Leveleihez atomi formulák vanna rendelve

Változók elsőrendű logikában

• Szabad
  • Nem esik \(x\)-re vonatkpozó kvantor hatáskörébe
• Kötött
  • Az \(x\)-re vonatkozó kvantor hatáskörébe esik

Formulában:

• Kötött
  • \(x\) Minden előfordulása kötött
• Szabad
  • \(x\) Minden előfordulása szabad
• Vegyes
  • \(x\) Minden előfordulása változó

Megjegyzés: Egy kötött változó átnevezhető a formulában elő nem forduló változó névre, és így is ekvivalens marad a két formula. Ez által a vegyes változók eltüntethetőek.

$ \forall x P(x) \supset \exists yQ(w, y) \lor P(v) \supset \forall z Q(w, z)$

Zártság

Formula:

• Zárt
  • Minden változója kötött
• Nyitott
  • Legalább egy individuumváltozónak van egy szabad előfordulása
• Kvantormentes
  • Nem tartalmaz kvantort

Az elsőrendű állítások az adott nyelv zárt formulái (más néven mondatok)

Alapkifejtés

Alapkifejtés - a változót nem tartalmazó \(ℒ\) kifejezés (alapformula, alapterm).

Ezek alappéldányok

Atomi formulák allapéldányai:

• Alapatom
  • Az argumentumai konstans szimbólumok vagy egy megadott univerzum elemei
  • pl.: \(P(c)\)
• Alappéldány
  • ha argumentumai alaptermek
  • pl.: \(Q(f(a,b),a)\)

Egy atomi formula tulajdonképpen paraméteres állítás.

Interpretáció

\(I= \left< I_{Srt}, ~ I_{Pr}, ~ I_{Fn}, ~ I_{Cnst} \right>\)

Termek Szemantikája

\(|c|^{I,\kappa}\)