Härledningsbegrepp – Wikipedia

Härledningsbegrepp är begrepp inom metalogik och bevisteori, vilka används för att beskriva formlers inbördes relationer. Syntax och semantik är två centrala begrepp inom logiken. Även implikation inom objektlogiker kan i vissa tillämpningar uppfattas som ett härledningsbegrepp.

I logik används ordet medför (en. entails) i villkorsrelationer mellan två uppsättningar formler i ett formellt språk. Om A och B är två uppsättningar formler i det formella språket, och om en interpretering, som gör alla formler i A sanna även gör formlerna i B sanna, så B följer av A, det vill säga A medför B. Om A medför B så är detta som agument giltigt. Symboliskt skrivs detta som:

${\displaystyle A\models B}$

Detta kan även utläsas som att B är en semantisk följd av A. Relationssymbolen har även andra betydelser, bl.a. inom "datavetenskap")

I logik används ordet bevisar (en. yields eller proves) i en relation mellan två uppsättningar formler i ett formellt system. Om A och B är två uppsättning formler i det formella systemet och A bevisar B, så är B bevisbar från A. Symboliskt skrivs detta som:

${\displaystyle A\vdash B}$

Detta kan utläsas som att B är en syntaktisk konsekvens av A. Symbolen introducerades i denna mening av Gottlob Frege ^[1] 1879.

Ett deduktivt system S är fullständigt eller komplett för språket L om och endast om ${\displaystyle A\models _{L}B}$ implicerar ${\displaystyle A\vdash _{S}B}$, dvs om alla giltiga argument är härledbara.

Ett deduktivt system S är sunt för språket L om och endast om ${\displaystyle A\vdash _{S}B}$ implicerar ${\displaystyle A\models _{L}B}$, det vill säga om inga ogiltiga argument kan härledas.

Begreppet "semantisk giltighet" definieras på skilda sätt hos hos olika författare. Vissa anser att en härledning med hjälp av sanningstabeller (dvs mening) skapar semantisk giltighet, andra att det är sanningen hos A och B som avgör semantisk giltighet. Därmed blir även begreppen "fullständighet" och "sundhet" oprecisa.

En formel A är ett teorem i det formella systemet S om

${\displaystyle \vdash _{S}A}$

A är således bevisbar i S men därmed inte nödvändigtvis logiskt sann, vilket kräver att ingen tilldelning till argumenten i axiomen i S kan göra A falsk (till exempel om S inte är sunt eller inte komplett).

En formel A är en tautologi i det formella språket L om

${\displaystyle \models _{L}A}$

A är således giltig i L men därmed inte nödvändigtvis logiskt sann, vilket kräver att ingen tilldelning till argumenten till formlerna i L kan göra A falsk.

En formel B är härledbar från en mängd A av satser i det formella systemet S om och endast om det med ett ändligt antal härledningssteg följer att B impliceras av A .

${\displaystyle \vdash _{S}(A\rightarrow B)}$