Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Logic.Classical_Pred_Type.
Require Import Logic.lib.Bijection.
Require Import Logic.lib.Countable.
Require Import Logic.lib.EnsemblesProperties.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.GeneralLogic.Complete.Lindenbaum.
Require Import Logic.GeneralLogic.Complete.Lindenbaum_Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Kripke.
Require Import Logic.GeneralLogic.Complete.ContextProperty_Trivial.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.Complete.Lindenbaum_Kripke.
Require Import Logic.MinimunLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.Classical.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.Complete.Lindenbaum_Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Kripke.
Require Import Logic.PropositionalLogic.Complete.ContextProperty_Trivial.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Section Lindenbaum_Trivial.

Context {L: Language}
        {minL: MinimunLanguage L}
        {pL: PropositionalLanguage L}
        {Gamma: ProofTheory L}
        {SC: NormalSequentCalculus L Gamma}
        {bSC: BasicSequentCalculus L Gamma}
        {fwSC: FiniteWitnessedSequentCalculus L Gamma}
        {minSC: MinimunSequentCalculus L Gamma}
        {ipSC: IntuitionisticPropositionalSequentCalculus L Gamma}
        {cpSC: ClassicalPropositionalSequentCalculus L Gamma}
        {minAX: MinimunAxiomatization L Gamma}
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma Lindenbaum_for_max_consistent: forall P,
  Lindenbaum_ensures P derivable_closed ->
  Lindenbaum_ensures P orp_witnessed ->
  Lindenbaum_ensures P consistent ->
  Lindenbaum_ensures P (maximal consistent).
Proof.
(* Goal: forall x : @expr L, @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@maximal L (@consistent L Gamma)) *)
  intros.
(* Goal: forall x : @expr L, @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@maximal L (@consistent L Gamma)) *)
  hnf; intros.
(* Goal: @maximal L (@consistent L Gamma) (@LindenbaumConstruction (@expr L) CA init P) *)
  apply DDCS_MCS; auto.
Qed.

Lemma Lindenbaum_cannot_derive_ensures_max_consistent {AX: NormalAxiomatization L Gamma}: forall x, Lindenbaum_ensures (cannot_derive x) (maximal consistent).
Proof.
(* Goal: forall x : @expr L, @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@maximal L (@consistent L Gamma)) *)
  intros.
(* Goal: @Lindenbaum_ensures (@expr L) (@cannot_derive L Gamma x) (@maximal L (@consistent L Gamma)) *)
  apply Lindenbaum_for_max_consistent.
  - apply Lindenbaum_cannot_derive_ensures_derivable_closed.
  - apply Lindenbaum_cannot_derive_ensures_orp_witnessed.
  - apply Lindenbaum_cannot_derive_ensures_consistent.
Qed.

End Lindenbaum_Trivial.
