24 Naturlig deduksjon Flashcards
utledninger og bevis
Mengden av utledninger (eng: derivations) i naturlig deduksjon er induktivt definert. Basismengden består av mengde av alle utsagnslogiske formler, og det er ett induksjonssteg for hver regel. Hver regel forteller hvordan en ny utledning kan konstrueres fra én eller to mindre utledninger. Et bevis (eng: proof) for en formel F er en utledning hvor F er konklusjonen og hvor alle antakelser er lukkede. En formel er bevisbar (eng: provable) hvis det finnes et bevis for den.
sunnhet og kompletthet
En kalkyle er sunnhet (eng sound) hvis enhver bevisbar formel i kalkylen er gyldig. En kalkyle er komplett (eng: complete) hvis enhver gyldig formel er bevisbar i kalkylen.
utledbarhet
La M være en mengde formler. Vi sier at en formel F er utledbar (eng: derivable) og at den kan utledes fra M, hvis det finnes en utledning av F hvor alle de åpne antakelsene er formler i M. Vi skriver i så fall M |- F, og vi skriver |- F hvis det finnes et bevis for F.
konsistent teori
En mengde formler er konsistent hvis det ikke er mulig å utlede både en formel og dens negasjon fra den.
Utledning av motsigelsesbevis (RAA)
[¬ F] … ⊥ - - (RAA) F
