Strict conditional: Difference between revisions

Revision as of 23:13, 16 August 2021

Revision as of 14:04, 12 December 2021

Line 35:

==Constructive logic==

In a 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

| doi = 10.1016/j.indag.2017.10.003

| last2=Visser |first2 = Albert

| author1 = Tadeusz Litak

| year = 2018

| author2 = Albert Visser

| title = Lewis meets Brouwer: Constructive strict implication

| journal = Indagationes Mathematicae

| doi = 10.1016/j.indag.2017.10.003

| volume = 29

| issue arxiv = 1 1708.02143

| pages volume = 36–9029

| yearissue = 1 = 2018

| pages = 36–90

| url = https://arxiv.org/abs/1708.02143 | arxiv = 1708.02143

}}</ref>