Jak ustalić, czy dowód wymaga „technik wnioskowania wyższego rzędu”?

15

Pytanie:

Załóżmy, że mam specyfikację problemu składającego się z aksjomatów i celu (tj. Powiązanym problemem dowodowym jest to, czy cel jest zadowalający, biorąc pod uwagę wszystkie aksjomaty). Załóżmy również, że problem nie zawiera żadnych niespójności / sprzeczności między aksjomatami. Czy istnieje sposób na wcześniejsze ustalenie (tj. Bez uprzedniego zbudowania pełnego dowodu), że udowodnienie problemu będzie wymagało „uzasadnienia wyższego rzędu”?

Przez „rozumowanie wyższego rzędu” mam na myśli stosowanie kroków dowodowych, które wymagają zapisania logiki wyższego rzędu. Typowym przykładem „rozumowania wyższego rzędu” może być indukcja: spisanie schematu indukcji wymaga zasadniczo użycia logiki wyższego rzędu.

Przykład:

Można określić problem dowodowy „Czy dodawanie dwóch liczb naturalnych jest przemienne?” używając logiki pierwszego rzędu (tj. zdefiniuj liczbę naturalną za pomocą konstruktorów zero / succ wraz ze standardowymi aksjomatami wraz z aksjomatami, które rekurencyjnie definiują funkcję „plus”). Udowodnienie tego problemu wymaga wprowadzenia do struktury pierwszego lub drugiego argumentu „plus” (w zależności od dokładnej definicji „plus”). Czy mógłbym to wiedzieć, zanim spróbuję to udowodnić, np. Analizując naturę problemu wejściowego ...? (Oczywiście jest to tylko prosty przykład w celach ilustracyjnych - w rzeczywistości byłoby to interesujące w przypadku trudniejszych problemów dowodowych niż przemiana plus.)

Więcej kontekstu:

W swoich badaniach często próbuję zastosować zautomatyzowane dowody twierdzeń pierwszego rzędu, takie jak Wampir, eprover itp., Aby rozwiązać problemy dowodowe (lub części problemów dowodowych), z których niektóre mogą wymagać uzasadnienia wyższego rzędu. Często dowódcy potrzebują sporo czasu, aby wymyślić dowód (pod warunkiem, że istnieje dowód, który wymaga jedynie technik rozumowania pierwszego rzędu). Oczywiście, próba zastosowania prover twierdzenia pierwszego rzędu do problemu, który wymaga rozumowania wyższego rzędu, zwykle powoduje przekroczenie limitu czasu.

Dlatego zastanawiałem się, czy są jakieś metody / techniki, które mogą z góry powiedzieć, czy problem dowodowy będzie wymagał technik rozumowania wyższego rzędu (co oznacza: „nie marnuj czasu na próby przekazania go osobie twierdzącej pierwszego rzędu” ) lub nie, przynajmniej może w przypadku określonych problemów z danymi wejściowymi.

Poszukałem w literaturze odpowiedzi na moje pytanie i zapytałem o to innych badaczy z obszaru twierdzenia - ale jak dotąd nie otrzymałem dobrych odpowiedzi. Oczekuję, że będą jakieś badania na ten temat od ludzi, którzy próbują połączyć interaktywne dowodzenie twierdzeń i automatyczne dowodzenie twierdzeń (społeczność Coq? Społeczność Isabelle (Sledgehammer)?) - ale jak dotąd nic nie znalazłem.

Myślę, że ogólnie problem, który tu opisałem, jest nierozstrzygalny (prawda?). Ale może są dobre odpowiedzi na wyrafinowane wersje problemu ...?

automated-theorem-proving program-verification Sylvia Grewe
źródło
2
To, o co pytasz, zasadniczo decyduje, czy daną formułę da się udowodnić (w twoim słabszym systemie), co jest ogólnie nierozstrzygalne nawet w przypadku prostej teorii takiej jak Q. Ale udowodnienie jest w rzeczywistości niezbyt przydatne, ponieważ silniejsza teoria może skrócić dowody twierdzenia a los. Decyzja, czy twierdzenie ma krótki dowód, jest NP-kompletna. Wątpię, by istniała dobra heurystyka.
Kaveh
2
Arytmetyka Peano ma indukcję, a arytmetyka Peano jest pierwszego rzędu (tj. Kwantyfikuje tylko jednostki). To samo dla ZFC. Cytując Martina Davisa: „Logika wyższego rzędu to tylko notacyjne warianty zestawów teorii sformalizowane w logice pierwszego rzędu, pytanie o zastosowanie formalizmu wyższego rzędu w mechanicznym dowodzeniu twierdzeń jest po prostu kwestią tego, czy takie formalizacje sugerują, czy nie przydatne algorytmy ”.
Martin Berger,
@MartinBerger Myślę, że do celów tego pytania schematy aksjomatów liczą się jako „techniki wnioskowania wyższego rzędu”
fread2281,
@ fread2281 Pomocna jest ostrożność z terminologią. Istnieją teorie zestawów, które mają skończoną aksjatyzację (np. Teoria mnogości Neumanna – Bernaysa – Gödela, która jest konserwatywnym rozszerzeniem ZFC). W przeciwieństwie do schematów aksjomatycznych ZFC nie można wyrazić skończoną liczbą aksjomatów. Myślę, ale nie jestem teraz pewien , czy schematy aksjomatów nie potrzebują pełnej mocy teorii mnogości lub logiki wyższego rzędu.
Martin Berger,

Odpowiedzi:

6

W skrócie, każde twierdzenie przedstawione w logice pierwszego rzędu ma dowód pierwszego rzędu.

W swojej książce „Wprowadzenie do logiki matematycznej i teorii typów” Peter B. Andrews rozwija zarówno logikę pierwszego rzędu, jak i system logiki wyższego rzędu Q 0 , który jest ogólnie uważany za podstawę teoretyczną współczesnych dowodów wyższego rzędu . (Zobacz na przykład wprowadzenie do logiki HOL).

W przypadku Q 0 i podobnych systemów Andrews pokazuje, że opisane przez niego logiki wyższego rzędu można uznać za konserwatywne rozszerzenia logiki pierwszego rzędu i pisze (drugie wydanie, s. 259), że „Podsumowując, każde twierdzenie pierwszego rzędu teoria typów ma dowód pierwszego rzędu. ”

Biorąc jednak pod uwagę twoje praktyczne obawy, cytuję również następujący akapit:

„Jednak niektóre twierdzenia dotyczące logiki pierwszego rzędu można najskuteczniej wykazać przy użyciu pojęć, które można wyrazić tylko w logice wyższego rzędu. Przykłady można znaleźć w [Andrews and Bishop, 1996] i [Boolos, 1998, Rozdział 25] Statman udowodnił [Statman, 1978, Propozycja 6.3.5], że minimalna długość dowodu w logice pierwszego rzędu wff logiki pierwszego rzędu może być wyjątkowo dłuższa niż minimalna długość dowodu tego samego wff w logika drugiego rzędu. Powiązany wynik Godela [Godel, 1936] jest taki, że generalnie „przejście do logiki następnego wyższego rzędu skutkuje nie tylko stworzeniem pewnych możliwych do udowodnienia twierdzeń, których wcześniej nie można było udowodnić, ale także stworzeniem w niewiarygodny sposób można skrócić nieskończenie wiele dostępnych już dowodów ”. Pełny dowód tego można znaleźć w [Buss,1994]. ”

Cris P.
źródło