10.12: Резюме
- Page ID
- 52840
Теорема повноти - це зворотна теорема про обґрунтованість. В одній формі він стверджує, що якщо\(\Gamma \Entails A\) потім\(\Gamma \Proves A\), в іншій,\(\Gamma\) що якщо послідовний, то він задовольняється. Ми довели другу форму (і вивели першу з другої). Доказ бере участь і вимагає виконання ряду кроків. Починаємо з послідовного набору\(\Gamma\). Спочатку ми додаємо нескінченно багато нових постійних символів, а\(c_i\) також формули виду,\(\lexists{x}{A(x)} \lif A(c)\) де кожна формула\(A(x)\) з вільною змінною в розширеній мові поєднується з однією з нових констант. Це призводить до насиченого послідовного набору пропозицій, що містять\(\Gamma\). Це все ще послідовно. Тепер ми беремо цей набір і розширюємо його до повного узгодженого набору. Повний послідовний набір має властивість nice, що для будь-якого речення\(A\), або\(A\) або\(\lnot A\) є в множині (але ніколи не обидва). Оскільки ми починали з насиченого набору, тепер у нас є насичений, повний, послідовний набір пропозицій,\(\Gamma^*\) який включає\(\Gamma\). З цього набору тепер можна визначити\(\Struct{M}\) таку структуру, що\(\Sat{M(\Gamma^*)}{A}\) iff\(A \in \Gamma^*\). Зокрема\(\Sat{M(\Gamma^*)}{\Gamma}\), тобто\(\Gamma\) є задовільним. Якщо\(=\) є, то конструкція трохи складніше.
З теореми про повноту випливають два важливі наслідки. Теорема компактності стверджує, що\(\Gamma \Entails A\) iff\(\Gamma_0 \Entails A\) для деяких скінченних\(\Gamma_0 \subseteq \Gamma\). Еквівалентним формулюванням\(\Gamma\) є те, що задовольняється, якщо кожен\(\Gamma_0 \subseteq \Gamma\) скінченний є задовільним. Теорема компактності корисна для доказу існування структур з певними властивостями. Наприклад, ми можемо використовувати його, щоб показати, що існують нескінченні моделі для кожної теорії, яка має довільно великі кінцеві моделі. Це означає, зокрема, що кінцевість не може бути виражена в логіці першого порядку. Другий наслідок, теорема Левенгейма-Сколема, стверджує, що кожен задоволений\(\Gamma\) має підрахункову модель. Це, в свою чергу, показує, що незліченність не може бути виражена в логіці першого порядку.