# Commits

committed fd52e4e

• Participants
• Parent commits fccdb8e
• Branches default

# File metalogic/Fol/TheoremModelExistence.v

• 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`