قضیه درخت کروسکال نقشی اساسی در علم کامپیوتر ایفا میکند. این قضیه توسط آندرو وزسونی حدس زده شده و توسط جوزف کروسکل ثابت شدهاست؛ شخص نش ویلیامز هم کمی در اثبات این قضیه نقش داشتهاست. این قضیه از زمانی که یک مثال برجسته در ریاضیات معکوس شناخته شد به عنوان بیانیه ای است که نمیتوان آن را با ATR0 ثابت کرد (یک شکل از ریاضیات نامحدود معکوس) و یکی از استفادههای این قضیه شدت رشد سریع تابع درخت است.
در سال ۲۰۰۴ این نتیجه کلی از درختان، به عنوان قضیه رابرتسون–سیمورگراف، به گرافها تعمیم یافت. یکی از نتایج ثابت شده از آن در ریاضی معکوس بسیار برجسته است و حتی ممکن است ریاضیات را برای رسیدن به توابع SSCG با رشد سریعتر هدایت کند.
ما اثباتکننده این قضیه را نش ویلیامز در نظر میگیریم اگرچه فرمول کروسکال به گونه ای بهتر است. یک درخت ریشه دار را T و دو رأس را V و W در نظر بگیرید. V را جانشین W گویند اگر یک مسیر از ریشه تا V شامل W هم شود و V را جانشین مستقیم W گویند اگر مسیر W تا V شامل رأس دیگری نباشد.X را یک مجموعه نیمه مرتب شده در نظر بگیرید. T1 و T2 را دو درخت ریشه دار با رأسهایی در مجموعه X در نظر بگیرید، میگوییم T1 در T2 جایگذاری شدهاست اگر یک نگاشت مثل F از رأسهای T1 به رأسهای T2 وجود داشته باشد به گونه ای که
نتیجه میشود که به ازای هر درخت ریشه دار که رأسهای آنها در مجموعه X باشد یک درخت مثل i داریم که در درخت j جایگذاری شده باشد به شرط اینکه i از j کوچکتر باشد.
برای یک مجموعه محدود از رأسها مثل X، قضیه درخت کروسکال میتواند توسط قضیه مرتبه دوم ریاضی بیان و ثابت شود. اگرچه، مثل قضیه گودزتین یا قضیه پاریس-هرینگتون، در بعضی موارد خاص این قضیه میتواند توسط زیرسیستمهای مرتبه دوم ریاضی خیلی کندتر از زیرسیستمها بیان شود. این موضوع اولین بار توسط هاروی فریدمن در اوایل سال ۱۹۸۰ مشاهده شد، یک موفقیت که بعدها زمینه ریاضیات معکوس شد. در این مورد که درختان بدون رأس برچسب گذاری شده در نظر گرفته شوند، فریدمن کشف کرد که نتیجه در ATR[۱] غیرقابل اثبات است پس اولین مثال از نتیجه قابل پیشبینی با یک اثبات غیرقابل پیشبینی و قابل اعتماد زده شد.[۲] این مورد از قضیه هنوز در Π11-CA۰ قابل اثبات است، اما با اضافه کردن یک «شرط جزئی» به تعریف مرتبسازی درختها در بالا، او یک تغییر طبیعی در تئوری یافت که در این سیستم غیرقابل اثبات بود .[۳][۴] مدتها بعد، رابرستون سیمور یک قضیه غیرقابل اثبات دیگر را در Π11-CA۰ مطرح کرد.
تحلیل و بررسی وصفی، استحکام قضیه کراسکال را تأکید میکند.
فرض کنید (P(n این بیانیه باشد
این بیانیه یک کاربرد ساده از قضیه کروسکال است. برای هر n ریاضیات پینو میتواند ثابت کند که (P(n درست است اما ریاضیات پینو نمیتواند این بیانیه را ثابت کند "(P(n درست است برای هر n".[۴] علاوه بر این کوتاهترین اثبات از (P(n به عنوان یک تابع از n در ریاضیات پینو به شدت سریع رشد میکند، خیلی سریعتر از هر تابع بازگشتی اولیه یا تابع آکرمن برای مثال.[۴]
با ترکیب برچسبها فریدمن یک تابع سریعتر را معرفی کرد.[۵] برای یک عدد صحیح مثبت n درخت (n) را در نظر میگیریم[۵] برای رسیدن به بزرگترین m مراحل زیر را طی میکنیم:
این دنباله درختی آغاز میشود با درخت(۱) = ۱, درخت(۲) = ۳ و سپس بهطور ناگهانی درخت(۳) گسترش مییابد به یک مقدار خیلی بزرگ که از مقدار ثابت دیگری، مانند جمله چهارم فریدمن، در مقایسه با آن بسیار کوچکاند. یک کران پایین برای (n(4، و از این جهت یک کران خیلی کوچک پایین برای درخت (۳) هست. برای مثال، اعداد گراهام، تقریباً برابر 64(4) هستند که خیلی کوچکتر از کران پایین (187196)(1) هستند. میتوان نشان داد که درجه رشد تابع درختی در سلسله مراتب رشد سریع حداقل هست.