Timeline for Intuitionistic proofs of propositional formulae versus natural transformations between finite sets
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 22 at 7:42 | comment | added | Brendan Murphy | I would like to return to this and think about it more seriously, but for the moment I'll say that the restriction to consistent variance feels like it might make things awkward. Similar sorts of variance issues come up when proving that a language admits "theorems for free" and the trick to make the induction work is to work with profunctors having possibly duplicated arguments (iirc) | |
| Dec 12, 2023 at 9:55 | comment | added | Gro-Tsen | @EmilJeřábek Concerning Kreisel-Putnam, at least, there is no natural transformation from $(B+C)^{0^A}$ to $B^{0^A} + C^{0^A}$: for $A=\varnothing$ this should be a nat.trans. $B+C \to B+C$ which it is easy to see is the identity, and for $A=\{\star\}$ this should be one of the two maps $\{\star\} \to \{\star_b,\star_c\}$ and then we get a contradiction by applying naturalness to the map $\varnothing \to \{\star\}$. | |
| Dec 12, 2023 at 9:47 | history | edited | Gro-Tsen | CC BY-SA 4.0 |
add some length remarks referencing related facts or questions
|
| Dec 12, 2023 at 9:06 | comment | added | Andrej Bauer | This sounds somewhat related to Statman's Finite Completeness Theorem. | |
| Dec 12, 2023 at 9:05 | comment | added | Gro-Tsen | @EmilJeřábek The question indeed arose partly out of my misremembering how Medvedev logic is defined, getting all confused about it, and trying to make sense of what I thought I had remembered — hence the common flavor. For those as confused as I was, the main difference is that ML defines “candidates” and “solutions”, and demand uniformity only when varying the solution sets for the variables, whereas my definition has only solutions (no candidates) and demands full functoriality of the problem solution (which in turn requires consistent variance). | |
| Dec 12, 2023 at 8:41 | comment | added | Emil Jeřábek | Or perhaps it is connected to admissible rules of intuitionistic logic? So, another test question: is there a natural transformation from $((A\to B)\to A\lor C)\hat{}$ to $(((A\to B)\to A)\lor((A\to B)\to C))\hat{}$? (This is the Mints rule, admissible in IPC, but not derivable in ML, or even in KC, as the latter has the same $\bot$-free fragment as IPC.) | |
| Dec 12, 2023 at 8:33 | comment | added | Emil Jeřábek | Test question: is there a natural transformation from $(\neg A\to B\lor C)\hat{}$ to $((\neg A\to B)\lor(\neg A\to C))\hat{}$? (Note that the Kreisel–Putnam schema $(\neg A\to B\lor C)\to(\neg A\to B)\lor(\neg A\to C)$ is valid in Medvedev’s logic.) | |
| Dec 12, 2023 at 8:29 | comment | added | Emil Jeřábek | There is too much category theory here for me to have a good intuition for what all this means, but it should be somehow connected to Medvedev’s logic (originally called the logic of finite problems, precisely because it has some kind of semantics based on operations on finite sets similar to here). | |
| Dec 11, 2023 at 23:18 | history | asked | Gro-Tsen | CC BY-SA 4.0 |