Commits

Paweł Wieczorek committed 7265e25

Comments (0)

Files changed (2)

metalogic/Fol/Model_facts3.v

 exists p. auto.
 Qed.
 Hint Resolve FolModel_sublang : metalogic_db.
+
+End ModelSublang.

metalogic/Fol/TheoremModelExistence.v

 
 End helpers.
 
+
+Section ModelConstruction.
+
+Variable L : FolLang.
+Variable T : FolPropSet L.
+Variable consT: FolConsistent T.
+Variable complT: FolComplete T.
+Variable wconsT: FolWitnessConsistent T.
+
+Let Muniv := folTermClosed L.
+
+Let Minhb : inhabited Muniv.
+Proof.
+apply inhabits.
+apply folTermClosed_intro with (folTermClosed_unpack L (folSomeClosedTerm L)).
+destruct folSomeClosedTerm.
+simpl. auto.
+Defined.
+
+Let Mfunc: forall f : folFuncs L, Defs.nAry (folFuncAr L f) Muniv.
+admit.
+Defined.
+
+Let Mrel: forall r : folRels L, Defs.nAryP (folRelAr L r) Muniv.
+admit.
+Defined.
+
+Let M := folStruct L Muniv Minhb Mfunc Mrel.
+
+Theorem FolModelExistence'': exists M, L@M ||= T.
+Proof.
+exists M.
+admit.
+Qed.
+
+End ModelConstruction.
+
 Theorem FolModelExistence': forall L (T:FolPropSet L),
         FolConsistent T
      -> FolWitnessConsistent T
 exists t.
 eauto with metalogic_db sets.
 
-set (Muniv := folTermClosed L).
-assert (inhabited Muniv) as Minh.
-apply inhabits.
-apply folTermClosed_intro with (folTermClosed_unpack L (folSomeClosedTerm L)).
-destruct folSomeClosedTerm.
-simpl. auto.
-
-assert (Mfunc : forall f : folFuncs L, Defs.nAry (folFuncAr L f) Muniv).
-admit.
-
-assert (forall r : folRels L, Defs.nAryP (folRelAr L r) Muniv) as Mrel.
-admit.
-
-set (M := folStruct L Muniv Minh Mfunc Mrel).
-exists M.
-admit.
+apply FolModelExistence''.
 Qed.
 
 Theorem FolModelExistence : forall L (T:FolPropSet L),