Timeline for Philosophical interpretation of the cut rule of Sequent Calculus
Current License: CC BY-SA 3.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 15, 2023 at 3:56 | answer | added | emesupap | timeline score: 0 | |
| Feb 19, 2017 at 16:34 | comment | added | Mauro ALLEGRANZA | It seems to me that Cut implies MP but the two are not equiv. Consider : premise →A and axiom B→B and apply (L⊃) to derive A⊃B→B. Consider it right seq with left seq →A⊃B and apply Cut to get →B. | |
| Feb 18, 2017 at 11:33 | comment | added | Boris | @MauroALLEGRANZA I know we can make proofs without cuts but can we also do it without MP ? Since MP is related to the implication connector... | |
| Feb 18, 2017 at 9:07 | comment | added | Mauro ALLEGRANZA | A suitable sequent version of MP is : Top : Γ→A, Bottom : A⊃B,Γ→B It is derivable from L⊃⊥ with C=B and considering that with this the top right seq becomes B,Δ→B i.e. an axiom. | |
| Feb 17, 2017 at 19:57 | comment | added | user9166 | If an analogy to computing would help, cuts are like scope closures, they move the basic functionality from a linear scope by putting some intermediate values into scopes far away from the point of application, but with the upside of breaking the context up into navigable layers. You can definitely remove all the scope closures from a program and view it in a single local scope, you just have to recompute stuff locally that could already be stored at some intermediate scope. Thus they are hardly the basis of all logic, and you can easily have whole languages that don't admit them. | |
| Feb 17, 2017 at 16:11 | comment | added | Boris | @MauroALLEGRANZA In the Carbone-Semmes paper, the authors are often referring to "proofs without Modus Ponens". Do they mean "without cuts" or do they really mean the modus ponens related to the arrow symbol ? | |
| Feb 17, 2017 at 15:25 | history | edited | Boris | CC BY-SA 3.0 |
added 3 characters in body
|
| Feb 17, 2017 at 10:28 | answer | added | Mauro ALLEGRANZA | timeline score: 4 | |
| Feb 17, 2017 at 4:44 | history | tweeted | twitter.com/StackPhilosophy/status/832450642127917057 | ||
| Feb 16, 2017 at 23:47 | comment | added | Joseph Weissman♦ | Maybe we should make a community wiki answer for this one! | |
| Feb 16, 2017 at 21:52 | comment | added | Conifold | Dan Piponi's answer links to a very interesting Carbone-Semmes paper (from which I quoted) that explains dynamics and complexity in detail. By "topology" I meant that cuts allow "distant connections" in inferences, which create interweaving logical dependencies instead of just linear chains. | |
| Feb 16, 2017 at 21:37 | comment | added | Boris | @Conifold I also heard that cuts introduce "dynamics" but what does that mean ? And what do you mean by "topology" in that context ? | |
| Feb 16, 2017 at 20:32 | comment | added | Conifold | There was a similar question on Math Overflow. If I understand the jist cuts introduce nontrivial dynamics and topology into proving and thus make proofs (and everything that depends on them, like meaning, if you follow Dummett) complex and opaque, "proofs with lemmas correspond to implicit descriptions of some underlying objects or structures, while cut elimination is a process for converting these descriptions into explicit constructions". | |
| Feb 16, 2017 at 20:01 | comment | added | Mauro ALLEGRANZA | You can see also this post on cut elimination. | |
| Feb 16, 2017 at 14:56 | comment | added | Boris | @MauroALLEGRANZA Thanks for these references ! | |
| Feb 16, 2017 at 14:06 | comment | added | Mauro ALLEGRANZA | Maybe useful SEP's entries : The Development of Proof Theory and Proof-Theoretic Semantics. | |
| Feb 16, 2017 at 12:56 | comment | added | Mauro ALLEGRANZA | See also Curtis Franks, Cut as Consequence (2010). | |
| Feb 16, 2017 at 12:55 | comment | added | Mauro ALLEGRANZA | A useful discussion is into Jan von Plato, Elements of Logical Reasoning, Cambridge (2013), Ch.13 Normalization and cut elimination. | |
| Feb 16, 2017 at 12:47 | comment | added | Mauro ALLEGRANZA | You can see the intro to Matthias Baaz & Alexander Leitsch, Methods of Cut-elimination, Springer (2011) | |
| Feb 16, 2017 at 12:23 | history | asked | Boris | CC BY-SA 3.0 |