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.
Härledningsbegrepp |
---|
Närliggande begrepp |
Medför, giltighet
redigeraI 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:
Detta kan även utläsas som att B är en semantisk följd av A. Relationssymbolen har även andra betydelser, bl.a. inom "datavetenskap")
Bevisbar, konsekvens
redigeraI 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:
Detta kan utläsas som att B är en syntaktisk konsekvens av A. Symbolen introducerades i denna mening av Gottlob Frege [1] 1879.
Fullständighet och sundhet
redigeraEtt deduktivt system S är fullständigt eller komplett för språket L om och endast om implicerar , dvs om alla giltiga argument är härledbara.
Ett deduktivt system S är sunt för språket L om och endast om implicerar , 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.
Teorem
redigeraEn formel A är ett teorem i det formella systemet S om
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).
Tautologi
redigeraEn formel A är en tautologi i det formella språket L om
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.
Härledbarhet
redigeraEn 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 .
Referenser
redigera- ^ Gottlob Frege, Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle, 1879.