Inferensregel

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 9. november 2021; verifikation kræver 1 redigering .

En slutningsregel er en effektiv procedure til at kontrollere, at en given formel i den undersøgte teori kan afledes direkte i ét trin fra andre givne formler.

I en ikke-modsigende teori opnås teoremer ved at kæde anvendelsen af denne teoris slutningsregler. Desuden, hvis formlen er afledt i et vist antal trin fra formlerne , så bruges notationen til at udtrykke dette faktum . Hvis i et sådant tilfælde teorien under overvejelse er konsistent , og hver af udsagn er enten et aksiom eller en sætning, så er det også en sætning. ${\cal {B}}$ ${\cal {A_{1}}},$ $\prikker,$ ${\displaystyle {\cal {A_{n))))$ ${\cal {A_{1}}},\dots ,{\cal {A_{n}}}\vdash {\cal {B}}$ ${\cal {A_{1}}},$ $\prikker,$ ${\displaystyle {\cal {A_{n))))$ ${\cal {B}}$

I prædikatregningen i Hilberts version er slutningsreglerne modus ponens og generaliseringsreglen . Ved Gödels fuldstændighedssætning kan en formel udledes i en førsteordens prædikatregning, hvis og kun hvis den er gyldig , det vil sige sand i enhver fortolkning af den prædikatregning.

I Gentzen-type calculi ( sequent calculus , naturlige inferenssystemer ) spiller slutningsregler en stor rolle - de bruger et lille antal aksiomer og udviklede systemer af slutningsregler. I bevisteori er det netop sådanne beregninger, der bruges, da det på grund af udvælgelsen af symmetriske systemer af inferensregler er muligt at opnå konstruktive resultater om systemernes konsistens .

Se også

Litteratur

Dragalin A. G. Matematisk intuitionisme. Introduktion til bevisteori. — M .: Nauka , 1979. — 256 s. — (Matematisk logik og matematikkens grundlag).