Merge pull request #4 from HermesMarc/formulas

Tennenbaum's Theorem

theories/Tennenbaum/Abstract_coding.v

@@ -0,0 +1,68 @@
+Require Import Lia.
+
+From FOL.Tennenbaum Require Import DN_Utils.
+
+Section Coding.
+
+(** We want to capture more abstractly what is needed for the coding
+  theorem to hold. Originally we used divisibility for numbers, but we
+  can more generally assume that there is some binary predicate satisfying
+  the following two axioms.
+*)
+Variable In : nat -> nat -> Prop.
+
+Notation "u ∈ c" := (In u c) (at level 45).
+
+Hypothesis H_empty     : exists e, forall x, ~ x ∈ e.
+Hypothesis H_extend  : forall n c, exists c', forall x, x ∈ c' <-> x = n \/ x ∈ c.
+
+
+(** We can now prove that this binary relation can be used for encoding predicates.
+ *)
+Lemma bounded_coding p n :
+  (forall x, x < n -> p x \/ ~ p x) ->
+  exists c, forall u, (u < n -> (p u <-> u ∈ c)) /\ (u ∈ c -> u < n).
+Proof.
+  assert (forall u n, u < S n -> u < n \/ u = n) as E by lia.
+  induction n.
+  { intros. destruct H_empty as [e He]. 
+    exists e. intros u. split; [lia|]. intros []%He. }
+  intros Dec_p.
+  destruct IHn as [c Hc], (Dec_p n ltac:(lia)) as [pn|pn'].
+  1, 2: intros; apply Dec_p; lia.
+  - destruct (H_extend n c) as [c' Hc']. exists c'.
+    intros u. split.
+    + intros [| ->]%E. split.
+      * intros p_u%Hc; auto. apply Hc'; auto.
+      * intros [->|]%Hc'; auto. now apply Hc.
+      * split; eauto. intros _. apply Hc'; auto.
+    + intros [->|H%Hc]%Hc'; auto.
+  - exists c.
+    intros u; split.
+    + intros [| ->]%E; [now apply Hc|].
+        split; [now intros ?%pn'|].
+        intros H%Hc. lia.
+    + intros H%Hc. lia.
+Qed.
+
+Lemma DN_bounded_lem p n :
+  ~ ~ (forall x, x < n -> p x \/ ~ p x).
+Proof.
+  induction n as [|n IH].
+  { DN.ret. lia. }
+  DN.lem (p n). intros Hn.
+  DN.bind IH. DN.ret. intros x Hx.
+  assert (x < n \/ x = n) as [| ->] by lia.
+  all: auto.
+Qed.
+
+Corollary DN_coding p n :
+  ~~ exists c, forall u, (u < n -> (p u <-> u ∈ c)) /\ (u ∈ c -> u < n).
+Proof.
+  eapply DN.bind_.
+  - apply DN_bounded_lem.
+  - intro. apply DN.ret_, (bounded_coding p n); eauto.
+Qed.
+
+
+End Coding.

theories/Tennenbaum/CantorPairing.v

@@ -18,7 +18,7 @@ Proof.
     intros. apply IHn. lia.
 Defined.
 
-
+(** We define the Cantor pairing function and show that it is a Bijection.  *)
 Section Cantor.
 
   Definition next '(x,y) := 

theories/Tennenbaum/Church.v

@@ -1,6 +1,7 @@
 From FOL Require Import FullSyntax Arithmetics Theories.
 From Undecidability.Shared Require Import ListAutomation.
-From FOL.Tennenbaum Require Import NumberUtils Formulas SyntheticInType Peano.
+From FOL.Tennenbaum Require Import NumberUtils DN_Utils Formulas SyntheticInType Peano.
+From FOL.Incompleteness Require Import qdec sigma1 ctq.
 
 (* Require Import FOL Tarski Deduction Peano Formulas NumberTheory Synthetic DecidabilityFacts. *)
 Require Import Lia.
@@ -15,96 +16,107 @@ Notation "x ∣ y" := (exists k, x * k = y) (at level 50).
 Definition unary α := bounded 1 α.
 Definition binary α := bounded 2 α.
 
-
-
 Section ChurchThesis.
+Existing Instance PA_preds_signature.
+Existing Instance PA_funcs_signature.
 
+Context {peirce : peirce}.
 Instance ff : falsity_flag := falsity_on.
-Context {Δ1 : Delta1}.
 
 (** * Church's Thesis *)
 
 (** ** CT_Q  *)
 
-(*  CT_Q internalizes computability, by claiming that every function
+(** CT_Q internalizes computability, by claiming that every function
     nat -> nat is computable in a model of computation. In this case,
     the model of computaion is based on arithmetic: It represents
-    functions by formulas in the language of PA in such a way that a 
-    weak fragment (Q <<= PA) can prove the agreement of the formula
-    with the function on every input.  
+    functions by formulas in the language of PA in such a way that a
+    weak fragment (Q ⊆ PA) can prove the agreement of the formula
+    with the function on every input.
  *)
 
-Definition represents ϕ f := forall x, Q ⊢I ∀ ϕ[up (num x)..] ↔ $0 == num (f x).
-Definition CT_Q := forall f : nat -> nat, exists ϕ, bounded 3 ϕ /\ inhabited(delta1 ϕ) /\ represents (∃ ϕ) f.
+Notation Q := Qeq.
 
-(*  Weaker Version of CT_Q, where the existence of the formula 
-    is only given potentially (i.e. behing a double negation). 
+Definition represents φ f := forall x, Q ⊢ ∀ φ[num x .: $0..] ↔ $0 == num (f x).
+Definition CT_Q := forall f : nat -> nat, exists φ, bounded 2 φ /\ Σ1 φ /\ represents φ f.
+(** WCT_Q is a weaker Version of CT_Q, where the existence of the formula
+    is only given potentially (i.e. behing a double negation).
  *)
-Definition WCT_Q := forall f : nat -> nat, ~ ~ exists ϕ, bounded 3 ϕ /\ inhabited(delta1 ϕ) /\ represents (∃ ϕ) f.
+Definition WCT_Q := forall f : nat -> nat, ~~exists φ, bounded 2 φ /\ Σ1 φ /\ represents φ f.
+
+Lemma prime_div_relation :
+  CT_Q -> exists Π, bounded 2 Π /\ Σ1 Π /\
+    forall x, Q ⊢ ∀ Π[num x .: $0..] ↔ $0 == num (Irred x).
+Proof.
+  intros ct. apply ct.
+Qed.
 
 (** Strong Representability *)
 
-Definition strong_repr ϕ (p : nat -> Prop) := (forall x, p x -> Q ⊢I ϕ[(num x)..]) /\ (forall x, ~ p x -> Q ⊢I ¬ϕ[(num x)..]).
-Definition RT_strong := forall p : nat -> Prop, Dec p -> exists ϕ, bounded 2 ϕ /\ inhabited(delta1 ϕ) /\ strong_repr (∃ ϕ) p.
-Definition WRT_strong := forall p : nat -> Prop, Dec p ->  ~ ~ exists ϕ, bounded 2 ϕ /\ inhabited(delta1 ϕ) /\ strong_repr (∃ ϕ) p.
+Definition strong_repr ϕ (p : nat -> Prop) :=
+  (forall x, p x -> Q ⊢ ϕ[(num x)..]) /\ (forall x, ~ p x -> Q ⊢ ¬ϕ[(num x)..]).
+Definition RT_strong :=
+  forall p : nat -> Prop, Dec p -> exists ϕ, bounded 1 ϕ /\ Σ1 ϕ /\ strong_repr ϕ p.
+Definition WRT_strong :=
+  forall p : nat -> Prop, Dec p -> ~ ~ exists ϕ, bounded 1 ϕ /\ Σ1 ϕ /\ strong_repr ϕ p.
 
 (** Weak Representability *)
 
-Definition weak_repr ϕ (p : nat -> Prop) := (forall x, p x <-> Q ⊢I ϕ[(num x)..]).
-Definition RT_weak := forall p : nat -> Prop, enumerable p -> exists ϕ, bounded 3 ϕ /\ inhabited(delta1 ϕ) /\ weak_repr (∃∃ ϕ) p.
-Definition WRT_weak := forall p : nat -> Prop, enumerable p -> ~ ~ exists ϕ, bounded 3 ϕ /\ inhabited(delta1 ϕ) /\ weak_repr (∃∃ ϕ) p.
+Definition weak_repr ϕ (p : nat -> Prop) := (forall x, p x <-> Q ⊢ ϕ[(num x)..]).
+Definition RT_weak :=
+  forall p : nat -> Prop, enumerable p -> exists ϕ, bounded 1 ϕ /\ Σ1 ϕ /\ weak_repr ϕ p.
+Definition WRT_weak :=
+  forall p : nat -> Prop, enumerable p -> ~ ~ exists ϕ, bounded 1 ϕ /\ Σ1 ϕ /\ weak_repr ϕ p.
 
 Definition RT := RT_strong /\ RT_weak.
 
-Lemma prv_split {p : peirce} α β Gamma :
-  Gamma ⊢ α ↔ β <-> Gamma ⊢ (α → β) /\ Gamma ⊢ (β → α).
+Lemma prv_split α β Γ :
+  Γ ⊢ α ↔ β <-> Γ ⊢ (α → β) /\ Γ ⊢ (β → α).
 Proof.
-  split; intros H.
+ split; intros H.
   - split.
     + eapply CE1. apply H.
     + eapply CE2. apply H.
   - now constructor.
 Qed.
 
-Lemma up_switch ϕ s t :
-  ϕ[up (num s)..][up (num t)..] = ϕ[up (up (num t)..)][up (num s)..].
-Proof.
-  rewrite !subst_comp. apply subst_ext. 
-  intros [|[|[]]]; cbn; now rewrite ?num_subst.
-Qed.
-
 Lemma CT_WCT :
   CT_Q -> WCT_Q.
 Proof. intros ct f. specialize (ct f). tauto. Qed.
 
+Hint Resolve CT_WCT : core.
+
 (** ** Strong part of the representability theorem.  *)
 Lemma CT_RTs :
   CT_Q -> RT_strong.
 Proof.
   intros ct p Dec_p.
   destruct (Dec_decider_nat _ Dec_p) as [f Hf].
-  destruct (ct f) as [ϕ [b2 [[s1] H]]].
-  pose (Φ := ϕ[up (num 0)..]).
-  exists Φ. split; unfold Φ.
-  { asimpl. eapply subst_bound; eauto.
-    intros [|[|[]]] G; cbn; try lia. all: solve_bounds. }
-  split.
-  { constructor. now apply delta1_subst. }
+  destruct (ct f) as [ϕ (bϕ2 & Sϕ & Hϕ)].
+  exists ϕ[$0 .: (num 0) ..].
+  assert (forall a b c, ϕ[a .: b .: c..] = ϕ[a .: b..]) as Help.
+  { intros *. eapply bounded_subst; eauto.
+    intros [|[]]; simpl; lia || reflexivity. }
   repeat split.
-  all: intros x; specialize (H x).
-  all: eapply AllE with (t := num 0) in H; cbn -[Q] in H.
-  all: apply prv_split in H; destruct H as [H1 H2].
+  { eapply subst_bound; eauto. 
+    intros [|[]] ?; try lia; simpl; solve_bounds. }
+  { now apply Σ1_subst. }
+  all: intros x; specialize (Hϕ x).
+  all: eapply AllE with (t := num 0) in Hϕ; cbn -[Q] in Hϕ.
+  all: asimpl; asimpl in Hϕ.
+  all: rewrite !num_subst in *; rewrite Help in *.
+  all: apply prv_split in Hϕ; destruct Hϕ as [H1 H2].
   - intros px%Hf. symmetry in px.
-    eapply num_eq with (Gamma := Q)(p := intu) in px; [|firstorder].
-    eapply IE. cbn -[Q num]. rewrite up_switch.
-    apply H2. now rewrite num_subst.
+    eapply num_eq with (Gamma := Q) in px; [|firstorder].
+    eapply IE. cbn -[Qeq num].
+    apply H2. apply px.
   - intros npx. assert (0 <> f x) as E by firstorder.
-    apply num_neq with (Gamma := Q)(p := intu) in E; [|firstorder].
+    apply num_neq with (Gamma := Q)in E; [|firstorder].
     apply II. eapply IE.
     {eapply Weak; [apply E|now right]. }
     eapply IE; [|apply Ctx; now left].
-    rewrite num_subst in H1. eapply Weak.
-    + cbn -[Q num]. rewrite up_switch. apply H1.
+    eapply Weak.
+    + cbn -[Q num]. apply H1.
     + now right.
 Qed.
 
@@ -113,128 +125,44 @@ Lemma WCT_WRTs :
   WCT_Q -> WRT_strong.
 Proof.
   intros wct p Dec_p.
-  destruct (Dec_decider_nat _ Dec_p) as [f Hf]. 
-  apply (DN_chaining (wct f)), DN. intros [ϕ [b2 [[s1] H]]].
-  pose (Φ := ϕ[up (num 0)..]).
-  exists Φ. split; unfold Φ.
-  { eapply subst_bound; eauto.
-    intros [|[|[]]] ?; cbn; try lia. all: solve_bounds. }
-  split.
-  { constructor. now apply delta1_subst. }
+  destruct (Dec_decider_nat _ Dec_p) as [f Hf].
+  apply (DN.bind_ (wct f)).
+  intros [ϕ (bϕ2 & Sϕ & Hϕ)]. DN.ret.
+  exists ϕ[$0 .: (num 0) ..].
+  assert (forall a b c, ϕ[a .: b .: c..] = ϕ[a .: b..]) as Help.
+  { intros *. eapply bounded_subst; eauto.
+    intros [|[]]; simpl; lia || reflexivity. }
   repeat split.
-  all: intros x; specialize (H x).
-  all: eapply AllE with (t := num 0) in H; cbn -[Q] in H.
-  all: apply prv_split in H; destruct H as [H1 H2].
+  { eapply subst_bound; eauto. 
+    intros [|[]] ?; try lia; simpl; solve_bounds. }
+  { now apply Σ1_subst. }
+  all: intros x; specialize (Hϕ x).
+  all: eapply AllE with (t := num 0) in Hϕ; cbn -[Q] in Hϕ.
+  all: asimpl; asimpl in Hϕ.
+  all: rewrite !num_subst in *; rewrite Help in *.
+  all: apply prv_split in Hϕ; destruct Hϕ as [H1 H2].
   - intros px%Hf. symmetry in px.
-    eapply num_eq with (Gamma := Q)(p := intu) in px; [|firstorder].
-    eapply IE. cbn -[Q num]. rewrite up_switch.
-    apply H2. now rewrite num_subst.
+    eapply num_eq with (Gamma := Q) in px; [|firstorder].
+    eapply IE. cbn -[Q num].
+    apply H2. apply px.
   - intros npx. assert (0 <> f x) as E by firstorder.
-    apply num_neq with (Gamma := Q)(p := intu) in E; [|firstorder].
+    apply num_neq with (Gamma := Q) in E; [|firstorder].
     apply II. eapply IE.
     {eapply Weak; [apply E|now right]. }
     eapply IE; [|apply Ctx; now left].
-    rewrite num_subst in H1. eapply Weak.
-    + cbn -[Q num]. rewrite up_switch. apply H1.
+    eapply Weak.
+    + cbn -[Q num]. apply H1.
     + now right.
 Qed.
 
 (** ** Weak part of the representability theorem.  *)
 Lemma CT_RTw :
   CT_Q -> RT_weak.
 Proof.
-  intros ct p [f Hf]%enumerable_nat.
-  destruct (ct f) as [ϕ [b2 [[s1] H]]].
-  pose (Φ := ϕ[up (σ $1)..] ).
-  exists Φ; split. 2: split.
-  - unfold Φ. eapply subst_bound; eauto.
-    intros [|[|[]]] ?; try lia; repeat solve_bounds.
-  - constructor. now apply delta1_subst. 
-  - intros x. rewrite Hf. split.
-    + intros [n Hn]. symmetry in Hn.
-      apply sigma1_ternary_complete.
-      { unfold Φ. eapply subst_bound; eauto.
-      intros [|[|[]]] ?; try lia; repeat solve_bounds. }
-      {unfold Φ. now apply delta1_subst. }
-      exists n. specialize (H n).
-      apply soundness in H.
-      unshelve refine (let H := (H nat (extensional_model interp_nat) (fun _ => 0)) _ in _ ).
-      {apply Q_std_axioms. }
-      cbn in H. specialize (H (S x)) as [_ H2].
-      rewrite eval_num, inu_nat_id in *.
-      apply H2 in Hn. destruct Hn as [d Hd].
-      exists d.
-      unfold Φ. rewrite !sat_comp in *.
-      eapply bound_ext with (N:=3).
-      apply b2. 2: apply Hd.
-      intros [|[|[]]]; cbn; rewrite ?num_subst, ?eval_num, ?inu_nat_id in *.
-      all: try lia.
-    + intros HQ%soundness. specialize (HQ nat (extensional_model interp_nat) (fun _ => 0)). cbn in HQ.
-      destruct HQ as [n [d Hnd]].
-      {apply Q_std_axioms. }
-      exists n. specialize (H n).
-      apply soundness in H.
-      unshelve refine (let H := (H nat (extensional_model interp_nat) (fun _ => 0)) _ in _ ).
-      apply Q_std_axioms.
-      cbn in H. specialize (H (S x)) as [H1 _].
-      rewrite eval_num, inu_nat_id in *.
-      symmetry. apply H1. exists d.
-      rewrite !sat_comp in Hnd. 
-      unfold Φ in Hnd. rewrite sat_comp in *.
-      eapply bound_ext.
-      apply b2. 2: apply Hnd.
-      intros [|[|[]]]; cbn; rewrite ?num_subst, ?eval_num, ?inu_nat_id in *.
-      all: try lia; reflexivity.
+  intros ct p Hp. unfold weak_repr.
+  apply ctq_weak_repr; auto.
 Qed.
 
 
-Lemma WCT_WRTw :
-  WCT_Q -> WRT_weak.
-Proof.
-  intros wct p [f Hf]%enumerable_nat.
-  apply (DN_chaining (wct f)), DN.
-  intros [ϕ [b2 [[s1] H]]].
-  pose (Φ := ϕ[up (σ $1)..] ).
-  exists Φ; split. 2: split.
-  - unfold Φ. eapply subst_bound; eauto.
-    intros [|[|[]]] ?; try lia; repeat solve_bounds.
-  - constructor. now apply delta1_subst. 
-  - intros x. rewrite Hf. split.
-    + intros [n Hn]. symmetry in Hn.
-      apply sigma1_ternary_complete.
-      { unfold Φ. eapply subst_bound; eauto.
-        intros [|[|[]]] ?; try lia; repeat solve_bounds. }
-      {unfold Φ. now apply delta1_subst. }
-      exists n. specialize (H n).
-      apply soundness in H.
-      unshelve refine (let H := (H nat (extensional_model interp_nat) (fun _ => 0)) _ in _ ).
-      {apply Q_std_axioms. }
-      cbn in H. specialize (H (S x)) as [_ H2].
-      rewrite eval_num, inu_nat_id in *.
-      apply H2 in Hn. destruct Hn as [d Hd].
-      exists d.
-      unfold Φ. rewrite !sat_comp in *.
-      eapply bound_ext with (N:=3).
-      apply b2. 2: apply Hd.
-      intros [|[|[]]]; cbn; rewrite ?num_subst, ?eval_num, ?inu_nat_id in *.
-      all: try lia; reflexivity.
-    + intros HQ%soundness. specialize (HQ nat (extensional_model interp_nat) (fun _ => 0)). cbn in HQ.
-      destruct HQ as [n [d Hnd]].
-      {apply Q_std_axioms. }
-      exists n. specialize (H n).
-      apply soundness in H.
-      unshelve refine (let H := (H nat (extensional_model interp_nat) (fun _ => 0)) _ in _ ).
-      apply Q_std_axioms.
-      cbn in H. specialize (H (S x)) as [H1 _].
-      rewrite eval_num, inu_nat_id in *.
-      symmetry. apply H1. exists d.
-      rewrite !sat_comp in Hnd. 
-      unfold Φ in Hnd. rewrite sat_comp in *.
-      eapply bound_ext.
-      apply b2. 2: apply Hnd.
-      intros [|[|[]]]; cbn; rewrite ?num_subst, ?eval_num, ?inu_nat_id in *.
-      all: try lia; reflexivity.
-Qed.
-
 
 End ChurchThesis.