Nachweis mit negativen induktiven Typen in Coq falsch

Question

Das dritte Kapitel von CPDT erläutert kurz, warum negative induktive Typen in Coq verboten sind. Wenn wir

Inductive term : Set := 
| App : term -> term -> term 
| Abs : (term -> term) -> term. 

hatte dann könnten wir leicht eine Funktion definieren

Definition uhoh (t : term) : term := 
    match t with 
    | Abs f => f t 
    | _ => t 
    end. 

so dass der Begriff uhoh (Abs uhoh) nicht-Abschluss wäre, mit dem „wir jeden Satz zu beweisen wäre in der Lage“.

Ich verstehe den Nicht-Kündigung Teil, aber ich verstehe nicht, wie wir damit etwas beweisen können. Wie würde man False mit term wie oben definiert beweisen?

Answer 1

Das Lesen Ihrer Frage ließ mich erkennen, dass ich Adams Argument auch nicht ganz verstanden habe. Aber Inkonsequenz in diesem Fall ergibt sich recht leicht aus Cantors üblichem diagonal argument (eine nie endende Quelle von Paradoxen und Puzzles in der Logik). Betrachten Sie die folgenden Annahmen:

Section Diag. 

Variable T : Type. 

Variable test : T -> bool. 

Variables x y : T. 

Hypothesis xT : test x = true. 
Hypothesis yF : test y = false. 

Variable g : (T -> T) -> T. 
Variable g_inv : T -> (T -> T). 

Hypothesis gK : forall f, g_inv (g f) = f. 

Definition kaboom (t : T) : T := 
    if test (g_inv t t) then y else x. 

Lemma kaboom1 : forall t, kaboom t <> g_inv t t. 
Proof. 
    intros t H. 
    unfold kaboom in H. 
    destruct (test (g_inv t t)) eqn:E; congruence. 
Qed. 

Lemma kaboom2 : False. 
Proof. 
    assert (H := @kaboom1 (g kaboom)). 
    rewrite -> gK in H. 
    congruence. 
Qed. 

End Diag. 

Dies ist eine generische Entwicklung, die mit dem term Typ in CPDT definiert instanziert werden könnte: T wäre term, x und y würden zwei Elemente term, die wir testen können zwischen unterscheiden (zB App (Abs id) (Abs id) und Abs id). Der entscheidende Punkt ist die letzte Annahme: Wir nehmen an, dass wir eine invertierbare Funktion g : (T -> T) -> T haben, die in Ihrem Beispiel Abs wäre. Mit dieser Funktion spielen wir den üblichen Diagonalisierungstrick: Wir definieren eine Funktion kaboom, die durch Konstruktion verschieden von jeder Funktion ist T -> T, einschließlich sich selbst. Daraus ergibt sich der Widerspruch.