数理逻辑中两种蕴含关系的formal定义

先直观的说下“推导”的概念，因为相信你不会陌生

“推导”就是“形如A=>B的序列”，这里的A，B不是随意的，而是满足给定的语法规则（作为“公理”），比如规则中有“A=>A”，据此就有推导：～A=>～A
因此推导是形式上的。而给定的规则集就叫做某种“证明系统”

正题
“┣” 是“推演”（或“证明”）的意思。在给定的证明系统中，如果存在从A到B的推导，就说A┣B（可以理解为从A可以经过有限步推导得出B）。┣是语法范畴的。

“╞” 是“使得真”的意思，一般写为M╞ F，其中M为某种解释，F为语句，意思就是“在解释M下F为真”。╞是语义范畴的。

再者纠正下这两个符号都不是“蕴含”关系（也叫“推论”）
“A蕴含B”定义为“任意使A为真的解释都使B为真”或者说成“如果M╞ A，则M╞ B”。蕴涵关系是语义范畴的，而且是语句间的关系。而上面说了“┣”是语法范畴的，“╞”也不是语句间的关系 。

至于说它们的关系。。。定义已经很明确了，谈不上什么关系啊。真要说关系，有一个“可靠性定理和歌德尔完备性定理”是联系语法和语义的。内容是
“存在某种证明系统满足：A┣B当且仅当A蕴含B”。再根据“蕴含”的定义：
“A┣B当且仅当如果M╞ A，则M╞ B”
这可以算是符号“┣”和“╞”的一种关系吧