Sprzeczność między drugim twierdzeniem Gödela o niekompletności a własnością Church-Rosser CIC?

Z jednej strony drugie twierdzenie Gödela o niekompletności stwierdza, że żadna spójna teoria formalna, która jest wystarczająco silna, aby wyrazić dowolne podstawowe stwierdzenia arytmetyczne, nie może udowodnić swojej spójności. Z drugiej strony właściwość Churcha-Rossera systemu formalnego (przepisywania) mówi nam, że jest on spójny w tym sensie, że nie wszystkie równania można wyprowadzić, na przykład K $\neq$ Ja , ponieważ nie mają takiej samej normalnej postaci.

Następnie rachunek konstrukcji indukcyjnych (CIC) wyraźnie spełnia oba warunki. Jest wystarczająco silny, aby reprezentować zdania arytmetyczne (w rzeczy samej $\lambda\beta\eta$ - sam rachunek jest już w stanie zakodować liczby Kościoła i reprezentować wszystkie prymitywne funkcje rekurencyjne). Ponadto CIC ma również konfluencję lub własność Church-Rosser. Ale:

czy CIC nie powinien być w stanie udowodnić swojej spójności przez twierdzenie Drugiej Niekompletności?

A może po prostu stwierdza, że CIC nie może udowodnić własnej spójności w systemie, a w jakiś sposób właściwość zbiegu jest meta-twierdzeniem? A może właściwość CIC zbieżności nie gwarantuje jej spójności?

Byłbym bardzo wdzięczny, gdyby ktoś mógł rzucić nieco światła na te problemy!

Dzięki!

lo.logic type-theory lambda-calculus

— StudentType
źródło

W jakim sensie CR oznacza spójność? Rozważ relację

x \to y

$x \rightarrow y$ kiedy tylko

x, y \in X

$x, y \in X$ .

— Martin Berger,

@MartinBerger Mówisz, że CR nie oznacza spójności w CIC? Ponieważ robi to w

λ

$\lambda$ -kalkul, np. K

\neq

$\neq$ Ja . I przepraszam, nie rozumiem, że masz na myśli powyższą relację.

— StudentType

Nic nie wiem o CIC, ale oczywistą możliwością byłoby to, że nie udowodni on swojej własności Church-Rosser.

— Emil Jeřábek

Silna normalizacja byłaby bliższa spójności dla teorii typów nie? CR sugeruje, że istnieją nierówne warunki, ale to nie wyklucza mieszkańca pustki. Silna normalizacja nie jest wewnętrznie możliwa do udowodnienia, więc twierdzenie Godelsa nadal obowiązuje

— Daniel Gratzer

Intuicja polega na tym, że zazwyczaj łatwo jest wykazać, że w systemie nie ma złego normalnego obiektu. Teraz, jeśli możemy udowodnić, że wszystkie warunki mają normalną formę, jesteśmy skończeni. Algorytm normalizacyjny jest łatwy do sformalizowania. Najtrudniejsze jest pokazanie, że się kończy. Jeśli mamy funkcje, które rosną wystarczająco szybko w systemie, możemy je wykorzystać do udowodnienia górnej granicy zakończenia algorytmu normalizacji. Myślę, że stara książka Girarda powinna je mieć. Dowody i typy mogą również. (Każda dobra książka teorii teorii, która omawia prawdopodobne całkowite funkcje teorii, powinna ją mieć).

— Kaveh

Po pierwsze, mylisz spójność CIC jako teorii równania z spójnością CIC jako teorii logicznej . Pierwszy oznacza, że nie wszystkie warunki CIC (tego samego typu) są $\beta\eta$ -odpowiednik. Drugi oznacza, że typ $\bot$ nie jest zamieszkany. CR oznacza pierwszy rodzaj spójności, a nie drugi. Jak zauważono w komentarzach, sugeruje to (słaba) normalizacja. Prototypowym przykładem tej sytuacji jest czystość $\lambda$ -calculus: jest równomiernie spójny (CR utrzymuje), ale jeśli weźmiesz go pod uwagę jako system logiczny (jak pierwotnie zamierzał Kościół Alonzo), to jest niespójny (w rzeczywistości nie normalizuje się).

Po drugie, jak zauważył Emil, nawet jeśli CIC ma daną właściwość (CR lub normalizacja), jest całkowicie możliwe, że CIC nie może sama udowodnić tej właściwości. W tym przypadku nie widzę żadnej niespójności w tym, że CIC jest w stanie udowodnić swoją własność CR, i wydaje mi się, że tak właśnie jest (elementarne argumenty kombinatoryczne zwykle wystarczają dla CR, a takie argumenty zdecydowanie mieszczą się w moc logiczna CIC). Jednak CIC z pewnością nie dowodzi własnej właściwości normalizacyjnej, właśnie z powodu twierdzenia o drugiej niekompletności.

— Damiano Mazza
źródło

+1 dzięki! Czy mógłbyś choć trochę rozwinąć, w jaki sposób ta (słaba) właściwość normalizacji implikuje spójność (teorii logicznej)? tzn. w jaki sposób implikuje to fakt, że każdy termin ma normalną formę

⊥

$\bot$ jest zamieszkały?

— StudentType

Oczywiście! Zasadniczo jest to fakt, że eliminacja cięć oznacza konsekwencję. Bardziej szczegółowo: ponieważ normalizacja zachowuje typy, słaba normalizacja oznacza, że jeśli

⊥

$\bot$ jest zamieszkany, to jest zamieszkany przez normalny termin. Ale jest to (zwykle) trywialna konsekwencja definicji systemu logicznego (takiego jak CIC lub dowolne z obliczeń

λ

$\lambda$ -cube), dla którego nie ma normalnego mieszkańca

⊥

$\bot$ .

— Damiano Mazza

@StudentType: jest to stosunkowo prosty lemat (przez indukcję nad pochodnymi), że termin typu indukcyjnego w normalnej formie w pustym kontekście musi być konstruktorem stosowanym do argumentów.

⊥

$\bot$ jest typem indukcyjnym bez konstruktorów. Podobne dowody działają z alternatywnymi definicjami

⊥

$\bot$ .

— cody

Tak, masz rację @cody! Powinienem był powiedzieć, że (w tradycyjnych systemach) nie ma zamkniętego normalnego mieszkańca

⊥

$\bot$ (jest wielu normalnych mieszkańców

⊥

$\bot$ które nie są zamknięte!).

— Damiano Mazza