diff --git a/Foundation/Logic/Decidability.lean b/Foundation/Logic/Decidability.lean new file mode 100644 index 00000000..2a331d0d --- /dev/null +++ b/Foundation/Logic/Decidability.lean @@ -0,0 +1,40 @@ +import Foundation.Logic.Entailment + +namespace LO.Entailment + +section + +variable {F S : Type*} [Primcodable F] [Entailment F S] + +variable (𝓒 : S) + +class Decidable where + dec : ComputablePred (theory 𝓒) + +def Undecidable := Β¬Decidable 𝓒 + +class EssentiallyUndecidable [LogicalConnective F] where + essentially_undec : βˆ€ 𝓣 : S, 𝓒 βͺ― 𝓣 β†’ Incomplete 𝓣 β†’ Undecidable 𝓣 + +variable {𝓒} + +lemma decidable_of_incomplete : Inconsistent 𝓒 β†’ Decidable 𝓒 := + fun h ↦ ⟨by rw [h.theory_eq]; exact ComputablePred.const _⟩ + +end + +class PrimrecLogicalConnective (F : Type*) [Primcodable F] extends LogicalConnective F where + and : Primrecβ‚‚ fun Ο† ψ : F ↦ Ο† ⋏ ψ + or : Primrecβ‚‚ fun Ο† ψ : F ↦ Ο† β‹Ž ψ + imply : Primrecβ‚‚ fun Ο† ψ : F ↦ Ο† ➝ ψ + neg : Primrec fun Ο† : F ↦ βˆΌΟ† + +section Craig's_trick + +variable {F : Type*} [Primcodable F] [Entailment F (Set F)] + + + +end Craig's_trick + +end LO.Entailment diff --git a/Foundation/Logic/Entailment.lean b/Foundation/Logic/Entailment.lean index cdf35ffc..087acf49 100644 --- a/Foundation/Logic/Entailment.lean +++ b/Foundation/Logic/Entailment.lean @@ -232,118 +232,37 @@ lemma Inconsistent.of_ge {𝓒 : S} {𝓣 : T} (h𝓒 : Inconsistent 𝓒) (h : lemma Consistent.of_le {𝓒 : S} {𝓣 : T} (h𝓒 : Consistent 𝓒) (h : 𝓣 βͺ― 𝓒) : Consistent 𝓣 := ⟨fun H ↦ not_consistent_iff_inconsistent.mpr (H.of_ge h) hπ“’βŸ© -@[ext] structure Translation {S S' F F'} [Entailment F S] [Entailment F' S'] (𝓒 : S) (𝓣 : S') where - toFun : F β†’ F' - prf {f} : 𝓒 ⊒ f β†’ 𝓣 ⊒ toFun f - -infix:40 " ↝ " => Translation - -@[ext] structure Bitranslation {S S' F F'} [Entailment F S] [Entailment F' S'] (𝓒 : S) (𝓣 : S') where - r : 𝓒 ↝ 𝓣 - l : 𝓣 ↝ 𝓒 - r_l : r.toFun ∘ l.toFun = id - l_r : l.toFun ∘ r.toFun = id - -infix:40 " β†­ " => Bitranslation - -@[ext] structure FaithfulTranslation {S S' F F'} [Entailment F S] [Entailment F' S'] (𝓒 : S) (𝓣 : S') extends 𝓒 ↝ 𝓣 where - prfInv {f} : 𝓣 ⊒ toFun f β†’ 𝓒 ⊒ f - -infix:40 " ↝¹ " => FaithfulTranslation - -namespace Translation - -variable {S S' S'' : Type*} {F F' F'' : Type*} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] - -instance (𝓒 : S) (𝓣 : S') : CoeFun (𝓒 ↝ 𝓣) (fun _ ↦ F β†’ F') := ⟨Translation.toFun⟩ - -protected def id (𝓒 : S) : 𝓒 ↝ 𝓒 where - toFun := id - prf := id - -@[simp] lemma id_app (𝓒 : S) (f : F) : Translation.id 𝓒 f = f := rfl - -def comp {𝓒 : S} {𝓣 : S'} {𝓀 : S''} (Ο† : 𝓣 ↝ 𝓀) (ψ : 𝓒 ↝ 𝓣) : 𝓒 ↝ 𝓀 where - toFun := Ο†.toFun ∘ ψ.toFun - prf := Ο†.prf ∘ ψ.prf - -@[simp] lemma comp_app {𝓒 : S} {𝓣 : S'} {𝓀 : S''} (Ο† : 𝓣 ↝ 𝓀) (ψ : 𝓒 ↝ 𝓣) (f : F) : - Ο†.comp ψ f = Ο† (ψ f) := rfl - -lemma provable {𝓒 : S} {𝓣 : S'} (f : 𝓒 ↝ 𝓣) {Ο†} (h : 𝓒 ⊒! Ο†) : 𝓣 ⊒! f Ο† := ⟨f.prf h.get⟩ - -end Translation - -namespace Bitranslation - -variable {S S' S'' : Type*} {F F' F'' : Type*} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] - -@[simp] lemma r_l_app {𝓒 : S} {𝓣 : S'} (f : 𝓒 β†­ 𝓣) (Ο† : F') : f.r (f.l Ο†) = Ο† := congr_fun f.r_l Ο† - -@[simp] lemma l_r_app {𝓒 : S} {𝓣 : S'} (f : 𝓒 β†­ 𝓣) (Ο† : F) : f.l (f.r Ο†) = Ο† := congr_fun f.l_r Ο† - -protected def id (𝓒 : S) : 𝓒 β†­ 𝓒 where - r := Translation.id 𝓒 - l := Translation.id 𝓒 - r_l := by ext; simp - l_r := by ext; simp - -protected def symm {𝓒 : S} {𝓣 : S'} (Ο† : 𝓒 β†­ 𝓣) : 𝓣 β†­ 𝓒 where - r := Ο†.l - l := Ο†.r - r_l := Ο†.l_r - l_r := Ο†.r_l - -def comp {𝓒 : S} {𝓣 : S'} {𝓀 : S''} (Ο† : 𝓣 β†­ 𝓀) (ψ : 𝓒 β†­ 𝓣) : 𝓒 β†­ 𝓀 where - r := Ο†.r.comp ψ.r - l := ψ.l.comp Ο†.l - r_l := by ext; simp - l_r := by ext; simp - -end Bitranslation - -namespace FaithfulTranslation - -variable {S S' S'' : Type*} {F F' F'' : Type*} [Entailment F S] [Entailment F' S'] [Entailment F'' S''] - -instance (𝓒 : S) (𝓣 : S') : CoeFun (𝓒 ↝¹ 𝓣) (fun _ ↦ F β†’ F') := ⟨fun t ↦ t.toFun⟩ - -protected def id (𝓒 : S) : 𝓒 ↝¹ 𝓒 where - toFun := id - prf := id - prfInv := id - -@[simp] lemma id_app (𝓒 : S) (f : F) : FaithfulTranslation.id 𝓒 f = f := rfl - -def comp {𝓒 : S} {𝓣 : S'} {𝓀 : S''} (Ο† : 𝓣 ↝¹ 𝓀) (ψ : 𝓒 ↝¹ 𝓣) : 𝓒 ↝¹ 𝓀 where - toFun := Ο†.toFun ∘ ψ.toFun - prf := Ο†.prf ∘ ψ.prf - prfInv := ψ.prfInv ∘ Ο†.prfInv - -@[simp] lemma comp_app {𝓒 : S} {𝓣 : S'} {𝓀 : S''} (Ο† : 𝓣 ↝¹ 𝓀) (ψ : 𝓒 ↝¹ 𝓣) (f : F) : - Ο†.comp ψ f = Ο† (ψ f) := rfl - -lemma provable {𝓒 : S} {𝓣 : S'} (f : 𝓒 ↝¹ 𝓣) {Ο†} (h : 𝓒 ⊒! Ο†) : 𝓣 ⊒! f Ο† := ⟨f.prf h.get⟩ - -lemma provable_iff {𝓒 : S} {𝓣 : S'} (f : 𝓒 ↝¹ 𝓣) {Ο†} : 𝓣 ⊒! f Ο† ↔ 𝓒 ⊒! Ο† := - ⟨fun h ↦ ⟨f.prfInv h.get⟩, fun h ↦ ⟨f.prf h.get⟩⟩ - -end FaithfulTranslation - section variable [LogicalConnective F] variable (𝓒 : S) -def Complete : Prop := βˆ€ f, 𝓒 ⊒! f ∨ 𝓒 ⊒! ∼f +class Complete : Prop where + con : βˆ€ Ο†, 𝓒 ⊒! Ο† ∨ 𝓒 ⊒! βˆΌΟ† -def Independent (f : F) : Prop := 𝓒 ⊬ f ∧ 𝓒 ⊬ ∼f +def Independent (Ο† : F) : Prop := 𝓒 ⊬ Ο† ∧ 𝓒 ⊬ βˆΌΟ† + +class Incomplete : Prop where + incon : βˆƒ Ο†, Independent 𝓒 Ο† end -lemma incomplete_iff_exists_undecidable [LogicalConnective F] {𝓒 : S} : - Β¬Entailment.Complete 𝓒 ↔ βˆƒ f, Independent 𝓒 f := by simp [Complete, Independent, not_or] +lemma complete_def [LogicalConnective F] {𝓒 : S} : + Complete 𝓒 ↔ βˆ€ Ο†, 𝓒 ⊒! Ο† ∨ 𝓒 ⊒! βˆΌΟ† := + ⟨fun h ↦ h.con, Complete.mk⟩ + +lemma incomplete_def [LogicalConnective F] {𝓒 : S} : + Incomplete 𝓒 ↔ βˆƒ Ο†, Independent 𝓒 Ο† := + ⟨fun h ↦ h.incon, Incomplete.mk⟩ + +lemma not_complete_iff_incomplete [LogicalConnective F] {𝓒 : S} : + Β¬Complete 𝓒 ↔ Incomplete 𝓒 := by + simp [complete_def, incomplete_def, Independent, not_or] + +lemma not_incomplete_iff_complete [LogicalConnective F] {𝓒 : S} : + Β¬Incomplete 𝓒 ↔ Complete 𝓒 := + Iff.symm <| iff_not_comm.mp not_complete_iff_incomplete.symm variable (S T) @@ -379,10 +298,6 @@ lemma weakening! (h : 𝓒 βŠ† 𝓣 := by simp) {f} : 𝓒 ⊒! f β†’ 𝓣 ⊒! def weakerThanOfSubset (h : 𝓒 βŠ† 𝓣) : 𝓒 βͺ― 𝓣 := ⟨fun _ ↦ weakening! h⟩ -def translation (h : 𝓒 βŠ† 𝓣) : 𝓒 ↝ 𝓣 where - toFun := id - prf := weakening h - end Axiomatized alias by_axm := Axiomatized.provable_axm @@ -409,10 +324,6 @@ variable [Collection F T] [StrongCut S T] lemma cut! {𝓒 : S} {𝓣 : T} {Ο† : F} (H : 𝓒 ⊒!* Collection.set 𝓣) (hp : 𝓣 ⊒! Ο†) : 𝓒 ⊒! Ο† := by rcases hp with ⟨b⟩; exact ⟨StrongCut.cut H.get b⟩ -def translation {𝓒 : S} {𝓣 : T} (B : 𝓒 ⊒* Collection.set 𝓣) : 𝓣 ↝ 𝓒 where - toFun := id - prf := StrongCut.cut B - end StrongCut noncomputable def WeakerThan.ofAxm! [Collection F S] [StrongCut S S] {𝓒₁ 𝓒₂ : S} (B : 𝓒₂ ⊒!* Collection.set 𝓒₁) : @@ -508,10 +419,6 @@ alias deduction! := Deduction.of_insert! lemma Deduction.inv! (h : 𝓒 ⊒! Ο† ➝ ψ) : cons Ο† 𝓒 ⊒! ψ := by rcases h with ⟨b⟩; exact ⟨Deduction.inv b⟩ -def Deduction.translation (Ο† : F) (𝓒 : S) : cons Ο† 𝓒 ↝ 𝓒 where - toFun := fun ψ ↦ Ο† ➝ ψ - prf := deduction - lemma deduction_iff : cons Ο† 𝓒 ⊒! ψ ↔ 𝓒 ⊒! Ο† ➝ ψ := ⟨deduction!, Deduction.inv!⟩ end deduction diff --git a/Foundation/Vorspiel/Vorspiel.lean b/Foundation/Vorspiel/Vorspiel.lean index 437a0d4c..954338e3 100644 --- a/Foundation/Vorspiel/Vorspiel.lean +++ b/Foundation/Vorspiel/Vorspiel.lean @@ -1105,3 +1105,24 @@ protected lemma comp {f : Ξ± β†’ Ξ²} (hf : Computable f) {p : Ξ² β†’ Prop} (hp : exact REPred.iff'.mpr ⟨_, pp.comp hf, by intro x; simp⟩ end REPred + +namespace ComputablePred + +variable {Ξ± Ξ² : Type*} [Primcodable Ξ±] [Primcodable Ξ²] {p q : Ξ± β†’ Prop} + +@[simp] protected lemma const (p : Prop) : ComputablePred fun _ : Ξ± ↦ p := + computable_iff_re_compl_re'.mpr ⟨REPred.const _, REPred.const _⟩ + +lemma and : ComputablePred p β†’ ComputablePred q β†’ ComputablePred fun x ↦ p x ∧ q x := by + simp_rw [computable_iff_re_compl_re'] + rintro ⟨hp, hnp⟩ + rintro ⟨hq, hnq⟩ + refine ⟨hp.and hq, (hnp.or hnq).of_eq <| by grind⟩ + +lemma or : ComputablePred p β†’ ComputablePred q β†’ ComputablePred fun x ↦ p x ∨ q x := by + simp_rw [computable_iff_re_compl_re'] + rintro ⟨hp, hnp⟩ + rintro ⟨hq, hnq⟩ + refine ⟨hp.or hq, (hnp.and hnq).of_eq <| by grind⟩ + +end ComputablePred