Skolem normal formu - Skolem normal form

Olarak matematiksel mantık , bir formül bir birinci dereceden mantık olan Skolem normal formda bu ise prenex normal formda yalnızca genel birinci dereceden Nicelik .

Her birinci dereceden formül , Skolemization adı verilen bir işlemle (bazen yazılan Skolemnization ) tatmin edilebilirliğini değiştirmeden Skolem normal formuna dönüştürülebilir . Ortaya çıkan formül mutlaka orijinal formülle eşdeğer değildir , ancak onunla eşitleştirilebilir : ancak ve ancak orijinal formül tatmin edici ise tatmin edicidir .

Skolem normal biçime indirgenmesi çıkarılması için bir yöntemdir varoluş nicelik gelen formel mantık genellikle ilk aşama olarak gerçekleştirilmektedir ifadeleri, otomatik teoremi prover .

Örnekler

Skolemization'ın en basit biçimi, evrensel bir niceleyicinin kapsamı içinde olmayan varoluşsal olarak nicelendirilmiş değişkenler içindir . Bunlar basitçe yeni sabitler oluşturularak değiştirilebilir. Örneğin, şekilde değiştirilebilir , burada yeni bir sabit (formül içinde başka bir yerde meydana gelmez gibi). ${\ displaystyle \ var xP (x)}$${\ displaystyle P (c)}$${\ displaystyle c}$

Daha genel olarak, Skolemization, varoluşsal olarak ölçülen her değişkeni , fonksiyon sembolü yeni olan bir terimle değiştirerek gerçekleştirilir . Bu terimin değişkenleri aşağıdaki gibidir. Formül prenex normal formundaysa , evrensel olarak ölçülen ve niceleyicileri ondan önce gelen değişkenlerdir . Genel olarak, evrensel olarak ölçülen değişkenlerdir (sırayla varoluşsal niceleyicilerden kurtulduğumuzu varsayıyoruz, bu nedenle daha önce tüm varoluşsal niceleyiciler kaldırıldı) ve nicelik belirteçlerinin kapsamında meydana gelen böyle . Bu süreçte tanıtılan işleve bir Skolem işlevi (veya sıfır ariteye sahipse Skolem sabiti ) ve terime Skolem terimi denir . ${\ displaystyle y}$${\ displaystyle f (x_ {1}, \ ldots, x_ {n})}$${\ displaystyle f}$${\ displaystyle x_ {1}, \ ldots, x_ {n}}$${\ displaystyle y}$${\ displaystyle \ var y}$${\ displaystyle \ var y}$${\ displaystyle f}$

Örnek olarak, formül Skolem normal formunda değildir çünkü varoluşsal niceleyiciyi içerir . Skolemization yerini ile nerede, yeni bir işlev simgesi olduğunu ve üzerinde kantifikasyonunu kaldırır . Ortaya çıkan formül . Skolem terimi içerir , ancak kaldırılacak nicelik, çünkü kapsamında olup ancak bu olarak ; Bu formül prenex normal formunda olduğundan, bu, nicelik belirteçleri listesinde, bundan önce gelirken olmadığının söylenmesi ile eşdeğerdir . Bu dönüşümle elde edilen formül, ancak ve ancak orijinal formül doğru ise tatmin edilebilir. ${\ displaystyle \ forall x \ var y \ forall zP (x, y, z)}$${\ displaystyle \ var y}$${\ displaystyle y}$${\ displaystyle f (x)}$${\ displaystyle f}$${\ displaystyle y}$${\ displaystyle \ forall x \ forall zP (x, f (x), z)}$${\ displaystyle f (x)}$${\ displaystyle x}$${\ displaystyle z}$${\ displaystyle \ var y}$${\ displaystyle \ forall x}$${\ displaystyle \ forall z}$${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle z}$

Skolemization nasıl çalışır?

Skolemization, birinci dereceden tatminkarlık tanımına bağlantılı olarak ikinci dereceden bir denklik uygulayarak çalışır . Eşdeğerlik, varoluşsal niceleyiciyi evrensel olandan önce "hareket ettirmek" için bir yol sağlar.

${\ displaystyle \ forall x {\ Büyük (} R (g (x)) \ vee \ var yR (x, y) {\ Büyük)} \ iff \ var f \ forall x {\ Büyük (} R (g ( x)) \ vee R (x, f (x)) {\ Büyük)}}$

nerede

${\ displaystyle f (x)}$ eşleştiren bir fonksiyondur için . ${\ displaystyle x}$${\ displaystyle y}$

Sezgisel, cümle "her için bir vardır böyle eşdeğer forma dönüştürülür" "bir işlev vardır her haritalama bir içine her için, böyle o tutan ". ${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle R (x, y)}$${\ displaystyle f}$${\ displaystyle x}$${\ displaystyle y}$${\ displaystyle x}$${\ displaystyle R (x, f (x))}$

Bu eşdeğerlik yararlıdır, çünkü birinci dereceden tatmin edilebilirliğin tanımı, işlev sembollerinin değerlendirilmesi üzerinde dolaylı olarak varoluşsal olarak nicelendirir. Özel olarak, bir birinci dereceden, formül bir model vardır ise kabul edilebilirdir ve bir değerlendirme için aşağıdaki formüle değerlendirmek formülünün serbest değişkenlerin gerçek . Model, tüm fonksiyon sembollerinin değerlendirmesini içerir; bu nedenle, Skolem işlevleri dolaylı olarak varoluşsal olarak ölçülür. Yukarıdaki örnekte, bir model vardır, ancak ve ancak karşılanabilir olduğu için değerlendirilmesini içermektedir, örneğin, serbest değişkenleri (bu durumda yok) arasında bir değerlendirme için de geçerlidir. Bu, ikinci sırada olarak ifade edilebilir . Yukarıdaki denklik ile bu, tatmin edilebilirliği ile aynıdır . ${\ displaystyle \ Phi}$${\ displaystyle M}$${\ displaystyle \ mu}$${\ displaystyle \ forall xR (x, f (x))}$${\ displaystyle M}$${\ displaystyle f}$${\ displaystyle \ forall xR (x, f (x))}$${\ displaystyle \ vardır f \ forall xR (x, f (x))}$${\ displaystyle \ forall x \ var yR (x, y)}$

Meta düzeyinde, bir formülün birinci dereceden tatmin edilebilirliği , bir modelin nerede olduğu , serbest değişkenlerin bir değerlendirmesidir ve altında doğru olduğu anlamına geldiğinden , küçük bir notasyon kötüye kullanımı ile yazılabilir . Birinci dereceden modeller tüm işlev simgelerinin değerlendirmesini içerdiğinden, içeren herhangi bir Skolem işlevi örtük olarak varoluşsal olarak ölçülür . Sonuç olarak, varoluşsal niceleyicileri, formülün önündeki fonksiyonlar yerine varoluşsal niceleyicilerle değişkenler yerine değiştirdikten sonra, formül yine de bu varoluşsal niceleyiciler kaldırılarak birinci dereceden bir formül olarak ele alınabilir. İşlevler, birinci dereceden tatminkarlık tanımında dolaylı olarak varoluşsal olarak ölçüldüğü için tamamlanmış gibi muamele etmenin bu son adımı tamamlanabilir . ${\ displaystyle \ Phi}$${\ displaystyle \ var M \ var \ mu ~. ~ (M, \ mu \ modeller \ Phi)}$${\ displaystyle M}$${\ displaystyle \ mu}$${\ displaystyle \ modelleri}$${\ displaystyle \ Phi}$${\ displaystyle M}$${\ displaystyle \ mu}$${\ displaystyle \ Phi}$${\ displaystyle \ var M}$${\ displaystyle \ vardır f \ forall xR (x, f (x))}$${\ displaystyle \ forall xR (x, f (x))}$${\ displaystyle \ var M}$

Skolemization'ın doğruluğu aşağıdaki örnek formülde gösterilebilir . Bu formül bir model tarafından ancak ve ancak , modelin etki alanındaki olası her değer için , modelin etki alanında doğru yapan bir değer varsa sağlanır . By Seçim aksiyomu , bir işlev vardır öyle . Bunun bir sonucu olarak, formül bunun değerlendirilmesine eklenmesi ile elde edilen modeli, çünkü, karşılanabilir olduğu için . Bu, ancak tatmin edici ise tatmin edilebilir olduğunu gösterir . Tersine, eğer tatmin edici ise, o zaman onu tatmin eden bir model vardır; bu model, işlevin her değeri için formülün geçerli olacağı şekilde bir değerlendirme içerir . Sonuç olarak, aynı model tarafından tatmin edilir, çünkü değerin her değeri için , değerin nerede değerlendirileceğini seçebilir . ${\ displaystyle F_ {1} = \ forall x_ {1} \ noktalar \ forall x_ {n} \ var yR (x_ {1}, \ noktalar, x_ {n}, y)}$ ${\ displaystyle M}$${\ displaystyle x_ {1}, \ noktalar, x_ {n}}$${\ displaystyle y}$${\ displaystyle R (x_ {1}, \ noktalar, x_ {n}, y)}$${\ displaystyle f}$${\ displaystyle y = f (x_ {1}, \ noktalar, x_ {n})}$${\ displaystyle F_ {2} = \ forall x_ {1} \ dots \ forall x_ {n} R (x_ {1}, \ dots, x_ {n}, f (x_ {1}, \ dots, x_ {n }))}$${\ displaystyle f}$${\ displaystyle M}$${\ displaystyle F_ {1}}$${\ displaystyle F_ {2}}$${\ displaystyle F_ {2}}$${\ displaystyle M '}$${\ displaystyle f}$${\ displaystyle x_ {1}, \ noktalar, x_ {n}}$${\ displaystyle R (x_ {1}, \ noktalar, x_ {n}, f (x_ {1}, \ noktalar, x_ {n}))}$${\ displaystyle F_ {1}}$${\ displaystyle x_ {1}, \ ldots, x_ {n}}$${\ displaystyle y = f (x_ {1}, \ noktalar, x_ {n})}$${\ displaystyle f}$${\ displaystyle M '}$

Skolemization Kullanımları

Skolemization'ın kullanımlarından biri otomatik teorem kanıtlamadır . Örneğin, analitik tablo yönteminde , önde gelen nicelleştiricisi varoluşsal olan bir formül ortaya çıktığında, Skolemization yoluyla bu niceleyicinin kaldırılmasıyla elde edilen formül üretilebilir. Örneğin , serbest değişkenlerin olduğu bir tabloda ortaya çıkarsa , o zaman tablonun aynı dalına eklenebilir. Bu ilave, tablonun tatmin edilebilirliğini değiştirmez: eski formülün her modeli , yeni formülün bir modeline uygun bir değerlendirme eklenerek genişletilebilir . ${\ displaystyle \ var x. \ Phi (x, y_ {1}, \ ldots, y_ {n})}$${\ displaystyle x, y_ {1}, \ ldots, y_ {n}}$${\ displaystyle \ Phi (x, y_ {1}, \ ldots, y_ {n})}$${\ displaystyle \ Phi (f (y_ {1}, \ ldots, y_ {n}), y_ {1}, \ ldots, y_ {n})}$${\ displaystyle f}$

Skolemization'ın bu formu, sadece formülde serbest olan değişkenlerin Skolem terimine yerleştirilmesi bakımından "klasik" Skolemization'a göre bir gelişmedir. Bu bir gelişmedir çünkü tablonun anlambilimi formülü dolaylı olarak formülün kendisinde olmayan bazı evrensel niceliklendirilmiş değişkenlerin kapsamına yerleştirebilir; bu değişkenler Skolem teriminde değildir, ancak Skolemization'ın orijinal tanımına göre orada olurlar. Kullanılabilecek diğer bir iyileştirme, değişken yeniden adlandırmaya kadar özdeş olan formüller için aynı Skolem işlevi sembolünü uygulamaktır .

Diğer bir kullanım, birinci dereceden mantık için çözümleme yönteminde , formüllerin evrensel olarak nicelendirildiği anlaşılan cümle kümeleri olarak temsil edilmesidir. (Bir örnek için içici paradoksuna bakın .)

Skolem teorileri

Genel olarak, bir teoriyse ve serbest değişkenli her formül için , kanıtlanabilir bir şekilde Skolem fonksiyonu olan bir fonksiyon sembolü varsa , o zaman Skolem teorisi olarak adlandırılır . ${\ displaystyle T}$ ${\ displaystyle x_ {1}, \ noktalar, x_ {n}, y}$${\ displaystyle F}$${\ displaystyle y}$${\ displaystyle T}$

Her Skolem teorisi model tamamlanmıştır , yani bir modelin her altyapısı temel bir altyapıdır . Bir Skolem teorisi T'nin bir M modeli verildiğinde , belirli bir A kümesini içeren en küçük alt yapı , A'nın Skolem gövdesi olarak adlandırılır . Arasında Skolem gövde A bir olan atom asal modeli üzerinde A .

Tarih

Skolem normal formu, adını geç Norveçli matematikçi Thoralf Skolem'den almıştır .

Ayrıca bakınız

• Herbrandization , Skolemization'ın ikili
• Functor mantığını tahmin et

Notlar

Referanslar

• Hodges, Wilfrid (1997), A Shorter Model Theory , Cambridge University Press , ISBN   978-0-521-58713-6 CS1 Maint: önerilmeyen parametre ( bağlantı )

Dış bağlantılar

• "Skolem işlevi" , Matematik Ansiklopedisi , EMS Press , 2001 [1994]
• PlanetMath.org'da Skolemization
• Skolemization , Hector Zenil, The Wolfram Gösteriler Projesi .
• Weisstein, Eric W. "SkolemizedForm" . MathWorld .