24 Naturlig deduksjon Flashcards
24.1 Utledninger og bevis
Mengden av utledninger 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 for en formel F er en utledning hvor F er konklusjonen og hvor alle antakelser er lukkede. En formel er bevisbar hvis det finnes et bevis for den.
24.2 Sunnhet og kompletthet
En kalkyle er sunn hvis enhver bevisbar formel i kalkylen er gyldig. En kalkyle er komplett hvis enhver gyldig formel er bevisbar i kalkylen.
24.3 Utledbarhet
La M være en mengde formler. Vi sier at en formel F er utledbar 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.
23.4 Konsistent teori
En mengde formler er konsistent hvis det ikke er mulig å utlede både en formel og dens negasjon fra den.
