New answers tagged lo.logic
0
I’m not sure I get what you are trying to do – or, rather, how your example corresponds to your goal. Indeed, in your code you postulate those three types a, b and c, but these are not really "arbitrary terms", rather they are types (this is just what you have postulated!). If you wanted to work with unspecified carriers, what you could do instead ...
1
You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has "coexponentials." Unfortunately you can't combine "coimplication" and "implication" constructively. You need to weaken something somewhere ...
4
Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): Olivier Laurent, Étude de la polarisation en logique (2002). A good explanation of what is going on from a categorical perspective is given in Melliès and Tabareau, Resource modalities in tensor logic (2010). A ...
3
For me, what is going on is reasonably standard:
You have $c$ with free variables $(x_i : \tau_i)_i$, and you replace it with $c[t_i/x_i]$ with the $(t_i)_i$ at types $(\tau_i)_i$; this is a standard cut/substitution.
The replacement is done along a variable $k$ that is defined somewhere and used elsewhere; this sort of "action at a distance" is ...
7
The two-variable fragment of intuitionistic first-order logic is undecidable, as proved in
Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev: Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables, Bulletin of Symbolic Logic 11 (2005), no. 3, pp. 428–438. http://www.jstor.org/stable/1578742.
Top 50 recent answers are included