# Finite Strong Completeness Theorem for BL logic

I need to prove the finite strong completeness theorem for Basic Logic, where $BL$ is: $\vdash_{BL} =\vDash_{FLew}$ + linearity + division. The strong completeness is:

$$\varphi_1,...,\varphi_n \vdash_{BL} \varphi \Leftrightarrow \varphi_1,...,\varphi_n \vDash_{+} \varphi$$ Where $+$ is $\{[0,1]*cut \ t-norms\}$.

Now, I have a few notions, I know I need to use/check that: Any $BL$ chain is locally embeddable into $\{[0,1] \ continuos \ t-norms\}$

I also now I need to check that every $BL$ chain is embeddable into an ultra product of standard $BL$ chains.

My main problem is figuring out the structure of this proof, if someone could point out wither some set of steps that I need to follow, or even better a book or article where a similar proof is worked out for some other Many valued logic (Lukasiewics, product, etc...) I'd very much appreciate your help.

• What are the problems you find when you try to use any of these two embeddability results to provide a direct proof (of the finite strong completeness)? – boumol Jan 4 '16 at 14:11
• I don't know how to apply them, I understand why I need them, but when I try to justify how to do it I bump into a wall. – Sara Jan 4 '16 at 14:19
• Hint: When you assume that $\varphi_1, \ldots, \varphi_n \not \vdash_{BL} \varphi$, use the fact that $\vdash_{BL}$ is strongly complete with respect to the class of all BL-chains. I guess you are aware of this result (it can be "easily" proved using a Lindenbaum-Tarski argument together with the fact that all subdirectly irreducible BL-algebras are chains). – boumol Jan 4 '16 at 14:28
• Thank you for your help. Ok, so a structure something like this?: assume $\varphi_1,...,\varphi_n \not vdash_{BL} \varphi$, then as $\vdash_{BL}$ is complete with respect to the class of BL chains, so by applying the first thing I stated, it is locally embeddable into the cont. t norm? something like that? – Sara Jan 4 '16 at 15:21