|
|
Aksiome i važnije teoreme kvantifikatorskog računa
Aksiome:
Ax1. A=>(B=>A)
Ax2. (A=>(B=>C))=>((A=>B)=>(A=>C))
Ax3. ('not'A=> 'not'B)=>(B=>A)
Ax4. ( 'za svako'x )A(x)=>A(t), term t je slobodan za x u A(x)
Ax5. ( 'za svako'x )(A=>B)=>(A=>( 'za svako'x )B) x nije slobodna promenljiva u A gde su A,B,C bilo koje formule računa K
Pravila iyvodjenja računa K:
(MP) Iz A i A=>B sledi B
(GEN) Iz A sledi ( 'za svako'x )A, gde je x promenljiva.
S obzirom da su u ra;unu K prisutne aksiome Ax1,Ax2,Ax3 i pravilo izvodjenja (MP) iskaznog računa, jedan broj teorema računa K dobija se iz teorema iskznog računa L zmenom iskaznih slova nekim formulama računa K. Takve teoreme računa K zovu se izvodi odgovarajućih teorema računa L.
Postoje teoreme računa K koje nisu izvodi teorema računa L. Takve su, na primer:
( 'za svako'x )( 'za svako'y )A<=>( 'za svako'y )( 'za svako'x )A
( 'za svako'x )A=>( 'postoji'x)A
('za svako'x)(A'i'B)<=>('za svako'x)A'i'('za svako'x)B
('za svako'x)AV('za svako'x)B=>('za svako'x)(AVB)
A(t)=>('postoji'x)A(x) t je slobodan ya x u A
('postoji'x)('za svako'y)A=>('za svako'y)('postoji'x)A
(('za svako'x)(B=>C)'i'('za svako'x)(A=>B))=>('za svako'x)(A=>C)
((('za svako'x)(C=>B)'i'('za svako'x)(C=>A))'i'('postoji'x)C)=>('postoji'x)(A'i'B)