Analytiskt bevis
Inom matematik är ett analytiskt bevis ett bevis på en sats i analys som endast använder sig av metoder från analys, och som inte till övervägande del använder sig av algebraiska eller geometriska metoder. Termen användes först av Bernard Bolzano , som först gav ett icke-analytiskt bevis på hans mellanvärdessats och sedan flera år senare gav ett bevis för satsen som var fri från intuitioner om linjer som korsar varandra vid en punkt, och så han kände sig glad när han kallade det analytiskt (Bolzano 1817).
Bolzanos filosofiska arbete uppmuntrade en mer abstrakt läsning av när en demonstration kunde betraktas som analytisk, där ett bevis är analytiskt om det inte går utöver sitt ämne (Sebastik 2007). I bevisteorin har ett analytiskt bevis kommit att betyda ett bevis vars struktur är enkel på ett speciellt sätt, på grund av villkor om typen av slutsatser som säkerställer att ingen av dem går utöver vad som finns i antagandena och vad som visas.
Strukturell bevisteori
I bevisteorin tillhandahåller begreppet analytiskt bevis det grundläggande konceptet som framhäver likheterna mellan ett antal väsentligen distinkta beviskalkyler , vilket definierar underområdet för strukturell bevisteori . Det finns ingen okontroversiell generell definition av analytiskt bevis, men för flera beviskalkyler finns det en accepterad uppfattning. Till exempel:
- I Gerhard Gentzens naturliga deduktionskalkyl är de analytiska bevisen de i normal form; det vill säga att ingen formelförekomst är både den huvudsakliga premissen för en elimineringsregel och slutsatsen av en introduktionsregel;
- I Gentzens sequential calculus är de analytiska bevisen de som inte använder cut-regeln .
Det är dock möjligt att utöka slutledningsreglerna för båda kalkylerna så att det finns bevis som uppfyller villkoret men inte är analytiska. Ett särskilt knepigt exempel på detta är till exempel den analytiska skärningsregeln , som används flitigt i tablåmetoden , som är ett specialfall av skärningsregeln där skärningsformeln är en underformel av sidoformler till skärningsregeln: ett bevis som innehåller ett analytiskt snitt är i kraft av den regeln inte analytiskt.
Dessutom har strukturella bevisteorier som inte är analoga med Gentzens teorier andra föreställningar om analytiska bevis. Till exempel strukturkalkylen sina slutledningsregler i par, kallade upp-fragmentet och ned-fragmentet, och ett analytiskt bevis är ett som bara innehåller ned-fragmentet.
Se även
- Bernard Bolzano (1817). Rent analytiskt bevis för satsen att mellan två valfria värden som ger resultat med motsatt tecken, ligger det åtminstone en reell rot av ekvationen. I Abhandlungen der koniglichen bohmischen Gesellschaft der Wissenschaften Vol. V, sid. 225-48.
- Frank Pfenning (1984). Analytiska och icke-analytiska bevis. I Proc. 7:e internationella konferensen om automatiskt avdrag .
- Jan Šebestik (2007). Bolzanos logik . Inlägg i Stanford Encyclopedia of Philosophy .