Teorema di eliminazione del taglio

Questa voce o sezione sull'argomento matematica è stata parzialmente tradotta dalla lingua inglese.

Puoi contribuire terminando la traduzione o usando altre fonti. Non usare programmi di traduzione automatica. Usa {{Tradotto da}} quando hai terminato. Se nella pagina di modifica trovi del testo nascosto, controlla che sia aggiornato servendoti dei collegamenti «in altre lingue» in fondo alla colonna di sinistra. Segui i suggerimenti del progetto di riferimento.

Il Teorema di eliminazione del taglio (o Hauptsatz di Gentzen) è il principale risultato che mostra l'importanza del calcolo dei sequenti. Venne dimostrato originariamente da Gerhard Gentzen nel suo storico articolo "Investigations in Logical Deduction" per i sistemi LJ ed LK, in cui sono formalizzate rispettivamente la logica intuizionista e la logica classica. Il teorema di eliminazione del taglio stabilisce che ogni giudizio che possiede nel calcolo dei sequenti una dimostrazione facente uso della regola del taglio possiede anche una dimostrazione senza taglio cioè una dimostrazione che non fa uso della regola del taglio.

La regola del taglio

Un sequente è un'espressione logica che mette in relazione molte formule, nella forma " $A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots$ ", che deve essere letta come " $A_{1},A_{2},A_{3},\ldots$ dimostra $B_{1},B_{2},B_{3},\ldots$ ", e (come messo in evidenza da Gentzen) deve essere concepita come equivalente alla funzione di verità "Se ( $A_{1}$ and $A_{2}$ and $A_{3}$ …) allora ( $B_{1}$ or $B_{2}$ or $B_{3}$ …)."^[1] Il lato sinistro (left-hand site o LHS) è una congiunzione mentre il lato destro (right-hand site o RHS) è una disgiunzione.

Il lato sinistro può avere poche o tante formule e quando è vuoto il lato destro è una tautologia. Nella logica classica il lato destro può avere qualsiasi numero di formule; se è vuoto il lato sinistro è una contraddizione, mentre nella logica intuizionista il lato destro può avere solo una formula o nessuna: notiamo che ammettere più di una formula nel lato destro equivale, in presenza della regola di contrazione, all'ammissibilità del principio del terzo escluso.Comunque il calcolo dei sequenti è uno schema abbastanza espressivo e sono stati proposti calcoli dei sequenti per la logica intuizionista che ammettono più formule nel lato destro. Dal calcolo classico dei sequenti (LC) di Jean-Yves Girard è semplice ottenere una formulazione piuttosto naturale della logica classica dove il lato destro contiene al massimo una formula; la chiave è l'interazione della logica e delle regole strutturali.

Il "taglio" è una regola nella normale esposizione del calcolo dei sequenti, e equivalente ad una varietà di regole in altre teorie della dimostrazione che dato

$\Gamma \vdash A,\Delta$

$\Pi ,A\vdash \Lambda$

permette di inferire

$\Gamma ,\Pi \vdash \Delta ,\Lambda$

Cioè, "taglia" l'occorrenza della formula $A$ dalla relazione di inferenza.

Note

^ Wilfried Buchholz, Beweistheorie (university lecture notes about cut-elimination, German, 2002-2003)

Collegamenti esterni

(EN) Eric W. Weisstein, Teorema di eliminazione del taglio, su MathWorld, Wolfram Research.

Read other articles:

Kuliax

KuliaxPerusahaan / pengembangKuliax ProjectKeluargaLinuxRilis stabil terkini7.0 / 23 Agustus 2010Kernel typeMonolithic kernelAntarmuka bawaanKDELisensiSebagian besar GPLSitus web resmikuliax.net[pranala nonaktif] Kuliax adalah sebuah distribusi Linux LiveCD yang dikembangkan oleh Kuliax Project[pranala nonaktif] untuk pendidikan di universitas. Distribusi ini awalnya berbasis Debian GNU/Linux dan Knoppix, kemudian setelah versi 6.0 pengembangannya diubah ke basis Debian G...

Gibuti

Disambiguazione – Se stai cercando altri significati, vedi Gibuti (disambigua). Gibuti (dettagli) (dettagli) (FR) Unité, Égalité, Paix(AR) اتحاد، مساواة، سلام (Aitihadun, Musawat, Salam)(IT) Unità, Uguaglianza, Pace Gibuti - Localizzazione Dati amministrativiNome completoRepubblica di Gibuti Nome ufficiale(AR) جمهورية جيبوتيJumhuriya Jibuti(FR) République de Djibouti Lingue ufficialifrancese e arabo Altre linguesomalo, afar Capitale Gibuti (561 ...

Kubak Belarusi 2014-2015

Kubak Belarusi 2014-2015 Competizione Kubak Belarusi Sport Calcio Edizione 24ª Organizzatore BFF Date dal 25 luglio 2014al 24 maggio 2015 Luogo Bielorussia Formula Eliminazione diretta Risultati Vincitore BATĖ Borisov(3º titolo) Secondo Šachcër Salihorsk Cronologia della competizione 2013-2014 2015-2016 Manuale La Coppa di Bielorussia 2014-2015 (in bielorusso Кубак Беларусі, Kubak Belarusi) è stata la 24ª edizione del torneo. Il torneo è iniziat...

W. A. R. Goodwin

American Episcopal clergyman, historian and author For other people named William or Bill Goodwin, see William Goodwin (disambiguation). The ReverendW. A. R. GoodwinGoodwin in 1926BornJune 18, 1869Richmond, VirginiaDiedSeptember 7, 1939(1939-09-07) (aged 70)EducationRichmond CollegeAlma materRoanoke CollegeVirginia Theological SeminarySpouses Evelyn Tannor (died 1915) Ethel Howard (m. 1918) Children6Parent...

大字 (数字)

この項目には、一部のコンピュータや閲覧ソフトで表示できない文字が含まれています（詳細）。数字の大字（だいじ）は、漢数字の一種。通常用いる単純な字形の漢数字（小字）の代わりに同じ音の別の漢字を用いるものである。概要壱万円日本銀行券（「壱」が大字）弐千円日本銀行券（「弐」が大字）漢数字には「一」「二」「三」と続く小字と、「壱」「�...

Pirmin Schwegler

Pirmin Schwegler Informasi pribadiNama lengkap Pirmin SchweglerTanggal lahir 9 Maret 1987 (umur 37)Tempat lahir Ettiswil, SwissTinggi 1,79 m (5 ft 10+1⁄2 in)Posisi bermain Gelandang tengahInformasi klubKlub saat ini 1899 HoffenheimNomor 16Karier junior1992–2002 FC Grosswangen2002–2003 FC LuzernKarier senior*Tahun Tim Tampil (Gol)2003–2005 FC Luzern 40 (3)2005–2006 Young Boys 32 (1)2006–2009 Bayer Leverkusen 46 (0)2009–2014 Eintracht Frankfurt 128 (6)2014...

Little Silver station

NJ Transit rail station Little SilverLittle Silver station in January 2018.General informationLocationOceanport (CR 11) and Sycamore Avenues at Ayers Lane, Little Silver, New Jersey 07739Owned byNJ TransitLine(s)North Jersey Coast LinePlatforms2 side platformsTracks2Connections Academy BusConstructionParkingYesBicycle facilitiesYesAccessibleNoOther informationFare zone19HistoryOpened1875Rebuilt1890, 2003Passengers2012783 (average weekday)[1] Services Preceding station NJ Tra...

قائمة المدن العربية في إسرائيل

خريطة توضح المناطق العربيَّة في دولة إسرائيل (بما في ذلك القدس الشرقية ومرتفعات الجولان). تُمثل المخططات المدن المختلطة رسمياً (يسكن ما لا يقل عن 2% من العرب في مدن ذات أغلبيّة يهودية). وفقاً لإحصاءات عام 2010، يعيش 91.6% من السكان العرب في 134 مجلس وبلدية ذات أغلبية عربيّة. ويعيش ح�...

1278 en santé et médecine

Chronologies Données clés 1275 1276 1277 1278 1279 1280 1281Décennies :1240 1250 1260 1270 1280 1290 1300Siècles :XIe XIIe XIIIe XIVe XVeMillénaires :-Ier Ier IIe IIIe Chronologies thématiques Religion (,) et * Croisades Science () et Santé et médecine Terrorisme Calendriers Romain Chinois Grégorien Julien Hébraïque Hindou Hégirien Persan Républicain modifier Années de la santé et de la médecine ...

Simatic

Series of programmable logic controllers This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages) This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (March 2020) (Learn how and when to remove this message) This article relies excessively on references to primary sourc...

Liberty First Credit Union Arena

Liberty First Credit Union ArenaThe Slaughterhouse[1]Ralston ArenaLocation within NebraskaShow map of NebraskaRalston ArenaLocation within the United StatesShow map of the United StatesFormer namesRalston Arena (2012–2021)Location7300 Q StreetRalston, Nebraska 68127,United StatesCoordinates41°12′25″N 96°01′37″W / 41.20694°N 96.02694°W / 41.20694; -96.02694Public transitMetro TransitOwnerCity of RalstonOperatorCity of RalstonCapacity4,356 - (End St...

قائمة مغتصبي العرش البيزنطي

هذه المقالة بها مشكلات متعدِّدة. فضلًا ساعد في تحسينها أو ناقش هذه المشكلات في صفحة النقاش. يفتقر محتوى هذه المقالة إلى الاستشهاد بمصادر. فضلاً، ساهم في تطوير هذه المقالة من خلال إضافة مصادر موثوق بها. أي معلومات غير موثقة يمكن التشكيك بها وإزالتها. (ديسمبر 2018) هذه المقالة ي�...

1914–15 Star

Campaign medal of the British Empire Award1914–15 StarTypeCampaign medalAwarded forCampaign serviceCountry United KingdomPresented bythe Monarch of the United Kingdom and the British Dominions, and Emperor of IndiaEligibilityBritish and Imperial forcesCampaign(s)First World WarEstablishedDecember 1918Total2,366,000Ribbon bar Order of wearNext (higher)1914 StarNext (lower)British War MedalRelated1914 StarAfrica General Service MedalKhedive's Sudan Medal of 1910 The 1914–15 Star i...

2022 Conservative Party of Canada leadership election

Political party leadership contest 2022 Conservative Party of Canada leadership election ← 2020 September 10, 2022 Opinion pollsTurnout64.51%[1] Candidate Pierre Poilievre Jean Charest Points 22,993.42(68.15%) 5,421.62(16.07%) Candidate Leslyn Lewis Roman Baber Points 3,269.54(9.69%) 1,696.76(5.03%) Previous Leader Candice Bergen (interim) Elected leader Pierre Poilievre 2022 Conservative leadership electionDateSeptember 10, 2022ConventionShaw Centre, Ott...

2011 FA Community Shield

Football match2011 FA Community ShieldThe match programme cover Manchester City Manchester United 2 3 Date7 August 2011VenueWembley Stadium, LondonMan of the MatchNani (Manchester United)RefereePhil Dowd (Staffordshire)[1]Attendance77,169WeatherRain16 °C (61 °F)[2]← 2010 2012 → The 2011 FA Community Shield (also known as The FA Community Shield sponsored by McDonald's for sponsorship reasons) was the 89th FA Community Shield, an annual football match c...

University of Paris

Historic university in Paris, France (1150–1970) University of ParisFrench: Université de ParisCoat of arms Latin: Universitas magistrorum et scholarium ParisiensisMottoHic et ubique terrarum (Latin)Motto in EnglishHere and anywhere on EarthTypeCorporative, then public universityEstablishedOrigin: High Middle Ages at the Parisian cathedral school Founded: 1045–1150Suppressed: 1793Faculties reestablished: 1806University reestablished: 1896Divided: 1970LocationParis, FranceCampusUrban...

Rome

Pour les articles homonymes, voir Rome (homonymie). Pour les articles ayant des titres homophones, voir Rom, Romme, Roms et Rhum. Rome Roma Armoiries Drapeau De gauche à droite et de haut en bas : le Colisée, le monument à Victor-Emmanuel II, la place de la République, le château Saint-Ange, la fontaine de Trevi, la basilique Saint-Pierre et une vue aérienne de la ville. Administration Pays Italie Région Latium Ville métropolitaine Rome Capitale Maire Mandat Rob...

اشتهاء المجرمين

اشتهاء المجرمين هو شذوذ جنسي يكون فيه الشخص منجذبا جنسيا نحو الأشخاص الذي قاموا بارتكاب جرائم مثل المغتصب والقتلة واللصوص.[1][2][3] على عكس معظم حالة الاشتهاء الأخرى، فإن اشتهاء المجرمين يحدث بشكل حصري بالعادة للنساء. تعرف في الثقافة الشعبية باسم «حالة بوني وكلا...

Luke Hughes (ice hockey)

American ice hockey player (born 2003) Ice hockey player Luke Hughes Hughes with the Devils in 2023Born (2003-09-09) September 9, 2003 (age 20)Manchester, New Hampshire, U.S.Height 6 ft 2 in (188 cm)Weight 184 lb (83 kg; 13 st 2 lb)Position DefenseShoots LeftNHL team New Jersey DevilsNational team United StatesNHL draft 4th overall, 2021New Jersey DevilsPlaying career 2023–present Luke Warren Hughes (born September 9, 2003) is an American pr...

Paper Airplane (The Office)

20th episode of the 9th season of The Office Paper AirplaneThe Office episodeEpisode no.Season 9Episode 20Directed byJesse PeretzWritten by Halsted Sullivan Warren Lieberstein Cinematography byMatt SohnEditing by David Rogers Curtis Thurber Production code9020[1]Original air dateApril 25, 2013 (2013-04-25)[1]Running time22 minutesGuest appearances Roseanne Barr as Carla Fern Nora Kirkpatrick as Esther Bruegger Mark Proksch as Nate Nickerson Blake Robbins as...