New Foundations'ın Tutarlılığı – Lean Kullanılarak Kanıtlanan Çetin Bir Matematiksel İspat

Here is a summary of the key points from the given article, organized using Markdown:

New Foundations küme kuramının tutarlılık kanıtı

• Quine'ın 1937'de önerdiği "New Foundations(NF)" küme kuramının tutarlılığının Randall Holmes tarafından 2010'dan bu yana kanıtlandığı öne sürülüyordu
• Bu depo, etkileşimli teorem ispatlayıcısı Lean kullanılarak Holmes'un ispatının zor kısımlarını doğrulayarak NF'nin gerçekten çelişkisiz olduğunu kanıtlıyor
• İspat artık tamamlandı ve teorem ifadesi ConNF/Model/Result.lean içinde bulunabilir

Amaç

• NF'nin, Tangled Type Theory(TTT) tutarlıysa ve ancak o zaman tutarlı olduğu biliniyor
• Lean içinde TTT'nin bir modelini biçimsel olarak kurarak NF'nin tutarlı olduğu kanıtlanıyor
• Holmes'un ispatının çeşitli sürümleri temel alınsa da, Lean'ın tip kuramıyla uyumlu olması için çok sayıda değişiklik ve ekleme yapılmış
• Bu proje, Lean ile yazılmış topluluk matematik kütüphanesi mathlib'e dayanıyor; böylece kardinal sayılar veya gruplar gibi tanıdık sonuçlar yeniden doğrudan ispatlanmadan kullanılabiliyor
• mathlib ve bu projedeki tüm tanım ve teoremler, Lean'ın güvenilir çekirdeği tarafından doğrulanmış olsa da, Lean tanım ve teorem açıklamalarının amaçlanan İngilizce açıklamalarla eşleşip eşleşmediğini denetleyemez; bu nedenle projenin kodundan sonuç çıkarırken İngilizce ile yapılan çeviriye dikkat etmek gerekir

Tangled Type Theory(TTT)

• TTT, eşitlik ilişkisi "=" ve üyelik ilişkisi "∈" içeren çok sıralı bir küme kuramıdır
• Sıralar bir limit ordinal λ ile indekslenir ve λ'nın elemanlarına tip indisleri denir
• "x = y" formülü, x ve y aynı tipte olduğunda iyi biçimlenir; "x ∈ y" formülü ise x, y'den daha küçük herhangi bir tipe sahip olduğunda iyi biçimlenir
• TTT'nin aksiyomlarından biri, α tipindeki bir kümenin β < α olan herhangi bir β tipindeki elemanları tarafından tekil biçimde belirlenmesi anlamındaki dışlemselliktir
• Örneğin α tipindeki iki küme farklıysa, her β < α için farklı β tipinde elemanlara sahip olurlar; bu özellik TTT modeli kurmayı zorlaştırır

Strateji

• Model kurma süreci kabaca şu stratejiyi izliyor:

  • Temel tiplerin kurulumu

    • λ bir limit ordinal, κ > λ bir düzenli ordinal ve μ > κ, en az κ kofinalitesine sahip güçlü limit kardinal olarak alınır
    • κ'dan küçük kümelere küçük denir
    • -1 seviyesinde, sonradan modelin parçası olacak tüm tiplerin altında yer alan yardımcı bir temel tip kurulur
    • Bu tipin elemanlarına atom denir (ZFU ya da NFU anlamındaki atomlar değildir) ve μ tane atom vardır; bunlar κ büyüklüğündeki litter'lara ayrılır

  • Her tipin inşası

    • Her α tip seviyesi için, TTT'nin amaçlanan modeli için bazen t-kümeleri denen bir model öğeleri koleksiyonu üretilir
    • t-kümeleri üzerinde etki eden, izinli permütasyonlar denen bir permütasyon grubu oluşturulur
    • Üyelik ilişkisi, izinli permütasyonların etkisi altında korunur
    • Her t-kümesinin, izinli permütasyonların etkisi altında bir desteğe sahip olması şart koşulur; bu destek adresler denen küçük nesneler kümesidir ve izinli bir permütasyon destekteki tüm öğeleri sabitlediğinde t-kümesi de sabit kalır
    • α seviyesindeki her t-kümesine, β < α tipindeki tercih edilen bir uzantı verilir ve t-kümesinin elemanlarından hangi uzantının tercih edildiği geri kazanılabilir
    • t-kümelerinin diğer alt tiplerdeki uzantıları bu β-uzantısından çıkarılabilir; böylece TTT'nin dışlemsellik aksiyomu sağlanabilir

  • Her tipin büyüklüğünün kontrolü

    • Her α tipi, yalnızca tüm β < α tiplerinin büyüklüğünün tam olarak μ olduğu varsayımı altında (başka varsayımlarla birlikte) kurulabilir
    • α seviyesindeki t-kümeleri koleksiyonunun en az μ kardinalitesine sahip olduğunu göstermek kolaydır; dolayısıyla bu kümenin en fazla μ öğe içerdiğini göstermek gerekir
    • Bu, izinli permütasyonların etkisi altındaki dolaşıklık için özünde farklı açıklamaların çok fazla olmadığını göstererek yapılabilir
    • Bunun için, izinli permütasyonların kurulmasına imkân veren teknik bir yardımcı lemma olan eylemin özgürlüğü teoremi gerekir
    • Bu bölümün ana sonucu burada yer alır

  • Tümevarımın tamamlanması

    • Yukarıdaki süreç özyinelemeli olarak yürütülerek her α tip seviyesinde tangled type'lar üretilebilir
    • Bu, küme kuramında kolay bir adım olsa da, gerekli çeşitli tümevarım varsayımlarının karşılıklı bağlantısı nedeniyle tip kuramında çok iş gerektirir
    • Ardından kurulumumuzun gerçekten TTT'nin bir modelini üretip üretmediği, yani kuramın sonlu aksiyomatizasyonunu sağlayıp sağlamadığı doğrulanır
    • NF'nin kavrama şeması için Hailperin'in sonlu aksiyomatizasyonunu TTT'nin sonlu aksiyomatizasyonuna dönüştürmeyi seçtik ve bunu sonuç dosyasında sunduk
    • Ancak bu seçim keyfidir; zaten kurulmuş altyapı kullanılarak başka sonlu aksiyomatizasyonlar da kolayca kanıtlanabilir

GN⁺ görüşü

• Bu ispat, şimdiye kadar yalnızca çok soyut bir düzeyde bilinen NF küme kuramının tutarlılığını biçimsel olarak ortaya koyması bakımından çok anlamlı bir sonuçtur. Bu, yalnızca saf matematik açısından değil, ispat yardımcı araçlarının gelişimi ve otomatik teorem ispatında somut ilerlemeyi göstermesi açısından da önemlidir
• Lean ile yapılan biçimselleştirme çalışması ispatın doğruluğunu ve tamlığını güvence altına alır; ancak aynı zamanda matematikçilere alışıldık gelmeyen bir dilde yazıldığı için anlaşılması zor olabilir. İspatın temel fikirlerini doğal dille açık biçimde anlatan çalışmaların da eşlik etmesi gerekir
• TTT'nin tuhaf dışlemsellik aksiyomunun neden gerekli olduğu, başka küme kuramlarıyla ilişkisinin ne olduğu gibi arka plan kuramına dair sezgisel açıklamalar da görece yetersizdir. Yalnızca biçimsel ispat değil, felsefi ve tarihsel bağlamın tartışılması da eklenirse NF kuramının anlaşılması daha da artabilir
• Kurulan modelin standart ZFC küme kuramı modelleriyle nasıl bir ilişki içinde olduğu, NF'nin tutarlılığının başka aksiyom sistemlerinin tutarlılığıyla nasıl bağlantı kurduğu gibi gelecekteki ek araştırma başlıkları da ilgi çekici görünüyor
• Böylesine karmaşık bir ispatın Lean ile biçimselleştirilmesi, matematiğin başka alanlarında ispat otomasyonu için de örnek olabilir. İspat süreci daha önce iyi bilinmeyen teoremler üzerinde benzer çalışmalar yapılırsa matematik dünyasında büyük etki yaratması beklenebilir

[GN⁺]

Hacker News yorumları

• Lean kullanılarak yapılan bir ispatın yanlış olma riski çok düşüktür. Ancak Lean’daki hatalardan bağımsız olarak, yazılım doğrulama ve matematikte bilinen bir sorun olarak, sonucun dikkatle okunup gerçekten ispatlanan şeyin bu olup olmadığının kontrol edilmesi gerekir.
• Bu örnek, zor bir ispatın durumunu çözmek için ispat yardımcısının kullanıldığı ilk örnek gibi görünüyor. Daha önce, güvenilir olmayan yazılımlarla işlenen büyük ölçekli hesaplama unsurları içeren mevcut ispatları doğrulayan projeler vardı; ancak bu örnek, sonucun epistemolojik statüsünün matematik dünyasında belirsiz olduğu ilk örnekti.
• Coq ile Lean arasındaki temel farkların ne olduğu ve aynı tür mantık üzerinde çalışıp çalışmadıkları konusunda merak dile getiriliyor. İlgili tartışmada anlaşılması zor içeriklerden söz ediliyor.
• Lean destekçileri, Lean’ın üstün bir ispat yöntemi olduğu fikrine fazla ağırlık verme eğiliminde. Lean sadece alternatif bir ispat yöntemidir; ayrıca bir programlama dili ve sistem olarak kendi hatalarına sahiptir ve başkaları tarafından yazılmış çeşitli kütüphane yığınlarına büyük ölçüde dayanır.
• “Lean ispatın doğru olduğunu söyledi” demektense, yazılan ispatın insan matematikçiler tarafından doğrulandığını ve ardından Lean’a aktarılıp orada da doğrulandığını söylemek daha doğru ve dürüst olur. Lean’ın tek ve altın standart bir doğrulama sunduğu yönündeki açıklama ya doğru değil ya da en azından bunu böyle söyleyen bir açıklama görülmemiş.
• "New Foundations" küme kuramı biçimselleştirmesinin, diğer biçimselleştirmelere kıyasla özel ya da yeni olan yönlerine dair, matematik lisans öğrencilerinin veya mühendislik alanındaki uzmanların okuyabileceği düzeyde kabaca bir açıklama isteniyor.
• Bu yaklaşımın sonunda işbirlikçi ispatlara ve “bug fix”lere yol açıp açmayacağı, matematiği GitHub’daki koda benzer bir sürece dönüştürüp dönüştürmeyeceği merak ediliyor.
• Gödel’in teoremine göre yeterince güçlü hiçbir sistem kendi tutarlılığını gösteremez denildiği için, buna ilişkin soru soruluyor.
• mathlib projesini takip etmeyi sürdürmek isteniyor ama zaman yok. Çok pasif bir şekilde katılmanın bir yolu olup olmadığı merak ediliyor.