Avtagbarhet av sektioner

Avlägsnande av sektioner ( Gentzens sats , eliminationssats ) är en egenskap hos logiska kalkyler, enligt vilken vilken som helst sekvensavledning i en given kalkyl kan härledas utan att tillämpa sektionsregeln [1] . Den spelar en grundläggande roll i bevisteorin och en viktig metodologisk roll i matematisk logik i allmänhet på grund av att den tillhandahåller en konstruktiv metod för att bevisa konsistens , i synnerhet för klassiska och intuitionistiska logiker av första ordningen [2] .

För de klassiska och intuitionistiska sekvenskalkylerna bevisades egenskapen av Gentzen 1934 . 1953 angavs Takeuchis gissning , enligt vilken borttagningsbarheten av sektioner äger rum för den enkla teorin om typer och den högre ordningens logik som motsvarar den, senare bekräftades det - för den klassiska logiken av andra ordningen, borttagbarheten av avsnitten bevisades av Tate , för den enkla teorin om typer - Takahashi och Pravitsa , hittades snart bevis för en serie icke-klassiska teorier av högre ordning ( Dragalin ) och avancerade typteorier ( Girard för system F ).

Symbolisk formulering: låt och  vara bevisbara följder av kalkylen ; om  är en kalkylsekvens , då är det bevisbart [3] .

Anteckningar

  1. ↑ Proof Theory, 1978 , sid. 29.
  2. ↑ P. I. Bystrov. Eliminationssats  // New Philosophical Encyclopedia  : i 4 volymer  / föregående. vetenskaplig-ed. råd av V. S. Stepin . — 2:a uppl., rättad. och ytterligare - M .  : Tanke , 2010. - 2816 sid.
  3. ↑ Ershov, 1987 , sid. 214.

Litteratur