Deduktiolause

Deduktiolause ( deduktiolemma , deduktiolause ) on yksi todistusteorian perustuloksista , se formalisoi päättelymenetelmän, jossa implikaatiota käytetään välttämättömänä edellytyksenä johtamisen perustamiselle. Sitä käytetään päätelmien ja todisteiden olemassaolon toteamiseen käyttämättä niiden rakennetta. Herbran muotoili sen ensimmäisen kerran ja todisti sen vuonna 1930 , ja Herbran käytti sitä ilman todisteita vuonna 1928. Tarski muotoili tämän periaatteen itsenäisesti vuonna 1930. Tarskin mukaan hän tiesi ja sovelsi tätä periaatetta jo vuonna 1921 [1] . $A\Nuoli oikealle B$ $A$

Lauselaskennan formulointi

Jos , niin . $A \vdash B$ $\vdash A\Rightarrow B$
Jos , niin . $A_{1},...,A_{m-1},A_{m}\vdash B$ $A_{1},...,A_{m-1}\vdash A_{m}\Rightarrow B$

Tässä - loogiset kaavat ( muototeoria lauselaskennassa), tarkoittaa, että kaava on johdettu kaavasta (teoriassa ), ja tarkoittaa, että kaava on todistettavissa (on teorian lause ). Merkki tarkoittaa implikoinnin loogista toimintaa . ${\näyttötyyli A,B,A_{1},...,A_{m-1},A_{m))$ $L$ $A \vdash B$ $B$ $A$ $L$ $\vdash B$ $B$ $L$ $A\Nuoli oikealle B$

Ensimmäisen asteen teorioiden muotoilu

Antaa olla osajoukko (mahdollisesti tyhjä ) kaavoista jonkin ensimmäisen asteen teoriasta ja olla teorian kaavoja . Sitten jos kaavojen joukosta on olemassa sellainen kaavan johtaminen, jossa mikään kaavan vapaista muuttujista ei liity yleistyssäännön soveltamiseen kaavoihin, jotka riippuvat tämän johdannaisen kaavasta , niin . $\Gamma$ $K$ $A$ $B$ $K$ $B$ $\Gamma \cup \{A\}$ $A$ $A$ $\Gamma \vdash A\Rightarrow B$

Katso myös

Herbrandin lauseet

Muistiinpanot

↑ Matemaattinen logiikka, 1973 , s. 54-55.

Kirjallisuus

Kleene S.K. Matemaattinen logiikka. - M .: Mir, 1973. - 480 s.