Timeline for Logic without disjunction
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 4, 2013 at 8:16 | comment | added | serras | The main problem, I think, is that I want conjunction, implication and negation, but do not want to introduce disjunction. The ultimate reason is that I want all the proofs to have constructive content of certain kind. | |
| Dec 4, 2013 at 2:01 | answer | added | Margaret Friedland | timeline score: 1 | |
| Dec 3, 2013 at 16:36 | comment | added | François G. Dorais |
Presumably you don't allow $(A \to B) \to C$ for reasons Emil gave, but you could allow $A \to (B \to C)$ since that is equivalent to $(A \land B) \to C$. Maybe you don't allow nested implications at all as in Horn logic? Perhaps it would be best to include your current system in the question. Your description of != suggests that you are aiming at a form of intensional or definitional equality.
|
|
| Dec 3, 2013 at 16:02 | answer | added | Peter LeFanu Lumsdaine | timeline score: 5 | |
| Dec 3, 2013 at 15:37 | review | First posts | |||
| Dec 3, 2013 at 15:44 | |||||
| Dec 3, 2013 at 15:28 | comment | added | Emil Jeřábek | I can’t say I understand the description of the system, but if you have implication, you already have disjunction, as $\phi\lor\psi$ is equivalent to $(\phi\to\psi)\to\psi$. | |
| Dec 3, 2013 at 15:21 | history | asked | serras | CC BY-SA 3.0 |