Teorija

Iz MaFiRaWiki


V logiki teorija opisuje matematično strukturo, kot sta grupa in projektivna geometrija, ali matematično teorijo, kot sta teorija množic in teorija kategorij. Sama teorija zaobjema le osnovne pojme in aksiome, iz katerih izpeljemo še ostale pojme in dokažemo nove izreke teorije.

Teorijo sestavljajo:

  • osnovni pojmi, o katerih govori teorija. Vsaka vrsta pojma tvori sorto ali tip. Nekatere teorije imajo en sam osnovni pojem in zato eno samo sorto, v drugih pa sorte tvorijo bogato strukturo, ki jo opišemo s primerno teorijo tipov.
  • osnovne konstante, operacije in relacije določajo konstrukcije in razmerja med osnovnimi pojmi. Vsaka osnovna konstanta pripada eni od sort teorije, vsaka osnovna operacija in relacija pa ima signaturo, ki določa njeno domeno in kodomeno.
  • aksiomi so izjave o osnovnih pojmih, konstantah, operacijah in relacijah.

Teorije ločimo glede na vrsto logike, v kateri jo izrazimo, na primer:

Osnovni pojmi teorije so v nekem smislu nedefinirani, saj jih ne opišemo neposredno, ampak z aksiomi opišemo njihove značilnosti. Šele ko govorimo o modelu teorije, osnovne pojme natančno opredelimo in definiramo, kaj so. Seveda pa imajo lahko osnovni pojmi v različnih modelih različen pomen. Pogosto se izkaže, da ima teorija, ki je bila sprva mišljena kot opis neke matematične strukture, tudi druge, nepričakovane modele.


Zgledi

Teorija naravnih števil

  • osnovni pojem: naravno število
  • osnovne konstante, operacije in relacije: konstanta 0, enomestna operacija naslednik S
  • aksiomi: Peanovi aksiomi

Teorija množic

Teorija digrafa

  • osnovna pojma: vozlišče in lok
  • osnovni operaciji: operaciji začetek in konec loka, ki loku priredita vozlišči
  • aksiomi: ta teorija nima nobenih aksiomov

Teorija enostavnega grafa

  • osnovna pojma: vozlišče in polpovezava
  • osnovni operaciji: operacija začetek polpovezave i, ki polpovezavi priredi vozlišče, in operacija nasprotna polpovezava o, ki polpovezavi priredi polpovezavo
  • aksiomi: za vsaki polpovezavi p,q velja:
    • o(p)) \neq p
    • o(o(p)) = p
    • i(p) = i(q) \land i(o(p)) = i(o(q)) \implies p = q (največ ena povezava med vozliščema)
    • i(p) \neq i(o(p)) (ni zank)
Osebna orodja