Odporucam precitat sekciu 1.1 Predbeznosti z http://blackhole.sk/~kabel/doc/logika.pdf
(to su minulorocne Mlckove skripta). Viem ze sa to cita tazko a clovek sa zlakne tych nakope
nahadzanych nealfanumerickych znakov, ale je to zaujimave. (A nie len precitat ale aj nad tym
posediet a pochopit to).

Dalsi zdroj: http://en.wikipedia.org/wiki/First-order_logic

Motivacia:
  automaticke dokazovanie viet   http://en.wikipedia.org/wiki/Automated_theorem_proving

  KLEE (o tomto si nie som isty, ale myslim ze pouziva logicke odvodzovacie pravidla a
  poznatky z logiky, a kedze to naslo v 20 rokov starych unixovyh utilitach bezpecnostne
  chyby, formalnym dokazovanim, vsetci budu suhlasit, ze je logika pouzitelna v praxi)
                                 http://ccadar.github.io/klee/

  databazy (dotazy), trebars temporalna databaza pouziva dotazy v temporalnej logike

  a celkovo teoria formalneho dokazovania, ako chcete nieco dokazovat ked nemate
  axiomatizovany sposob dokazovania? Pretoze ten intuitivny je sporny, podobne ako je
  dokazatelne hocico v nainvnej teorii mnozin (Russelov paradox)

(Chceme system dokazovania, ktory by sme mohli naprogramovat, nejake syntakticne transformacie
formuli, ktore su logicky korektne.)

Jazyk predikatove logiky obsahuje:
  - premenne (mnozina Var)
  - spojky ¬, →, a potom z nich odvodene ∧, ∨, ↔
  - pomocne symboly: zatvorka (, ),  ciarka ,
  - kvantifikator ∀, ∃
  - signatura: mimologicke symboly
         R … mnozina relacnych symbolov
         F … mnozina funkcnych symbolov
     plus funkcie urcujure aritu (kolko premennych sa rve do daneho relacneho (funkcneho)
     symbolu):
         Ar_R: R → ℕ₀
         Ar_F: F → ℕ₀                      (podciarka F znamena, ze F je v dolnom indexe)

     napriklad F = {f, g, c} kde f je jednej premennej, g dvoch a c je konstanta, potom
         Ar_F(f) = 1, Ar_F(g) = 2, Ar_F(c) = 0

(Pozorovanie: funkcne symboly su vlastne relacne symboly s jednou premennou navyse, trebars
f(x) = y mozme zmenit na relacny symbol f(x,y).)

Rozlisujeme jazyk s rovnostou a bez rovnosti. Rovnost je binarny relacny symbol =, ktory sa
neudava do mnoziny R a pre ktory platia axiomy rovnosti:
  1. reflexivita: pre vsetky premenne x
       x = x
  2. substitucia pre funkcie: pre vsetky premenne x, y a hocijaky funkcny symbol f
       x = y → f(…, x, …) = f(…, y, …)
  3. substitucia pre formule: pre vsetky premenne x, y a hocijaku formulu φ(x), ak φ' je
     vytvorena z φ nahradenim vsetkych volnych vyskytov x vo φ za y, a vsetky tieto nahradene
     vyskyty zostavaju volne, potom
       x = y → (φ → φ')
(Toto v skutocnosti nie su axiomy, ale schemy axiomov, kazda z nich specifikuje nekonecne
vela axiomov.)
Symetria (x = y → y = x) a tranzitivita (x = y ∧ y = z → x = z) plynu z tychto axiomov.

Ak mame jazyk bez rovnosti a chceme rovnost, musime = pridat do R a do teorie narvat tieto
axiomy. (Zo Simonovej teorie mnozin: v logike su dve prvky rovne, ked pre ne platia tie iste
formule.) Takto mozme za = dosadit hociktoru ekvivalenciu na nosnej mnozine (tj. hociktoru
binarnu relaciu, ktora je ekvivalencia), ak splna axiomy rovnosti.

Realizacia funkcneho (relacneho) symbolu na nosnej mnozine (univerze) U
Zatial nevieme, naco sa dany funkcny symbol pre dane argumenty zobrazi. To ani vediet nemozeme,
pretoze v cistom jazyku hovorime iba o tom, ako sa funknce (relacne) symboly volaju (f, g)
a aku maju aritu (kolko sa do nich rve premennych). A pokial nemam nosnu mnozinu (ktoru
v jazyku nemame, pretoze to je iba jazyk), tak to vediet ani nemozme (naco sa co zobrazi).
Ak mame univerzum U, potom:

  f ∈ F     f^U (U je v hornom indexe) je (nejaka) realizacia funknceho symbolu f na mnozine U
            f^U: U^Ar_F(f) → U

            ak teda f je binarny symbol (Ar_F(f) = 2), potom f^U: U² → U je nejaka funkcia,
            ktora zobrazuje UxU na U.

  r ∈ R     r^U (U je v hornom indexe) je (nejaka) realizacia relacneho symbolu r na mnozine U
            r^U ⊆ U^Ar_R(r)

            ak teda r je binarny relacny symbol (Ar_R(r) = 2), potom r^U je nejaka podmnozina
            U², teda relacia na U×U

            Kedze U⁰ = {Ø} je jednoprvkova mnozina obsahujuca prazdnu mnozinu, existuju iba dve
            realizacie nularneho relacneho symbolu (2 podmnoziny mnoziny {Ø}), a to su Ø a {Ø}.
            Realizacia nularneho relacneho symbolu je teda prvovyrok.

            Poznamka:
            Ak ste citali predbeznosti, tak ste sa docitali o induktivnej definicii mnoziny
            prirodzenych cisel ℕ v teorii mnozin, teda ze cislo 0 definujeme ako prazdnu
            mnozinu Ø, a potom n = {0, 1, 2, …, n-1}. Teda
              0 = Ø
              1 = {0} = {Ø}
              2 = {0, 1} = {Ø, {Ø}}
              3 = {0, 1, 2} = {Ø, {Ø}, {Ø, {Ø}}}
              …
            V tomto ponimani realizaciu relacneho symbolu mozme chapat aj ako funkciu, ktora
            zobrazuje na {false, true} = {0, 1} = 2.

Struktura
Mame jazyk L s nejakymi funkcnymi a relacnymi symbolmy. Ak k tomuto jazyku pridame nosnu mnozinu
(univerzum) a nejako realizujeme vsetky funkcne a relacne symboly, dostaneme strukturu jazyka L.

Teoria je nejaka mnozina formuli.
Model teorie T je taka struktura, ze v nej platia vsetky formule teorie T.

Vyrokova logika je predikatova logika bez rovnosti obsahujuca iba nularne relacne symboly
(prvovyroky) a ziadne funkcne symboly. Nezavisi na nosnej mnozine, pretoze prvky nie je
ako pouzit.

Zakladne axiomy logiky (Hilbertovskeho kalkulu):
  Pre hocijake formule φ, ψ, χ plati:

  HK1: φ → (ψ → φ)
  HK2: (¬φ → ¬ψ) → (ψ → φ)
  HK3: (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))

V skutocnosti su to zase schemy axiomov. Mohli by byt, samozrejme, ekvivalentne vybrane
aj inak, toto je zrejme najlepsia verzia (nie prilis dlha a je korektna, nevedie k sporom a
zachovava modely).

Pravidlo modus ponens (MP):
  ak vieme, ze plati φ a (φ → ψ), potom plati ψ.

Zatial vsetko, so long.