From Loeb Require Import Definitions External_Provability.
From Loeb.util Require Import Util.
From Equations Require Import Equations.
Require Equations.Type.DepElim.
Import EqNotations.
Require Import Eqdep_dec.
From FOL Require Import FullSyntax Arithmetics.
From FOL.Proofmode Require Import Theories ProofMode.
From FOL.Incompleteness Require Import Axiomatisations fol_utils qdec sigma1 ctq.
From FOL.Tennenbaum Require Import SyntheticInType MoreDecidabilityFacts.
Require FOL.Proofmode.Hoas.
Require Import String Lia List.
Import ListNotations.
Open Scope string_scope.
From Loeb.util Require Import Util.
From Equations Require Import Equations.
Require Equations.Type.DepElim.
Import EqNotations.
Require Import Eqdep_dec.
From FOL Require Import FullSyntax Arithmetics.
From FOL.Proofmode Require Import Theories ProofMode.
From FOL.Incompleteness Require Import Axiomatisations fol_utils qdec sigma1 ctq.
From FOL.Tennenbaum Require Import SyntheticInType MoreDecidabilityFacts.
Require FOL.Proofmode.Hoas.
Require Import String Lia List.
Import ListNotations.
Open Scope string_scope.
Section ExternalMostowski.
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.
Existing Instance falsity_on.
Variables pei: peirce.
Variables göd: goedelisation.
Instance eqdec_funcs : EqDec PA_funcs_signature.
Proof. intros x y; decide equality. Qed.
Instance eqdec_preds : EqDec PA_preds_signature.
Proof. intros x y. destruct x, y. now left. Qed.
Lemma encoding_ineq T n:
(forall φ, In φ Qeq -> T φ) -> n <> g ⊥ -> T ⊩ ¬(num n == num (g ⊥)).
Proof.
intros HT Hφ. eapply WeakT.
- apply (list_theory_provability Qeq).
specialize (Qdec_eq (num n) (num (g ⊥))) as HQdec.
assert (Qeq ⊢ (num n == num (g ⊥))[fun n => num 0] \/ Qeq ⊢ ¬(num n == num (g ⊥))[fun n => num 0]) as [Heq|Hneq].
apply HQdec. intros _. solve_bounds.
+ cbn in Heq. repeat rewrite num_subst in Heq. exfalso. apply Hφ.
eapply Σ1_soundness in Heq.
Unshelve. 4: exact (fun _ => 0).
2: now constructor.
2: { solve_bounds; apply num_bound. }
cbn in Heq. now repeat rewrite nat_eval_num in Heq.
+ cbn in Hneq. now repeat rewrite num_subst in Hneq.
- eauto.
Qed.
Definition mostowski_mod prov := prov ∧ ¬($0 == num (g ⊥)).
Lemma mostowski_consistency_sentence prov T:
(forall φ, In φ Qeq -> T φ) -> T ⊩ ¬(mostowski_mod prov)[(num (g ⊥))..].
Proof.
intros HT. eapply WeakT.
- apply (list_theory_provability Qeq). fstart.
unfold mostowski_mod. cbn. fintros "[Hpr Hineq]".
rewrite num_subst. fapply "Hineq". fapply ax_refl.
- eauto.
Qed.
Lemma mostowski_weak_repr prov T:
~T ⊩ ⊥ -> (forall φ, In φ Qeq -> T φ) ->
(forall φ, T ⊩ φ <-> T ⊩ prov[(num (g φ))..]) -> (forall φ, T ⊩ φ <-> T ⊩ (mostowski_mod prov)[(num (g φ))..]).
Proof.
intros HConsistent HT Hprov φ. split.
- intros Hφ. unfold mostowski_mod. cbn. apply T_CI; first firstorder.
rewrite num_subst. apply encoding_ineq; first easy. enough (φ <> ⊥).
{ rewrite inv_fg in H. rewrite (inv_fg ⊥) in H. congruence. }
congruence.
- intros HM. unfold mostowski_mod in HM. cbn in HM.
apply Hprov. now eapply T_CE1.
Qed.
There exists a sound external provability predciate for which a the consistency sentence is provable
Lemma ext_prov_modus_ponens_counteraxample (ctq: CTQ) T:
enumerable T -> Sig1_sound T -> (forall φ, In φ Qeq -> T φ) -> exists prov, sound_prov_pred pei göd T prov /\
T ⊩ ¬prov[(quine_quote ⊥)..].
Proof.
intros HEnum HSound HIncl.
destruct (ex_prov_T ctq göd HEnum HSound HIncl) as (prov & HΣ1 & Hrepr1 & Hrepr2).
unfold ext_prov_pred in Hrepr1. destruct Hrepr1 as (HprovB & Hrepr1).
exists (mostowski_mod prov). repeat split.
- unfold mostowski_mod. solve_bounds; first assumption. apply num_bound.
- apply mostowski_weak_repr.
+ now apply Sig1_sound_consistent.
+ assumption.
+ intros φ. unfold quine_quote in Hrepr1, Hrepr2. split; first apply Hrepr1.
apply Hrepr2.
- apply mostowski_weak_repr.
+ now apply Sig1_sound_consistent.
+ assumption.
+ intros φ. unfold quine_quote in Hrepr1, Hrepr2. split; first apply Hrepr1.
apply Hrepr2.
- now apply mostowski_consistency_sentence.
Qed.
Lemma mostowski_strong_sep prov T:
~T ⊩ ⊥ -> (forall φ, In φ Qeq -> T φ) ->
(forall φ, T ⊩ φ -> T ⊩ prov[(num (g φ))..]) -> (forall φ, (T ⊩ ¬φ) -> T ⊩ ¬prov[(num (g φ))..]) ->
(forall φ, T ⊩ φ -> T ⊩ (mostowski_mod prov)[(num (g φ))..]) /\ (forall φ, (T ⊩ ¬φ) -> T ⊩ ¬(mostowski_mod prov)[(num (g φ))..]).
Proof.
intros HConsistent HT HProv HnegProv. split; intros φ.
- intros Hφ. unfold mostowski_mod. cbn. apply T_CI; first firstorder.
rewrite num_subst. apply encoding_ineq; first easy. enough (φ <> ⊥).
{ rewrite inv_fg in H. rewrite (inv_fg ⊥) in H. congruence. }
congruence.
- intros Hφ. unfold mostowski_mod. cbn. rewrite num_subst.
apply T_II. specialize (HnegProv φ Hφ). fapply HnegProv.
eapply T_CE1. eapply T_Ctx. eapply contains_extend1.
Qed.
End ExternalMostowski.
Section ProofPredicateMostowski.
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.
Existing Instance falsity_on.
Variables pei: peirce.
enumerable T -> Sig1_sound T -> (forall φ, In φ Qeq -> T φ) -> exists prov, sound_prov_pred pei göd T prov /\
T ⊩ ¬prov[(quine_quote ⊥)..].
Proof.
intros HEnum HSound HIncl.
destruct (ex_prov_T ctq göd HEnum HSound HIncl) as (prov & HΣ1 & Hrepr1 & Hrepr2).
unfold ext_prov_pred in Hrepr1. destruct Hrepr1 as (HprovB & Hrepr1).
exists (mostowski_mod prov). repeat split.
- unfold mostowski_mod. solve_bounds; first assumption. apply num_bound.
- apply mostowski_weak_repr.
+ now apply Sig1_sound_consistent.
+ assumption.
+ intros φ. unfold quine_quote in Hrepr1, Hrepr2. split; first apply Hrepr1.
apply Hrepr2.
- apply mostowski_weak_repr.
+ now apply Sig1_sound_consistent.
+ assumption.
+ intros φ. unfold quine_quote in Hrepr1, Hrepr2. split; first apply Hrepr1.
apply Hrepr2.
- now apply mostowski_consistency_sentence.
Qed.
Lemma mostowski_strong_sep prov T:
~T ⊩ ⊥ -> (forall φ, In φ Qeq -> T φ) ->
(forall φ, T ⊩ φ -> T ⊩ prov[(num (g φ))..]) -> (forall φ, (T ⊩ ¬φ) -> T ⊩ ¬prov[(num (g φ))..]) ->
(forall φ, T ⊩ φ -> T ⊩ (mostowski_mod prov)[(num (g φ))..]) /\ (forall φ, (T ⊩ ¬φ) -> T ⊩ ¬(mostowski_mod prov)[(num (g φ))..]).
Proof.
intros HConsistent HT HProv HnegProv. split; intros φ.
- intros Hφ. unfold mostowski_mod. cbn. apply T_CI; first firstorder.
rewrite num_subst. apply encoding_ineq; first easy. enough (φ <> ⊥).
{ rewrite inv_fg in H. rewrite (inv_fg ⊥) in H. congruence. }
congruence.
- intros Hφ. unfold mostowski_mod. cbn. rewrite num_subst.
apply T_II. specialize (HnegProv φ Hφ). fapply HnegProv.
eapply T_CE1. eapply T_Ctx. eapply contains_extend1.
Qed.
End ExternalMostowski.
Section ProofPredicateMostowski.
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.
Existing Instance falsity_on.
Variables pei: peirce.
Instance eqdec_funcs' : EqDec PA_funcs_signature.
Proof. intros x y; decide equality. Qed.
Instance eqdec_preds' : EqDec PA_preds_signature.
Proof. intros x y. destruct x, y. now left. Qed.
Definition impl_dec:
forall φ ψ, {τ & ψ = φ → τ} + ({τ & ψ = φ → τ} -> False).
Proof.
intros φ ψ. destruct ψ.
- right. intros [τ Hτ]. congruence.
- right. intros [τ Hτ]. congruence.
- destruct b0. 1-2: right; intros [τ Hτ]; congruence.
destruct (dec_form _ _ _ _ φ ψ1).
+ left. exists ψ2. congruence.
+ right. intros [τ Hτ]. apply n.
destruct b; eapply form_inv in Hτ as []; congruence.
- right. intros [τ Hτ]. congruence.
Qed.
Variables göd: goedelisation.
Variables T: form -> Prop.
Variables T_enumerator: nat -> option form.
Variables HEnum: forall φ, T ⊢T φ <-> exists n, T_enumerator n = Some φ.
Definition prf n s := T_enumerator n = Some (f s).
Definition prov s := exists n, prf n s.
Definition prf_decider t:
forall n, {prf n t} + {prf n t -> False}.
Proof.
intros n. unfold prf. destruct (T_enumerator n) as [φ |] eqn:E; cbn; last (right; congruence).
destruct (dec_form _ _ _ _ φ (f t)).
- left. congruence.
- right. congruence.
Qed.
Definition prf_decider':
forall n s, (prf n s) + (prf n s -> False).
Proof.
intros n s. now destruct (prf_decider s n).
Qed.
Maps two formulas φ ψ to the Gödel number of φ ψ
Maps the Gödel numbers n, m to the Gödel number of the formula (f n) → (f m)
Given a proof n of the formula (f s) and a proof m of the formula (f s) → (f m),
computes a proof of the formula (f m).
Definition proof_MP:
forall n m s t, prf n s -> prf m (impl' s t) -> {k & prf k t}.
Proof.
intros n m s t Hn Hm. unfold prf in *.
assert (Hfs: T ⊩ f s). apply HEnum. easy.
assert (Himpl: T ⊩ f (impl' s t)). apply HEnum. easy.
assert (Hconcl: T ⊩ f t).
- unfold impl' in Himpl. destruct (impl (f s) (f t)) as [i Hi]. cbn in Himpl.
rewrite Hi in Himpl. rewrite <- inv_fg in Himpl.
now eapply T_IE.
- specialize (@Witnessing_nat (fun n => prf n t) (prf_decider t)) as Hwitn.
apply Hwitn. now apply HEnum.
Qed.
forall n m s t, prf n s -> prf m (impl' s t) -> {k & prf k t}.
Proof.
intros n m s t Hn Hm. unfold prf in *.
assert (Hfs: T ⊩ f s). apply HEnum. easy.
assert (Himpl: T ⊩ f (impl' s t)). apply HEnum. easy.
assert (Hconcl: T ⊩ f t).
- unfold impl' in Himpl. destruct (impl (f s) (f t)) as [i Hi]. cbn in Himpl.
rewrite Hi in Himpl. rewrite <- inv_fg in Himpl.
now eapply T_IE.
- specialize (@Witnessing_nat (fun n => prf n t) (prf_decider t)) as Hwitn.
apply Hwitn. now apply HEnum.
Qed.
Takes proofs n (of some formula φ) and m (of some formula ψ) and sends it to a proof of
τ (provided that ψ is of the form φ → τ).
Returns 0 if either n or m are not encodings of proofs.
Returns 0 if ψ is not of the required form.
Definition proof_MP' (n m: nat): nat :=
match (T_enumerator n), (T_enumerator m) with
| Some φ, Some ψ => match (impl_dec φ ψ) with
| inl Sigτ => match (prf_decider' n (g φ)), (prf_decider' m (impl' (g φ) (g (projT1 Sigτ)))) with
| inl P, inl Q => projT1 (proof_MP P Q)
| _, _ => 0
end
| _ => 0
end
| _, _ => 0
end.
Lemma proof_MP'_correct:
inv g f -> forall n m s t, prf n s -> prf m (impl' s t) -> prf (proof_MP' n m) t.
Proof.
intros inv_gf n m s t Hn Hm.
assert (Hn': T_enumerator n = Some (f s)). easy.
assert (Hm': T_enumerator m = Some (f (impl' s t))). easy.
unfold proof_MP'. destruct (T_enumerator n) as [φ |]; last easy.
destruct (T_enumerator m) as [ψ |]; last easy.
assert (φ = f s) as -> by congruence.
assert (ψ = f (impl' s t)) as -> by congruence.
clear Hn' Hm'.
destruct (impl_dec (f s) (f (impl' s t))) as [[τ Hτ] | HnegImpl].
- assert (τ = f t) as ->. unfold impl' in Hτ. destruct (impl (f s) (f t)) as [x Hx].
cbn in Hτ. rewrite Hx in Hτ. rewrite <- inv_fg in Hτ.
eapply form_inv in Hτ as []. congruence.
rewrite <- inv_gf. destruct (prf_decider' n s) as [P | nP].
+ cbn. destruct (prf_decider' m (g (f s → f (g (f t))))) as [Q | nQ].
* destruct (proof_MP P Q). cbn. rewrite <- inv_gf in p. assumption.
* rewrite <- inv_fg in nQ. exfalso. apply nQ.
unfold impl' in Hm. destruct (impl (f s) (f t)) as [x Hx].
rewrite <- Hx. cbn in Hm. assumption.
+ exfalso. apply nP. assumption.
- destruct (impl (f s) (f t)) as [imp Himp]. exfalso. apply HnegImpl.
exists (f t). cbn. now rewrite <- inv_fg.
Qed.
match (T_enumerator n), (T_enumerator m) with
| Some φ, Some ψ => match (impl_dec φ ψ) with
| inl Sigτ => match (prf_decider' n (g φ)), (prf_decider' m (impl' (g φ) (g (projT1 Sigτ)))) with
| inl P, inl Q => projT1 (proof_MP P Q)
| _, _ => 0
end
| _ => 0
end
| _, _ => 0
end.
Lemma proof_MP'_correct:
inv g f -> forall n m s t, prf n s -> prf m (impl' s t) -> prf (proof_MP' n m) t.
Proof.
intros inv_gf n m s t Hn Hm.
assert (Hn': T_enumerator n = Some (f s)). easy.
assert (Hm': T_enumerator m = Some (f (impl' s t))). easy.
unfold proof_MP'. destruct (T_enumerator n) as [φ |]; last easy.
destruct (T_enumerator m) as [ψ |]; last easy.
assert (φ = f s) as -> by congruence.
assert (ψ = f (impl' s t)) as -> by congruence.
clear Hn' Hm'.
destruct (impl_dec (f s) (f (impl' s t))) as [[τ Hτ] | HnegImpl].
- assert (τ = f t) as ->. unfold impl' in Hτ. destruct (impl (f s) (f t)) as [x Hx].
cbn in Hτ. rewrite Hx in Hτ. rewrite <- inv_fg in Hτ.
eapply form_inv in Hτ as []. congruence.
rewrite <- inv_gf. destruct (prf_decider' n s) as [P | nP].
+ cbn. destruct (prf_decider' m (g (f s → f (g (f t))))) as [Q | nQ].
* destruct (proof_MP P Q). cbn. rewrite <- inv_gf in p. assumption.
* rewrite <- inv_fg in nQ. exfalso. apply nQ.
unfold impl' in Hm. destruct (impl (f s) (f t)) as [x Hx].
rewrite <- Hx. cbn in Hm. assumption.
+ exfalso. apply nP. assumption.
- destruct (impl (f s) (f t)) as [imp Himp]. exfalso. apply HnegImpl.
exists (f t). cbn. now rewrite <- inv_fg.
Qed.
We can represent prf in T
Variables prf_form: form.
Variables Hprf_form_bnd: bounded 2 prf_form.
Variables Hprf_form: forall n m, (prf n m <-> T ⊩ prf_form[(num n) .: (num m) ..]) /\ (~prf n m -> T ⊩ ¬prf_form[(num n) .: (num m) ..]).
Definition prf_form_mostowski := prf_form[$0 .: $1..] ∧ ¬($1 == num (g ⊥)).
Variables Hprf_form_bnd: bounded 2 prf_form.
Variables Hprf_form: forall n m, (prf n m <-> T ⊩ prf_form[(num n) .: (num m) ..]) /\ (~prf n m -> T ⊩ ¬prf_form[(num n) .: (num m) ..]).
Definition prf_form_mostowski := prf_form[$0 .: $1..] ∧ ¬($1 == num (g ⊥)).
prf_form_mostowski also represents prf
Lemma prf_form_mostowski_represents_prf:
~T ⊢T ⊥ -> (forall φ, In φ Qeq -> T φ) -> forall n m, (prf n m <-> T ⊩ prf_form_mostowski[(num n) .: (num m) ..]) /\ (~prf n m -> T ⊩ ¬prf_form_mostowski[(num n) .: (num m) ..]).
Proof.
intros Hconsistent Hincl n m. repeat split.
- intro Hprf.
unfold prf_form_mostowski. asimpl. replace (prf_form[_]) with (prf_form[(num n) .: (num m)..]).
2: { apply subst_bound_2. assumption. }
assert (HmBot: m <> (g ⊥)).
intros HmBot. apply Hconsistent. apply HEnum.
exists n. unfold prf in Hprf. rewrite Hprf. rewrite HmBot. now rewrite <- inv_fg.
assert (T ⊩ ¬ FA.num m == FA.num (g ⊥)) as HNeq. now apply encoding_ineq.
apply T_CI.
+ now apply Hprf_form.
+ cbn. now rewrite num_subst.
- intros Hmos.
unfold prf_form_mostowski in Hmos. asimpl in Hmos. replace (prf_form[_]) with (prf_form[(num n) .: (num m)..]) in Hmos.
2: { apply subst_bound_2. assumption. }
apply T_CE1 in Hmos. now apply Hprf_form.
- intros nprf. apply Hprf_form in nprf. unfold prf_form_mostowski. asimpl.
replace (prf_form[_ .: _ .: _ .: _ ..]) with (prf_form[num n .: (num m)..]).
2: { apply subst_bound_2. assumption. }
apply T_II. fapply nprf. eapply T_CE1. eapply T_Ctx. eapply contains_extend1.
Qed.
~T ⊢T ⊥ -> (forall φ, In φ Qeq -> T φ) -> forall n m, (prf n m <-> T ⊩ prf_form_mostowski[(num n) .: (num m) ..]) /\ (~prf n m -> T ⊩ ¬prf_form_mostowski[(num n) .: (num m) ..]).
Proof.
intros Hconsistent Hincl n m. repeat split.
- intro Hprf.
unfold prf_form_mostowski. asimpl. replace (prf_form[_]) with (prf_form[(num n) .: (num m)..]).
2: { apply subst_bound_2. assumption. }
assert (HmBot: m <> (g ⊥)).
intros HmBot. apply Hconsistent. apply HEnum.
exists n. unfold prf in Hprf. rewrite Hprf. rewrite HmBot. now rewrite <- inv_fg.
assert (T ⊩ ¬ FA.num m == FA.num (g ⊥)) as HNeq. now apply encoding_ineq.
apply T_CI.
+ now apply Hprf_form.
+ cbn. now rewrite num_subst.
- intros Hmos.
unfold prf_form_mostowski in Hmos. asimpl in Hmos. replace (prf_form[_]) with (prf_form[(num n) .: (num m)..]) in Hmos.
2: { apply subst_bound_2. assumption. }
apply T_CE1 in Hmos. now apply Hprf_form.
- intros nprf. apply Hprf_form in nprf. unfold prf_form_mostowski. asimpl.
replace (prf_form[_ .: _ .: _ .: _ ..]) with (prf_form[num n .: (num m)..]).
2: { apply subst_bound_2. assumption. }
apply T_II. fapply nprf. eapply T_CE1. eapply T_Ctx. eapply contains_extend1.
Qed.
The mostowski modification proves the consistency sentence
Lemma prf_form_mostowski_consistency_sentence:
(forall φ, In φ Qeq -> T φ) -> T ⊩ ¬ ∃ prf_form_mostowski[$0 .: (num (g ⊥))..].
Proof.
eapply WeakT. apply (list_theory_provability Qeq).
fstart. unfold prf_form_mostowski. asimpl. cbn. rewrite num_subst.
fintros "[x [Hprf Heq]]". repeat rewrite num_subst. fapply "Heq". fapply ax_refl.
Qed.
End ProofPredicateMostowski.
(forall φ, In φ Qeq -> T φ) -> T ⊩ ¬ ∃ prf_form_mostowski[$0 .: (num (g ⊥))..].
Proof.
eapply WeakT. apply (list_theory_provability Qeq).
fstart. unfold prf_form_mostowski. asimpl. cbn. rewrite num_subst.
fintros "[x [Hprf Heq]]". repeat rewrite num_subst. fapply "Heq". fapply ax_refl.
Qed.
End ProofPredicateMostowski.