Timeline for Non-Computational classical subterms
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 7, 2012 at 22:02 | comment | added | Christoph-Simon Senjak | I am not currently working for Schwichtenberg. This is just something that interests me. However, I do not see a deeper connection to the principle of independence of premise. | |
| Jan 7, 2012 at 22:01 | history | edited | Christoph-Simon Senjak | CC BY-SA 3.0 |
added 1238 characters in body
|
| Jan 7, 2012 at 7:51 | comment | added | Andrej Bauer | I am not sure I really understand your question, but I think you want to look up independence of premise, en.wikipedia.org/wiki/Independence_of_premise, and wonder why the premise cannot be moved when it is classical. | |
| Jan 7, 2012 at 7:42 | comment | added | Andrej Bauer | Yes thanks, you should have said "minilog" or "Schwichtenberg" at the very beginning. Say hi to prof. Schwichtenberg! | |
| Jan 6, 2012 at 22:32 | comment | added | Christoph-Simon Senjak | Ok, I edited it, is it clearer now? | |
| Jan 6, 2012 at 22:32 | history | edited | Christoph-Simon Senjak | CC BY-SA 3.0 |
added 433 characters in body
|
| Jan 6, 2012 at 21:05 | comment | added | Andrej Bauer | Sorry, can't follow. You're writing down proof terms? What are those c's and nc's on the arrows? I think it would help if you used standard first-order logic notation. | |
| Jan 6, 2012 at 20:01 | history | asked | Christoph-Simon Senjak | CC BY-SA 3.0 |