Niceleyici Eleme
Niceleyici eleme, bir kuramdaki her formülün niceleyicisiz bir formüle eşdeğer olması özelliğidir; bu, karar prosedürleri ve tanımlanabilir kümelerin net bir tanımını sağlayan güçlü bir yapısal özelliktir.
Tanım
Bir kuram, eğer her formül, kuram modülünde, aynı serbest değişkenlere sahip niceleyicisiz bir formüle eşdeğerse, niceleyici eleme kabul etmektedir; bu da tanımlanabilir kümelerin tam olarak atomik formüllerle tanımlananların Boole birleşimleri olduğu anlamına gelmektedir.
Kapsam
Bu konu, niceleyici elemenin tanımını, bunu tesis etme kriterlerini, model tamlığı ile ilgili kavramı ve yoğun doğrusal sıralamalar, cebirsel olarak kapalı cisimler, reel kapalı cisimler ve Presburger aritmetiği gibi kanonik örnekleri ile bu örneklerin ima ettiği karar verilebilirlik sonuçlarını kapsamaktadır.
Temel sorular
- Bir kuramın formüllerinden niceleyiciler ne zaman sistematik olarak kaldırılabilir?
- Niceleyici eleme, bir yapının tanımlanabilir kümelerini nasıl tanımlar?
- Niceleyici eleme neden sıklıkla karar verilebilirliği sağlar?
- Hangi klasik cebirsel kuramlar niceleyici eleme kabul eder?
Temel kuramlar
- Niceleyici eleme testi
- Atomik ve olumsuz atomik formüllerin birleşimlerinden tek bir varoluşsal niceleyiciyi elemek yeterlidir; bu, özelliği, alt yapıların gömülmeleri aracılığıyla sıklıkla kontrol edilen yönetilebilir bir yerel koşula indirgemektedir.
- Cebirsel ve reel kapalı cisimler
- Cebirsel olarak kapalı cisimler ve reel kapalı cisimler kuramları niceleyici eleme kabul etmektedir; bu nedenle tanımlanabilir kümeleri sırasıyla inşa edilebilir ve yarı-cebirsel kümeler olup, klasik geometriyi yeniden ortaya koymaktadır.
- Tarski karar prosedürü
- Reel kapalı cisimler için niceleyici eleme, sıralı cisimler dilinde reel sayılar hakkındaki herhangi bir birinci dereceden ifadenin doğruluğunu kararlaştıran bir algoritma sağlamaktadır; bu nedenle temel cebir ve geometri karar verilebilirdir.
Klinik önem
Niceleyici eleme, mantıksal soruları cebire dönüştürmektedir: bilgisayar cebiri ve doğrulama alanlarında kullanılan karar prosedürleri sağlamakta ve reel sayılar üzerindeki tanımlanabilir kümelerin yarı-cebirsel doğası gibi geometrik içeriği, model kuramını reel cebirsel geometriye ve o-minimaliteye bağlamaktadır.
Tarihçe
Niceleyici eleme, 1920'ler ve 1930'larda Skolem, Langford ve Presburger tarafından belirli kuramları kararlaştırmak için kullanılmıştır. Tarski ise bunu reel kapalı cisimler için tesis ederek, temel cebir ve geometri için meşhur karar prosedürünü ortaya koymuştur. Robinson, çevreleyen fikirleri model tamlığı aracılığıyla yeniden şekillendirerek, bu tekniği uygulamalı model kuramının temel bir unsuru haline getirmiştir.
Öne çıkan isimler
- Alfred Tarski
- Thoralf Skolem
- Abraham Robinson
- Mojzesz Presburger
İlgili konular
Temel eserler
- marker2002
- hodges1993
- tarski1951
Sıkça sorulan sorular
- Niceleyici eleme bir kuramı neden karar verilebilir kılar?
- Bir cümle serbest değişken içermez, bu nedenle niceleyicilerini elemek, sabitler hakkındaki atomik ifadelerden oluşan niceleyicisiz bir cümle bırakır ve bu cümlenin doğruluğu doğrudan kontrol edilebilir. Eğer eleme etkiliyse, bu, her cümleyi kararlaştırmak için bir algoritma sağlamaktadır.
- Her kuram niceleyici eleme kabul eder mi?
- Hayır. Birçok kuram niceleyici eleme kabul etmemektedir ve bazen bunu elde etmek için dile tanımlanabilir yüklemler eklenebilmektedir. Niceleyici eleme, tanımlanabilir kümelerinin özellikle şeffaf bir tanımına sahip kuramların karakteristik, özel ve faydalı bir özelliğidir.