Editing Strict conditional (section)

==Constructive logic==
In a [[Constructive logic|constructive]] setting, the symmetry between ⥽ and <math>\Box</math> is broken, and the two connectives can be studied independently. Constructive strict implication can be used to investigate [[interpretability]] of [[Heyting arithmetic]] and to model [[arrow (computer science)|arrows]] and guarded [[recursion (computer science)|recursion]] in computer science.<ref>{{cite journal
| last1=Litak |first1 = Tadeusz 
| last2=Visser |first2 = Albert 
| year = 2018
| title = Lewis meets Brouwer: Constructive strict implication
| journal = [[Indagationes Mathematicae]]
| doi = 10.1016/j.indag.2017.10.003
| arxiv = 1708.02143
| volume = 29
| issue = 1 
| pages = 36–90
|s2cid = 12461587 
}}</ref>