1. Paweł Wieczorek
  2. Metalogic

Commits

Paweł Wieczorek  committed fd52e4e

  • Participants
  • Parent commits fccdb8e
  • Branches default

Comments (0)

Files changed (1)

File metalogic/Fol/TheoremModelExistence.v

View file
  • Ignore whitespace
 Require Import FunctionalExtensionality.
 
 (**************************************************************************
+ **************************************************************************
+ **************************************************************************
+ * Rozszerzanie do teorii swiadkowo zupelnej (opisowo konstruktywnej).
  *
 
+
 Module Type WitnessExtensionDef. 
 
 Include Type AscendingSetsChainDef.
 End helpers.
 
 
+(**************************************************************************
+ **************************************************************************
+ **************************************************************************
+ * Konstrukcja modelu z termow stalych.
+ *)
+
 Section ModelConstruction.
 
 Variable L : FolLang.
 simpl. auto.
 Defined.
 
-
-(*------------------------------------------------------------------------
+(**************************************************************************
  * Nadawanie interpretacji symbolom funkcyjnym i relacja.
  *
  * CEL: Nadac interpretacje symbolowi funkcyjnemu f, taka ze
          (fun ts => L@T ||-- folAtom L r (folTermListClosed_unpack _ ts)) 
 .
 
+(**************************************************************************
+ * MODEL TERMOW
+ *)
+
 Let M := folStruct L Muniv Minhb Mfunc Mrel.
+
 Let v_unpack v (x:string) := folTermClosed_unpack L (v x).
 
 
+(**************************************************************************
+ * t^M = t
+ *)
+
 Let Mfunc_correct: forall v t (H:folTerm_closed L t),
     folValueT L M v t = folTermClosed_intro L t H.
 Proof.
 admit.
 Qed.
 
+(**************************************************************************
+ * v [ x ~> v(x) ] = v
+ *)
+
 Let value_eq v (x:string) :
     funcUpd v x (folValueT L M v (v_unpack v x)) = v.
 Proof.
 Qed.
 
 
+(**************************************************************************
+ * r^M(x1,....,xn)  wtw  T |- r(x1,...,xn)
+ *)
+
 Let Mrel_correct: forall r ts,
         (L@M |= folAtom L r (folTermListClosed_unpack _ ts))
     <-> (L@T ||-- folAtom L r (folTermListClosed_unpack _ ts)).
 admit.
 Qed.
 
-(*
-Let FolTermModel_Prop_subst: forall p x s v,
-       FolSubstCorr L x s p  ->
-(      (folInterp M (funcUpd v x (folValueT L M v s)) p)
-       <->
-      (folInterp M v (p <[ x ~> s]>))
-).
-Proof.
-intros.
-apply FolModel_Prop_subst.
-Qed.
-*)
-
 Let Mrel_correct': forall r ts, folTermList_closed L _ ts -> (
         (L@M |= folAtom L r ts)
     <-> (L@T ||-- folAtom L r ts)).
 apply Mrel_correct.
 Qed.
 
+(**************************************************************************
+ * Dla dowolnego zdania p: M |= p  wtw  T |- p
+ *)
+
 Theorem FolModelExistence_correct: forall p, folProp_closed L p
         -> ((L@M |= p) <-> (L@T ||-- p)).
 Proof.
 
 Qed.
 
+(**************************************************************************
+ * Teoria T ma model gdy jest niesprzeczna, swiadkowo-zupelna
+ * (o-konstruktywna) oraz zupelna.
+ *)
+
 Theorem FolModelExistence'': exists M, L@M ||= T.
 Proof.
 exists M.
 
 End ModelConstruction.
 
+(**************************************************************************
+ * Teoria T ma model gdy jest niesprzeczna i swiadkowo-zupelna
+ * (o-konstruktywna).
+ *)
+
 Theorem FolModelExistence': forall L (T:FolPropSet L),
         FolConsistent T
      -> FolWitnessConsistent T