Wikisida: Én sideversjon ble importert

2026-09-03T06:31:56Z

Én sideversjon ble importert

← Eldre sideversjon	Sideversjonen fra 3. sep. 2026 kl. 06:31
(Ingen forskjell)

nb>4ingBot: genitivsapostrof etter s, x og z using AWB

2022-11-10T19:19:02Z

genitivsapostrof etter s, x og z using AWB

Ny side

'''Naturlig deduksjon''' kan i [[logikk]] og [[bevisteori]] referere til både [[Gerhard Gentzen]]s og [[Jan Łukasiewicz]]' opprinnelige logiske kalkyler, eller til den generelle presentasjonen av logiske systemer som de innførte.
Før introduksjonen av naturlig deduksjon var logiske systemer basert på en mengde aksiomer og noen få regler, kjent som Hilbert systemer.
I artikkelen hvor Gentzen presenterer sin naturlig deduksjons-system, uttrykker han et ønske om at bevisene skal ligne hvordan ''matematiske'' bevis ser ut, og han identifiserer ressonering fra ''antagelser'' som et viktig
aspekt. I naturlig deduksjon er det ingen aksiomer, men derimot flere ressonerings-regler, sammen med hypotetiske antagelser.

== Gentzens naturlige deduksjon, NJ ==
Gentzen definerte først systemet NJ, som er en sunn og komplett logisk kalkyle for førsteordens intuitionistisk predikatlogikk.
Termer og formlene for det logiske systemet er definert som, hvor konstanter <math>c</math>, funksjonssymoboler <math>f</math> og
relasjonssymboler <math>R</math> er bestemt av et [[førsteordens språk]]:
:<math> t, s ::= x \mid c \mid f(t_1, \ldots, t_n) </math>

:<math> A, B, F ::= \top \mid \bot \mid R(t_1, \ldots, t_n) \mid A \land B \mid A \lor B \mid A \supset B \mid \forall x.\, A \mid \exists x. \, A </math>

Se artikkelen [[førsteordens logikk]] for mer informasjon om formler og termer.
I naturlig deduksjon er det vanlig å la negasjon være et definert konnektiv: <math> \neg A \equiv A \supset \bot</math>.

{| class="wikitable" style="width: 60%;"
|-
! Konnektiv !! Introduksjon !! Eliminasjon
|-
| <math>\top</math>
|| <math> {} \over \vdash \top </math>
|| ingen
|-
| <math>\bot</math>
|| ingen
|| <math> \vdash \bot \over \vdash A </math>
|-
| <math>\land</math>
|| <math>\vdash A \quad \vdash B \over \vdash A \land B </math>
|| <math> \vdash A \land B \over \vdash A</math> <math> \vdash A \land B \over \vdash B</math>
|-
| <math>\lor</math>
|| <math> \vdash A \over \vdash A \lor B </math> <math>\vdash B \over \vdash A \lor B</math>
|| <math> \cfrac{ \begin{matrix}
& \overline{\vdash A} & \overline{\vdash B} \\
& \vdots & \vdots \\
\vdash A \lor B & \vdash C & \vdash C
\end{matrix}
}{\vdash C} </math>
|-
| <math>\supset</math>
|| <math> \begin{matrix}
\overline{\vdash A} \\
\vdots \\
\vdash B \\
\overline{\vdash A \supset B }
\end{matrix}
</math>
|| <math> \vdash A \quad \vdash A \supset B \over \vdash B </math>
|-
| <math>\forall</math>
|| <math> {\vdash A \over \vdash \forall x.\, A}* </math>
|| <math> \vdash \forall x.\; A \over \vdash A[t / x] </math>
|-
| <math> \exists </math>
|| <math> \vdash A[t/x] \over \vdash \exists x.\, A </math>
|| <math> { \begin{matrix}
& \overline{\vdash A} \\
& \vdots \\
\exists x.\, A & C \\
\end{matrix}
\over \vdash C}*
</math>
|}
med følgende begrensinger på utledningene: <math>*</math> variabelen <math>x</math> kan ikke forekomme fritt i en åpen antagelse som denne utledningen avhenger av, og
i tilfellet med eliminasjon av <math>\exists</math>, så kan ikke <math>x</math> forekomme i <math>C</math>.

=== Konsistent ===
Gentzens naturlig deduksjon, NJ, er konsistent, i den forstand at det ikke finnes noen derivasjon for <math>\vdash \bot</math> fra ingen antagelser.

Da Gentzen publiserte NJ, greide han ikke å bevise at NJ er konsistent, og han konstruerte derfor en annen kalkyle LJ, [[sekventkalkyle]], som han beviste
var logisk ekvivalent med NJ, og som han beviste var konsistent. I ettertid har konsistensen til NJ blitt bevist direkte, ved å ''normalisere'' bevis, som har en tett sammenheng
med å [[Typeteori#Normalform|redusere typede lambdatermer]], gjennom [[Curry-Howard korrespondansen]].

== Gentzens naturlig deduksjon, NK ==
Samtidig som Gentzen presenterte NJ presenterte han også NK, som er nøyaktig som NJ, men med en ekstra regel, som tilsvarer ''motsigelsesbevis'':

:<math> {\begin{matrix}
\vdash \neg A \\
\vdots \\
\vdash \bot \end{matrix}} \over \vdash A </math>

Gentzen konstruerte også sekventkalkylen LK, og NK er også konsistent.

== Litteratur ==
* Gerhald Gentzen. ''Untersuchungen über das logische Schlissen", 1934. (Oversatt til engelsk av M.E. Szabo, ''Investigations Into Logical Deduction'', 1964).

{{Autoritetsdata}}

[[Kategori:Beviser]]
[[Kategori:Filosofi]]

Naturlig deduksjon - Sideversjonshistorikk

Wikisida: Én sideversjon ble importert

nb>4ingBot: genitivsapostrof etter s, x og z using AWB