(*** 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
*)