Deduktívne systémy
- mnozina schém axióm
- mnozina odvodzovacích (inferencných) pravidiel
formula p je dokázatelná (zapisujeme ?p), ak pre nu existuje dôkaz, t.j. konecná postupnost formúl taká, ze na jej konci je p a kazdá formula v nej je bud prípad axiómy alebo vyplýva z predchádzajúcich pouzitím nejakého odvodzovacieho pravidla
Schémy axióm:
tautológie propozicnej logiky (Ax1)
EFp ? E(true ? p) (Ax2)
AGp ? ?EF?p (Ax2’)
AFp ? A(true ? p) (Ax3)
EGp ? ?AF?p (Ax3’)
EX(p ? q) ? EXp ? EXq (Ax4)
AXp ? ?EX?p (Ax5)
E(p ? q) ? q ? (p ? EXE(p ? q)) (Ax6)
A(p ? q) ? q ? (p ? AXA(p ? q)) (Ax7)
EX true ? AX true (Ax8)
AG(r ? (?q ? EXr)) ? (r ? ?A(p ? q)) (Ax9)
AG(r ? (?q ? EXr)) ? (r ? ?AFq) (Ax9’)
AG(r ? (?q ? (p ? AXr))) ? (r ? ?E(p ? q)) (Ax10)
AG(r ? (?q ? AXr)) ? (r ? ?EFq) (Ax10’)
AG(p ? q) ? (EXp ? EXq) (Ax11)