|
|
Specijalni kvantifikatorski računi - formalizacija problema
Aksiome Ax1.-Ax5. Računa K su logičke aksiome. Dodavanjem odredjenog broja formula računa K, koje nisu ni logičke aksiome ni teoreme računa K, odbijamo novi logički sistem specijalni kvantifikatorski račun . Formule koje priključujemo logičkim aksiomama zovemo sopstvene (specijalne) aksiome . U zavisnosti od izbora sopstvenih aksiom dobijaju se različiti specijalni specijalni kvantifikatorski računi. Svaki specijalni kvantifikatorski račun ima odrdjene skupove konstanti, funkcijskih simbola koji su podskupovi odgovarajućih skupova simbola računa K. Teoreme specijalnog kvantifikatorskog računa su sve formule koje su izvodjene iz skupa logičkih i sopstvenih aksioma po pravilima izvodjenja računa K. Na osnovu deduktivne jednakosti formula možemo pretpostaviti da su sve sopstvene aksiome zatvorene formule.Kako je svako izvodjenje konačan niz u kojem za svaku teoremu A učestvuje konačan broj sopstvenih aksioma [A1,A2,...,An] C_(podskup)Ax(S) važi:
Ax(S) |-k-A <--->{A1,.....,Ak} |-k-A
<--->|-k- (A1 'i'A2'i'...'i'Ak)=>A
Svakoj teoremi A specijalnog računa S odgovara jedna odredjena teorema računa K. Teorema računa S je tačna samo u onim interpretacijama u kojima su tačne sve sopstvene aksiome računa S. Model računa S je ona interpretacija pri kojoj su tačne specijalne aksiome računa S. Značaj uvodjenja specijalnih kvantifikatorskih računa je u nastojanju da se formalizuju neke posebne, sadržajne teorije.