IF逻辑与IF模态逻辑

IF Logic and IF Modal Logic

IF逻辑全名为独立友好的一阶逻辑,于上世纪80年代末90年代初由欣迪卡提出。欣迪卡发现在数学和自然语言中,不但存在传统一阶逻辑所刻画的量词之间相互依存的情况,有的时候还有不存在依存关系、相互独立的量词。为了刻画这种现象,他向一阶量词逻辑引入一个独立指针"/",表示指针上面的量词与指针下面的量词不存在依赖关系。IF逻辑在句法上是对一阶逻辑的直接扩张,表达力相当于二阶逻辑。之后,Bradfield尝试将IF逻辑的思想用于表示计算机系统执行路径的相互独立,用模态之间的独立来表示事件之间的独立,发展出IF模态逻辑。IF模态逻辑是模态逻辑的一个新兴分支,还存在很多有待深入思考和探究的问题。

Independence Friendly first-order Logic, shortened as IF logic, is proposed by Hintikka, a Finnish philosopher and logician, around late 1980s and early 1990s. Hintikka noticed there are cases like Henkin quantificational sentence ＇Some relative of every villager and some friend of every townsman hate each other＇ where the choice of some relative only depends on which villager＇ s relative he is, but is independent of the choice of both townsman and townsman＇ s friends. Likewise, only the choice of townsman matters to the interpretation of ＇ some friend＇ . Hintikka introduced an independent slash / to first-order quantificational logic to show that the quantifier above the slash is independent of those that are under. IF logic is a direct extension to first order logic. Its expressive power is amount to second-order logic. In around 2000, Bradfield integrated the this quantifier independent idea to Modal logic -- one of the two key notion in Computer science-to modal independent events in computation paths. IF modal logic is a newly sprout branch of Modal logic, which, for sure, remains a large amount of interesting topics for further exploration.