Zgodność pierwszego rzędu bez modeli skończonych

Wiemy z twierdzenia Kościoła, że określenie satysfakcji pierwszego rzędu jest ogólnie nierozstrzygalne, ale istnieje kilka technik, które można zastosować do ustalenia satysfakcji pierwszego rzędu. Najbardziej oczywiste jest poszukiwanie modelu skończonego. Istnieje jednak szereg instrukcji w logice pierwszego rzędu, które możemy wykazać, że nie mają modeli skończonych. Na przykład każda dziedzina, w której działa funkcja iniekcyjna i nieinwazyjna, jest nieskończona.

Jak wykazujemy satysfakcję dla instrukcji pierwszego rzędu, gdy nie ma modeli skończonych lub istnienie modeli skończonych jest nieznane? W automatycznym dowodzeniu twierdzeń możemy określić satysfakcję na kilka sposobów:

Możemy zanegować zdanie i poszukać sprzeczności. Jeśli taki zostanie znaleziony, potwierdzamy ważność oświadczenia pierwszego rzędu, a tym samym jego satysfakcję.
Używamy nasycenia z rozdzielczością i zabrakło wnioskowania. Najczęściej będziemy mieć nieskończoną liczbę wniosków, więc nie jest to niezawodne.
Możemy zastosować wymuszenie, które zakłada istnienie modelu, a także spójność teorii.

Nie znam nikogo, kto wdrażałby forsowanie jako zmechanizowaną technikę automatycznego dowodzenia twierdzeń i nie wygląda to łatwo, ale interesuje mnie to, czy zostało to zrobione czy usiłowane, ponieważ zostało wykorzystane do udowodnienia niezależności w wielu stwierdzeniach w teorii mnogości, która sama nie ma modeli skończonych.

Czy znane są inne techniki wyszukiwania spełniania pierwszego rzędu, które mają zastosowanie do automatycznego rozumowania, czy też ktoś pracował nad algorytmem automatycznego wymuszania?

reference-request lo.logic automated-theorem-proving

— dezakin
źródło

Podejście Infinox może być odpowiednie dla twojego pytania (bez odpowiedzi). Chodzi o to, aby wykorzystać dowody twierdzeń do wykazania nieistnienia modeli skończonych. Patrz na przykład gupea.ub.gu.se/bitstream/2077/22058/1/gupea_2077_22058_1.pdf

— selig

Oto zabawne podejście Brock-Nannestad i Schürmann:

Prawdziwe monadyczne abstrakcje

Chodzi o to, aby spróbować przełożyć zdania pierwszego rzędu na monadyczną logikę pierwszego rzędu , „zapominając” o niektórych argumentach. Z pewnością tłumaczenie nie jest kompletne : istnieją pewne spójne zdania, które stają się niespójne po tłumaczeniu.

Jednak monadyczna logika pierwszego rzędu jest rozstrzygalna . Można zatem sprawdzić, czy tłumaczenie wzoru jest spójne: $\overline F$ $F$

\bar{F} ⊬ ⊥

$\overline F\not\vdash\bot$

można to sprawdzić za pomocą procedury decyzyjnej i sugeruje

F ⊬ ⊥

$F\not\vdash\bot$

Co implikuje, że ma model według twierdzenia o kompletności. $F$

Temat ten można zastosować nieco bardziej ogólnie: zidentyfikuj rozstrzygającą podlogię swojego problemu, a następnie przełóż na niego swój problem w sposób, który zachowa prawdę. W szczególności nowoczesne solwery SMT, takie jak Z3, stały się zadziwiająco dobre w dowodzeniu spełniania formuł za pomocą kwantyfikatorów (domyślnie , ale mogą dobrze działać na formułach ). $\Sigma^0_1$ $\Pi^0_2$

Obecnie wymuszanie wydaje się być poza zasięgiem zautomatyzowanych metod.

— cody
źródło

Wydaje mi się to zaskakujące. Próbuję sobie wyobrazić przekładanie teorii mnogości NBG na logikę monadyczną, ale nie mogę sobie wyobrazić, że to takie proste. Wyobrażam sobie, że działa dobrze dla prawdziwych zamkniętych pól lub arytmetyki presburgera jako rozstrzygających teorii pierwszego rzędu z modelami skończonymi, ale trudno mi sobie wyobrazić, że działa dla czegoś tak wyrazistego jak teoria mnogości.

— dezakin

Wszystko jest trudne z NGB w automatycznym rozumowaniu. Zauważ, że celem tego artykułu nie jest użycie jednego tłumaczenia, ale wypróbowanie wielu możliwych tłumaczeń w poszukiwaniu modelu.

— cody