(*** A Feasible Formalization of Incompleteness *) (* Dominik Kirst - Saarland Universtiy Talk/Demo at Formalize!(?)-2 Workshop *) (*** Intro *) (* Topic 1: Coq as a proof assistant - Demo of usual workflow and main features - Depending on setting, formalization can be very compact Topic 2: Coq as a computational type theory - All functions definable in Coq are computable - Synthetic computability without Turing machines Topic 3: Incompleteness via Undecidability - Halting problem is at the core of incompleteness - Avoid all notoriously tricky machinery with Gödel codes Acknowledgements: - Building on joint work with Yannick Forster, Marc Hermes, Benjamin Peters, and Gert Smolka - Based on ideas by Post [1], Kleene [2], Richman [3], Bauer [4] Disclaimer: - Syntax might look scary, mathematics will stay basic - Break after first half to digest, second half pure pleasure [1] Post, Emil L. "A variant of a recursively unsolvable problem." Bulletin of the American Mathematical Society 52.4 (1946): 264-268. [2] Kleene, Stephen Cole. Mathematical logic. 1967. [3] Richman, Fred. "Church's thesis without tears." The Journal of symbolic logic 48.3 (1983): 797-803. [4] Bauer, Andrej. "First steps in synthetic computability theory." Electronic Notes in Theoretical Computer Science 155 (2006): 5-31. *) (*** Preamble *) Require Import ConstructiveEpsilon. Require Import Lia Cantor. Local Set Implicit Arguments. Local Unset Strict Implicit. Open Scope bool. (*** Warm-Up ***) (* predefined inductive type of natural numbers with O and S *) Print nat. (* typical definition of n <= m ordering for pairs a = (n, m) *) Definition leq (a : nat * nat) := exists k, snd a = fst a + k. Notation "n <= m" := (leq (n, m)). (* little proof that evenness can be characterised with modulo *) Lemma leq_minus : forall n m, n <= m <-> n - m = 0. Proof. intros n m. split. - intros H. unfold leq in H. cbn in H. destruct H as [k H]. rewrite H. lia. - intros H. exists (m - n). cbn. lia. Qed. (*** Synthetic Computability *) (* predefined inductive type of booleans with true and false *) Print bool. (* a decider is a boolean function f coinciding with a predicate p *) Definition decidable X (p : X -> Prop) := exists f : X -> bool, forall x, p x <-> f x = true. (* example: the ordering n <= m is decidable *) Lemma decidable_leq : decidable leq. Proof. unfold decidable. exists (fun a => match fst a - snd a with 0 => true | _ => false end). intros [n m]. cbn. rewrite leq_minus. destruct (n - m) as [|k]. - tauto. - split; congruence. Qed. (* a type is discrete if it has decidable equality *) Definition discrete X := decidable (fun a : X * X => fst a = snd a). (* predefined inductive type of options with Some and None *) Print option. (* discreteness is closed under options *) Definition discrete_option X : discrete X -> discrete (option X). Proof. intros [f Hf]. (* for Some x and Some y test whether x = y *) exists (fun a => match fst a, snd a with | Some x, Some y => f (x, y) | None, None => true | _, _ => false end). intros [[x|][y|]]; cbn; try (split; congruence). rewrite <- Hf. cbn. split; congruence. Qed. (* enumerability is expressed via sujections from the natural numbers *) Definition enumerable X (p : X -> Prop) := exists f : nat -> option X, forall x, p x <-> exists n, f n = Some x. Definition enumerableT X := exists f : nat -> option X, forall x, exists n, f n = Some x. (* basic computability result: decidable predicates are enumerable *) Lemma decidable_enumerable X (p : X -> Prop) : enumerableT X -> decidable p -> enumerable p. Proof. intros [f Hf] [g Hg]. (* enumerate all elements of X via f, test whether they are in p via g *) exists (fun n => match (f n) with Some x => if g x then Some x else None | _ => None end). intros x. rewrite Hg. split. - intros Hx. destruct (Hf x) as [n Hn]. exists n. rewrite Hn. rewrite Hx. tauto. - intros [n Hn]. destruct (f n) as [x'|]. + destruct (g x') eqn : Hx'. * congruence. * congruence. + congruence. Qed. (* basic computability result: decidable predicates are co-enumerable *) Notation complement p := (fun x => ~ p x). Lemma decidable_enumerable_complement X (p : X -> Prop) : enumerableT X -> decidable p -> enumerable (complement p). Proof. intros [f Hf] [g Hg]. exists (fun n => match (f n) with Some x => if g x then None else Some x | _ => None end). intros x. split. - intros Hx. destruct (Hf x) as [n Hn]. exists n. rewrite Hn. destruct (g x) eqn : Hx'; trivial. exfalso. apply Hx. apply Hg. apply Hx'. - intros [n Hn]. destruct (f n) as [x'|]; try congruence. intros Hx. apply Hg in Hx. destruct (g x') eqn : Hx'; congruence. Qed. (* slightly more involved result: bi-enumerable predicates are decidable *) Definition mu (p : nat -> Prop) f : (forall x, p x <-> f x = true) -> (exists n, p n) -> { n | p n }. Proof. intros Hf Hp. apply constructive_indefinite_ground_description_nat_Acc. - intros n. destruct (f n) eqn : Hn. + left. apply Hf. tauto. + right. intros H. apply Hf in H. congruence. - tauto. Qed. Definition definite X (p : X -> Prop) := forall x, p x \/ ~ p x. Theorem Post X (p : X -> Prop) : discrete X -> definite p -> enumerable p -> enumerable (complement p) -> decidable p. Proof. intros [h Hh] % discrete_option Hl [f Hf] [g Hg]. (* for every x, compute n such that one of the enumerators terminates for x *) assert (H : forall x, { n | f n = Some x \/ g n = Some x }). (* first we prove the asserted statement *) - intros x. apply (mu (f := fun n => h (f n, Some x) || h (g n, Some x))). + intros n. destruct h eqn : H1; destruct h eqn : H2; cbn. all: rewrite (Hh (f n, Some x)), (Hh (g n, Some x)); intuition congruence. + destruct (Hl x). * apply Hf in H as [n Hn]. exists n. tauto. * apply Hg in H as [n Hn]. exists n. tauto. (* now we use the asserted statement *) - exists (fun x => let (n, _) := H x in h (f n, Some x)). intros x. destruct (H x) as [n Hn]. rewrite <- Hh. cbn. firstorder. Qed. (*** Abstract Incompleteness *) Section Abstract. (* we assume an enumerable and discrete type of sentences... *) Variable sentences : Type. Hypothesis sentences_enum : enumerableT sentences. Hypothesis sentences_discrete : discrete sentences. (* ...an enumerable provability predicate... *) Variable provable : sentences -> Prop. Hypothesis provable_enum : enumerable provable. (* ...and a negation function provability is consistent for *) Variable neg : sentences -> sentences. Hypothesis consistency : forall phi, ~ (provable phi /\ provable (neg phi)). (* since proofs are enumerable, so are the proofs of negated sentences *) Lemma disprovable_enum : enumerable (fun phi => provable (neg phi)). Proof. destruct sentences_enum as [Fs HFs]. destruct sentences_discrete as [Fd HFd]. destruct provable_enum as [Fp HFp]. (* simultaneously enumerate proofs and formulas, check whether negation of formula was proven *) exists (fun n => let (k, l) := of_nat n in match Fs k, Fp l with | Some phi, Some psi => if Fd (neg phi, psi) then Some phi else None | _, _ => None end). intros phi. split. - intros [l Hl] % HFp. destruct (HFs phi) as [k Hk]. exists (to_nat (k, l)). rewrite cancel_of_to. rewrite Hk. rewrite Hl. assert (H : Fd (neg phi, neg phi) = true) by now apply HFd. rewrite H. tauto. - intros [n Hn]. destruct of_nat as [k l]. destruct (Fs k) as [psi|]; try congruence. destruct (Fp l) as [theta|] eqn : Hl; try congruence. destruct Fd eqn : Hd; try congruence. apply HFd in Hd. cbn in Hd. apply HFp. exists l. congruence. Qed. (* completeness states that every sentence is provable or disprovable *) Definition completeness := forall phi, provable phi \/ provable (neg phi). (* complete consistent systems conflate unprovability and refutability *) Lemma completeness_iff : completeness -> forall phi, ~ provable phi <-> provable (neg phi). Proof. intros HC. split; intros H1. - destruct (HC phi) as [H2|H2]. + tauto. + tauto. - intros H2. now apply (@consistency phi). Qed. (* main insight: complete systems are decidable *) Theorem completeness_decidable : completeness -> decidable provable. Proof. intros HC. apply Post. - apply sentences_discrete. - intros phi. rewrite (completeness_iff HC). apply HC. - apply provable_enum. - destruct disprovable_enum as [f Hf]. exists f. intros phi. rewrite (completeness_iff HC). apply Hf. Qed. (* contranegative reading: undecidable systems are incomplete *) Corollary undecidable_incompleteness : ~ decidable provable -> ~ completeness. Proof. intros H1 H2. apply H1, completeness_decidable, H2. Qed. (* so we just have to establich undecidability *) Section Reduction. (* assume an undecidable problem, could be halting problem for Turing machines *) Variable TM : Type. Variable Halt : TM -> Prop. Hypothesis Halt_undec : ~ decidable Halt. (* reductions between problems reflect decidability *) Definition reducible X Y (p : X -> Prop) (q : Y -> Prop) := exists f : X -> Y, forall x, p x <-> q (f x). Lemma reducible_decidable X Y (p : X -> Prop) (q : Y -> Prop) : reducible p q -> decidable q -> decidable p. Proof. intros [f Hf] [g Hg]. exists (fun x => g (f x)). intros x. rewrite <- Hg. apply Hf. Qed. (* contranegative reading: reductions between problems preserve undecidability *) Corollary reducible_undecidable X Y (p : X -> Prop) (q : Y -> Prop) : reducible p q -> ~ decidable p -> ~ decidable q. Proof. intros H1 H2 H3. apply H2. now apply (reducible_decidable H1). Qed. (* final result: any system strong enough to capture computation is incomplete *) Theorem Kleene : reducible Halt provable -> ~ completeness. Proof. intros H. apply undecidable_incompleteness. apply (reducible_undecidable H). apply Halt_undec. Qed. End Reduction. End Abstract. (*** Outro *) (* Instantiation: - Given for first-order axiomatisations Q, PA, HA, Z, ZF, HF... - Verifying the remaining reductions usually not much work, building on Coq Library of Undecidability Proofs [1] - Paper: https://www.ps.uni-saarland.de/extras/axiomatisations-ext/ - Code: github.com/dominik-kirst/coq-library-undecidability/ blob/itp-jar/theories/FOL/Util/Abstract.v Take-Home Messages: - Working in Coq is feasible and (mostly) fun - Synthetic computability is great - Constructive logic is great - Incompleteness is about computation (even stronger formulations [2]) [1] https://github.com/uds-psl/coq-library-undecidability [2] https://www.ps.uni-saarland.de/~peters/bachelor.php *)