New Foundations’ın tutarlılığı – Lean ile doğrulanmış zorlu matematiksel kanıt

 (leanprover-community.github.io)
1 puan yazan GN⁺ 2024-04-24 | 1 yorum | WhatsApp'ta paylaş
  • Quine’ın 1937’de önerdiği küme teorisi New Foundations için tutarlılık kanıtının zor kısmı Lean ile doğrulandı; temel teorem ConNF/Model/Result.lean içinde düzenlenmiş durumda
  • Yaklaşım, New Foundations ile Tangled Type Theory(TTT) tutarlılığının eşdeğer olduğu sonucundan yararlanarak Lean içinde biçimsel olarak bir TTT modeli kurmaya dayanıyor
  • TTT modelinin kurulması, kümelerin daha düşük tipteki elemanlar tarafından benzersiz biçimde belirlenmesini gerektiren dışsallık nedeniyle zorlaşıyor
  • Model kurulumunda base type, t-set, allowable permutations, small support ve preferred extension kullanılıyor; tip boyutunu μ ile kontrol etmek için freedom of action theorem gerekiyor
  • Lean çekirdeği biçimselleştirilmiş kanıtı denetliyor, ancak biçimsel ifadenin amaçlanan İngilizce anlamla örtüşmesini garanti etmediği için sonuçların yorumlanmasında çeviri kontrolü gerekiyor

Lean ile tamamlanan New Foundations tutarlılık doğrulaması

  • Quine 1937’de küme teorisi New Foundations’ı önerdi; Randall Holmes ise 2010’dan beri bunun tutarlılık kanıtına sahip olduğunu iddia ediyordu
  • Bu proje, Holmes’un kanıtının zor kısmını etkileşimli teorem kanıtlayıcı Lean ile doğrulayarak New Foundations’ın tutarlılığını göstermeye odaklanıyor
  • Kanıt tamamlandı; teorem ifadesi ConNF/Model/Result.lean içinde görülebilir
  • İlgili materyaller de birlikte sunuluyor

Kodu yerelde çalıştırma

  • Yerelde çalıştırmak için elan kurulup depo klonlandıktan sonra, depo kök dizininde şu komut çalıştırılabilir
lake exe cache get
  • Ardından kod Visual Studio Code gibi bir düzenleyicide incelenebilir; komut satırında ise lake build ile doğrudan derlenebilir

New Foundations ile TTT arasındaki bağlantı

  • New Foundations’ın, Tangled Type Theory(TTT) tutarlı olduğunda ve ancak o zaman tutarlı olduğu biliniyor
  • Proje, Lean’de TTT modelini biçimsel olarak kurdu; bunun üzerinden kâğıt üzerindeki sonuç olarak New Foundations’ın tutarlılığı, yani Con(NF) elde ediliyor
  • Çalışma Holmes’un çeşitli kanıt belgelerine dayanarak yürütüldü; ancak Lean’in tip teorisine uydurmak için çok sayıda değişiklik ve ekleme gerekti

Lean doğrulamasının temeli ve yorumlamada dikkat edilmesi gerekenler

  • Proje, Lean ile yazılmış topluluk matematik kütüphanesi mathlib’e dayanıyor
  • mathlib sayesinde kardinal sayılar ve gruplar gibi tanıdık sonuçlar proje içinde yeniden kanıtlanmadan kullanılabiliyor
  • mathlib’in ve bu projenin tanım ve teoremleri Lean’in güvenilir çekirdeği tarafından denetleniyor
    • Lean çekirdeği, oluşturulan kanıtın gerçekten doğru olup olmadığını hesaplamalı olarak doğruluyor
  • Ancak Lean, biçimsel ifadenin amaçlanan İngilizce karşılığıyla uyuşup uyuşmadığını denetleyemiyor
    • Koddan sonuç çıkarırken İngilizce açıklama ile biçimsel ifade arasındaki çeviriye dikkatle bakmak gerekiyor

Tangled Type Theory’nin yapısı ve zorlukları

  • TTT, eşitlik = ve üyelik ilişkisi ∈ içeren çok-türlü bir küme teorisidir
  • Türler(sort), limit ordinal λ ile indekslenir; λ’nın elemanları tip indeksleri olarak adlandırılır
  • İfadelerin oluşum koşulları tipler tarafından kısıtlanır
    • x = y, x ve y aynı tipte olduğunda iyi biçimlenmiştir
    • x ∈ y, x’in tipi y’nin tipinden düşük olduğunda iyi biçimlenmiştir
  • Temel zorluk TTT’nin dışsallık aksiyomundan kaynaklanır
    • α tipindeki bir küme, herhangi bir β < α tipindeki elemanlar tarafından benzersiz biçimde belirlenmelidir
    • Örneğin α tipindeki iki küme farklıysa, her β < α için birbirinden farklı β tipi elemanlara sahip olmalıdır
  • Bu gereklilik nedeniyle TTT modeli kurmak, basit bir küme teorisi modeli kurmaktan daha çetrefilli hâle gelir

Model kurulumunun başlıca adımları

  • Base type kurulumu

    • λ bir limit ordinal, κ > λ bir regular ordinal, μ > κ ise eşsonluluğu en az κ olan güçlü limit kardinal olacak şekilde alınır
    • Boyutu κ’dan küçük kümeler small olarak adlandırılır
    • Tüm model tiplerinin altındaki yardımcı tip olan seviye -1’deki base type önce kurulur
    • Bu tipin elemanlarına atoms denir; ancak bunlar ZFU veya NFU anlamındaki atomlar değildir
    • μ adet atom vardır ve bunlar κ büyüklüğündeki litters kümelerine ayrılır

  • t-set ve allowable permutations

    • Her tip seviyesi α’da TTT modelinin elemanları olacak koleksiyon oluşturulur; buna t-set denir
    • Aynı zamanda t-set’ler üzerinde etki eden permütasyon grubu olan allowable permutations kurulur
    • Üyelik ilişkisi, allowable permutations etkisi altında korunur
    • Her t-set’in allowable permutations etkisine göre bir support’a sahip olması sağlanır
    • support, addresses adı verilen nesnelerin small bir kümesidir
    • Bir allowable permutation support’un tüm elemanlarını sabitliyorsa, o t-set’i de sabitler

  • Preferred extension ile dışsallığı sağlama

    • Her seviye α’daki t-set, β < α olan bir tipin preferred extension’ına sahiptir
    • t-set’in elemanlarından hangi extension’ın tercih edildiği geri kazanılabilir; diğer daha düşük tiplerdeki extension’lar bu β-extension’dan türetilir
    • Bu yapı, TTT’nin dışsallık aksiyomunu karşılamak için kullanılır

  • Tip boyutunu kontrol etme

    • Her α tipi, tüm β < α tiplerinin boyutunun tam olarak μ olduğu varsayımı gibi koşullar altında kurulabilir
    • Seviye α’daki t-set koleksiyonunun boyutunun en az μ olduğunu kanıtlamak kolay olduğundan, en fazla μ olduğunu göstermek gerekir
    • Bunun için allowable permutations etkisi altında tangles için temelde farklı çok fazla betimleme olmadığını gösterirler
    • Bu adımda allowable permutations kurmayı sağlayan teknik yardımcı lemma olan freedom of action theorem gerekir
    • Bu bölümün ana sonucu ConNF.mk_tSet içinde yer alır

  • İndüksiyonun tamamlanması ve aksiyomların kontrolü

    • Yukarıdaki süreç özyinelemeli olarak yürütülerek tüm tip seviyeleri α için tangles’ın tipi oluşturulur
    • Küme teorisinde kolay bir adım olsa da, gerekli çeşitli indüksiyon varsayımları birbirine bağlı olduğu için tip teorisinde çok fazla çalışma gerektirir
    • Sonrasında, kurulan nesnenin TTT modeli olup olmadığını doğrulamak için teorinin sonlu aksiyomlaştırmasını sağlayıp sağlamadığı kontrol edilir
    • Proje, Hailperin’in NF comprehension scheme için sonlu aksiyomlaştırmasını TTT’nin sonlu aksiyomlaştırmasına dönüştürerek kullanır
    • Sonuç dosyası results file içinde bulunur
    • Bu seçim keyfîdir; hâlihazırda kurulan altyapı kullanılarak başka sonlu aksiyomlaştırmalar da kolayca kanıtlanabilir

İlgili okumalar

1 yorum

 
GN⁺ 2024-04-24
Hacker News yorumları

  • Lean ile yazılmış bir kanıtın hatalı olma riskinin çok düşük olduğunu düşünüyorum.
    Ancak Lean hatalarından bağımsız olarak, hem yazılım doğrulamada hem de matematikte iyi bilinen bir risk var: sonucu doğru okuyup, gerçekten ihtiyaç duyulan önermenin kanıtlanıp kanıtlanmadığını kontrol etmek gerekir.
    Wilshaw'un nihai sonucunu dikkatle okudum ve gerçekten kanıtlanması gereken şeyi kanıtladığına kanaat getirdim.

    • Makale de benzer bir noktaya değiniyor: mathlib'deki ve bu projedeki tüm tanımlar ile teoremler Lean'in güvenilir çekirdeği tarafından denetlendi ve kurduğumuz kanıtın gerçekten doğru olduğu hesaplamalı olarak doğrulandı.
      Ancak Lean, tanımların ve teorem ifadelerinin amaçlanan İngilizce ifadelerle örtüşüp örtüşmediğini kontrol edemez; bu yüzden bu projenin kodundan sonuç çıkarırken İngilizceyle çeviri konusunda dikkatli olmak gerekir.

    • Benim bahsettiğim sorun, kütüphanelerle ilgili endişeyle bağlantılı: Tanımlanmış bir kavram kullanıyorsanız, o tanımın doğru olduğundan, yani gerçekten ihtiyaç duyulan şeyin kanıtlandığından emin olmanız gerekir.
      Wilshaw'un formelleştirmesi kütüphane kullanmış olsa da bu itiraza açık değil. Kanıtlanan şey, tanımlanmış belirli bir kavramın birinci dereceden mantık formüllerinin belirli bir demetini sağladığı; böyle formülleri sağlayan bir yüklem varsa NF'nin tutarlı olduğudur.

    • Bir başka risk de Lean'in kendisindeki hatalar. Teorem kanıtlayıcılarda bunun emsali yok değil 1.
      Tesadüfen böyle bir şeye basmak zor olabilir, ama 3'te olduğu gibi rastgele kişilerin adımları doldurduğu büyük ölçekli işbirlikleri giderek büyüyor. Birinin bulduğu bir hatayla bir adımı doldurup sabotaj yapması endişe edilecek bir durum hâline gelebilir.

    • Temeller kuramı açısından, bu kanıtın NF ile Lean çekirdeği arasındaki eş-tutarlılığa dair bir kanıt olması da önemli. Lean çekirdeğinin kendisi insanlar tarafından inceleniyor.
      Mekanikleştirilmiş teorem kanıtlayıcılar, insanlar ya da başka dış sistemler tarafından enjekte edilen doğruluk düzeyini koruyan bir yöntemdir.

  • Yanılmıyorsam bu, yıllardır belirsiz durumda kalan zor bir kanıtın statüsünün bir kanıt asistanı ile netleştirildiği ilk örnek gibi görünüyor.
    Coq'taki dört renk teoremi gibi, güvenilmeyen yazılımın büyük bir hesaplama bileşenini üstlendiği mevcut kanıtları doğrulayan projeler olmuştu; ama daha geniş matematik topluluğunda sonucun epistemolojik statüsünün bizzat belirsiz olduğu bir durum sanırım ilk kez yaşanıyor.

  • “New Foundations” küme teorisi formelleştirmesini diğer formelleştirmelerle karşılaştırınca özel ya da yeni kılan şeyin ne olduğunu kabaca açıklayabilir misiniz?
    Ya da matematik lisans öğrencisinin veya mühendislik uzmanının okuyabileceği bir açıklama bağlantısı da olur.

    • Az önce Wikipedia maddesini düzenledim; artık biraz daha okunabilir olmalı: https://en.wikipedia.org/wiki/New_Foundations
      Bence kilit nokta evrensel kümenin varlığı. Benim kullanım alanım olan programlama dillerinin tip sistemlerinde böyle bir evrensel küme çok yararlı.
      Mevcut sistemlerdeki kümülatif evrenler veya type-in-type gibi çeşitli dolambaçlı çözümler tatmin edici değil. Bunun yerine, yalnızca tip imzalarının katmanlaştırılmış olup olmadığını kontrol edip, tiplerin sayısal seviyeleri olduğu gerçeğini unutabilirsiniz.
    • NF'de estetik açıdan gerçekten hoşuma giden şey, “tüm kümelerin kümesi”nin Russell paradoksuna yol açmaması için altküme seçme aksiyomunu ayarlama biçimi.
      Temelde, altküme seçmek için kullanılan yüklemin çok hafif bir tip sistemine uymasını şart koşuyor. “x kendi kendisinin elemanı değildir” makul bir tip sisteminde iyi tiplendirilmiş bir soru değildir; özellikle NF'nin “katmanlaştırılabilirlik” şartını da sağlamaz. Bu yüzden, kendi kendini içermeyen tüm kümelerin kümesi olan Russell paradoksu kümesini oluşturamazsınız.
    • NF'nin “iyi” yanlarından biri, yalnızca iki aksiyom/aksiyom şeması olması: 1) aynı elemanlara sahip kümeler aynıdır, 2) herhangi bir katmanlaştırılabilir özellik için, o özelliğe sahip olan her şeyin bir kümesi karşılık gelir.
      “Katmanlaştırılabilir” tanımı da pek karmaşık değil. Buna karşılık ZF'de epey geçici çözüm gibi görünen sekiz aksiyom/aksiyom şeması var.

  • Coq ile Lean arasındaki temel farkın ne olduğunu, aynı tür mantık üzerinde çalışıp çalışmadıklarını merak ettiğim için bu yazıyı buldum 1.
    Oradaki tartışmayı neredeyse hiç anlamadım ve ikisini de pratikte kullanmıyorum. Bu konuda daha fazla açıklama ya da başka kanıt asistanlarıyla karşılaştırma varsa duymak isterim.

    1 https://proofassistants.stackexchange.com/questions/153/what...

  • Lean savunucularının ifadeleri biraz abartılı kullandığını düşünüyorum. Lean, çoğu zaman ima edildiği gibi daha üstün bir ispat yöntemi değil, alternatif bir ispat biçimi
    Lean öğrenmeye kalkınca kısa sürede fark ediliyor: Kendi hataları olabilen bir programlama dili ve sistem; ayrıca başka insanların yazdığı çeşitli kütüphane katmanlarına büyük ölçüde dayanıyor. Bu kütüphanelerde tercihler var; boşluklar veya hatalar da olabilir
    Bu yüzden “Lean bu ispatın doğru olduğunu söyledi” türü ifadelere itirazım var. Bence daha doğru ve dürüst ifade şu: Yazılan ispat insan matematikçiler tarafından doğrulandı; ardından bir insan bu ispatı Lean’e çevirdi ve orada da doğrulandı. Lean’in tek altın doğrulamayı sağladığını söylemek tam olarak doğru olmayabilir; en azından bunun böyle olduğuna dair bir açıklama görmedim. Alt başlıktaki “Randall Holmes ispatının dijitalleştirilmesi” en doğru ifade gibi duruyor

    • Lean gibi güçlü bir sistemde makine tarafından doğrulanmış bir ispatın, yalnızca insanlar tarafından doğrulanmış bir ispattan çok daha üstün olduğunu düşünüyorum. İnsanlar hayret verici, ama sıkılabiliyor ve ayrıntıları kaçırabiliyorlar
      Bu yalnızca teorik bir iddia değil. İnsanlar Euclid’in Elemanlar’ını iki bin yılı aşkın süre okuduktan sonra eksik aksiyomu fark etti. Düzgün çalışan bir makine ispat doğrulama sistemi bunu hemen ortaya çıkaracak kadar temel bir hataydı
      Yayımlanmış matematik ispatlarının sonradan yanlış çıktığı da sık görülüyor. Matematik giderek daha incelikli hale geldikçe, insanların tüm adımları doğru biçimde doğrulaması giderek zorlaşıyor. Makineler ispat üretmede henüz insanlar kadar iyi değil, ama doğrulamada rakipsizler
      Lean ile “rekabet eden” sistemler de var; bu yüzden Lean’in “tek gerçek yol” olduğunu söylemem. Örneğin Metamath’i de seviyorum. Yine de bu sistemler arasındaki “rekabet” için tırnak işareti gerekiyor. Her birinin artıları ve eksileri farklı; birden fazla sistemi seven, kullanan veya katkı veren çok kişi var. Hepsi teoremleri insanlar için gerçekçi olmayan bir titizlik düzeyinde doğrulayabiliyor

    • Hatalar olabilir, ama anladığım kadarıyla güvenilmesi gereken tek şey çekirdek
      “Başka insanların yazdığı çeşitli kütüphane katmanları” ile mathlib kastediliyorsa, bunun doğru olmadığını düşünüyorum. Çünkü mathlib kodu da nihayetinde çekirdeğin işlediği koda derleniyor
      Web sitesindeki makale taslağı 0 da bu noktayı güçlendiriyor: Lean büyük bir proje, ancak kabul edilen bir ispatın doğru olduğunu garanti etmek için yalnızca çekirdeğe güvenmek yeterli. Bir taktik yanlış bir ispat terimi üretse bile, çekirdeğin ispatı kabul etmeden önce bu hatayı yakalama fırsatı var

    • Fark şu: Lean’de yalnızca çekirdeğe güvenmek yeterli. Geri kalan her şey onun üzerine kuruluyor. Çekirdek sağlamsa diğer her şey de sağlam
      Bu, genel amaçlı programlama dillerinden oldukça farklı. Genel dillerde her an hata girebilir. Ayrıca herhangi bir yardımcı teoremin hata barındırabileceği matematikten de epey farklı

    • Teorem ispatlayıcılarının harika yanı, çekirdeğin doğru olduğu varsayımıyla yanlış ispatın derlenememesi
      İspat söz konusu olduğunda, geleneksel yazılımdaki gibi yalnızca çalışma zamanında ortaya çıkan hatalar yok. Çünkü çalışma zamanı diye bir şey yok
      Lean’i “normal” bir programlama dili olarak da kullanabilirsiniz; o zaman çalışma zamanı hatası riski olur, ama burada söz konusu olan bu değil

    • Teorem ispatlayıcılarını yanlış anlıyorsunuz. Bu, “tüm soyutlamalar sızdırır” düzeyinde bir mesele değil. Kütüphanelere güvenmeniz gerekmiyor; yalnızca çekirdeğe güvenmek yeterli
      Çekirdeğe güvenmek de önemsiz değil, ama biçimsel olmayan ispatlara kıyasla büyük bir sıçrama. Biçimsel olmayan ispatlarda gerçekten de “kütüphane”ye, yani kültüre ve başkalarının bilgisine güvenmek zorundasınız. Çünkü pratikte aksiyomlara kadar indirmenin bir yolu yok

  • ZFC öldü, yaşasın NF mi?
    Kümeleri çoğunlukla başka şeyleri açıklamak için ortak bir dil olarak kullanan amatör bir matematikçi olarak, bunun daha geniş matematik alanı için ne anlama geldiğinden pek emin değilim. Özellikle NF’nin kullanışlılığı mevcut ZFC ve türevlerine benziyorsa
    Makine ispatlarında NF’nin ZFC kadar popüler olmasını beklemeli miyiz? Evrensel kümenin varlığı daha sezgisel geliyor; en azından bu ispat sayesinde biçimselleştirmeye yönelik kişisel ilgim yeniden canlandı

    • Saf bir amatör bakış açısından, her ZFC modelinin bir NF modeline genişletilebilmesi nedeniyle göreli tutarlılık sonucunun NF’yi en az ZFC kadar kullanışlı kıldığını düşünüyorum
      Ama aşağıdakilerden biri olmadığı sürece NF’nin çok daha kullanışlı hale geleceğini sanmıyorum

      1. NF’nin çelişkili olduğu kanıtlanır. O zaman ZFC de çelişkilidir. Gece göğündeki yıldızlar birer birer sönmeye başlar ;)

      2. ZFC’nin çelişkili olduğu kanıtlanır. O zaman NF’nin tutarlı olma ihtimali hâlâ kalır. Şansa ihtiyacımız olur

      Elbette doğru sınıflar hakkında konuşabilmek ya da katmanlandırılmış formüllerle Russell paradoksundan kaçınmak gibi NF’nin daha pratik “yaşam kalitesi” avantajlarını kaçırıyor olmam oldukça mümkün

    • NF’yi bağımsız bir temel sistem olarak öne sürme niyeti kesinlikle yok. NF oldukça tuhaf bir sistem
      Yine de biri bunu savunmak isterse, bu tutarlılık sonucu en azından ZFC’de bir çelişkiye ulaşma riskinden daha büyük bir risk olmadığını söylemek için kullanılabilir

  • Bunu gerçekten çok sevdim
    Sonunda işbirlikçi ispatlara ve “hata düzeltmeye” evrilip matematiğin GitHub’daki koda benzer bir sürece dönüşüp dönüşmeyeceğini merak ediyorum

  • mathlib projesini takip edecek boş zamanım olsaydı keşke. Gerçekten harika
    Çok gevşek biçimde de olsa katılmanın bir yolu var mı?

  • Bu alanın insanı değilim ama yeterince güçlü her sistemin kendi tutarlılığını gösteremeyeceğini söyleyen Gödel teoremi yok muydu?

    • Muhtemelen düşündüğün şey Gödel’in eksiklik teoremleri: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
      Ancak X sistemi kendi tutarlılığını kanıtlayamazken, daha güçlü bir Y sistemi X’in tutarlılığını kanıtlayabilir. Ve daha güçlü başka bir sistem de Y’nin tutarlılığını kanıtlayabilir. Böylece her sistemin daha zayıf bir sistemin tutarlılığını kanıtladığı bir zincir oluşur
      Bu, o sistemin mutlak anlamda tutarlı olduğunu kanıtlamaz. Çünkü Y çelişkiliyse hem X’in tutarlı olduğunu hem de X’in çelişkili olduğunu kanıtlayabilir. Yine de değerlidir. Sonuçta Y’yi kullanmamızın nedenlerinden biri, onun içinde bir çelişki bilmiyor olmamızdır. Biçimsel sistemler çoğu zaman ince bir şekilde çelişkili olabilir; bu yüzden “başka bir sistemin tutarlı olduğu varsayımı altında tutarlı” olmak, “hiç tutarlılık kanıtı olmaması”ndan çok daha iyidir
    • Burada sistem kendi tutarlılığını kanıtlamıyor. Tutarlılık başka, daha güçlü bir sistemde kanıtlanıyor
    • İlginç olan şu: güçlü bir sistem kendi tutarlılığını kanıtlayabilse bile, bu tek başına bize hiçbir şey söylemez
      Çelişkili bir sistem de kendi tutarlılığını kanıtlayabilir. Dolayısıyla bir sistemin kendisinin tutarlı olduğuna dair bir kanıtı olsa bile, gerçekten tutarlı olup olmadığını hâlâ bilemeyiz
    • Bu kanıtı “Lean 4 tutarlıysa New Foundations da tutarlıdır” diye anlamak yeterli. Gödel’in eksiklik teoremleriyle çelişmez
    • Buradaki sistem, kendi temel varsayımlarını kanıtlamaya çalışmaktan ziyade mevcut varsayımlar kümesinin üzerine inşa ediliyor gibi görünüyor. Aklındaki teorem muhtemelen uygulanmaz

  • Oluşturanlardan birinin katıldığı Reddit tartışması da görülmeye değer 0

    https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...