{"id":3248,"date":"2017-02-15T12:36:00","date_gmt":"2017-02-15T11:36:00","guid":{"rendered":"https:\/\/www.illc.uva.nl\/lgc\/seminar\/?p=3248"},"modified":"2017-03-05T19:49:27","modified_gmt":"2017-03-05T18:49:27","slug":"lira-session-greg-restall","status":"publish","type":"post","link":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/2017\/02\/lira-session-greg-restall\/","title":{"rendered":"LIRa session: Greg Restall"},"content":{"rendered":"<p>Speaker:\u00a0<a href=\"http:\/\/consequently.org\/\">Greg Restall<\/a> (University of Melbourne)<\/p>\n<p>Date and Time: Monday, March&nbsp;6th 2017, 16:00-17:30<\/p>\n<p>Venue: KdVI Seminar Room F3.20, Science Park 107.<\/p>\n<p>Title: <strong>Proof Terms for Classical Derivations<\/strong>.<\/p>\n<p><em>Abstract<\/em>. I give an account of proof terms for derivations in a sequent calculus for classical propositional logic. The term for a derivation \u03b4 of a sequent \u03a3\u227b\u0394 encodes how the premises \u03a3 and conclusions \u0394 are related in \u03b4. This encoding is many\u2013to\u2013one in the sense that different derivations can have the same proof term, since different derivations may be different ways of representing the same underlying connection between premises and conclusions. However, not all proof terms for a sequent \u03a3\u227b\u0394 are the same. There may be different ways to connect those premises and conclusions.<br \/>\nProof terms can be simplified in a process corresponding to the elimination of cut inferences in sequent derivations. However, unlike cut elimination in the sequent calculus, each proof term has a unique normal form (from which all cuts have been eliminated) and it is straightforward to show that term reduction is strongly normalising \u2014 every reduction process terminates in that unique normal form. Further- more, proof terms are invariants for sequent derivations in a strong sense \u2014 two derivations \u03b41 and \u03b42 have the same proof term if and only if some permutation of derivation steps sends \u03b41 to \u03b42 (given a relatively natural class of permutations of derivations in the sequent calculus). Since not every derivation of a sequent can be permuted into every other derivation of that sequent, proof terms provide a non-trivial account of the identity of proofs, independent of the syntactic representation of those proofs.<\/p>\n<p>Link: <a href=\"http:\/\/consequently.org\/writing\/proof-terms-for-classical-derivations\/\">http:\/\/consequently.org\/writing\/proof-terms-for-classical-derivations\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Speaker:\u00a0Greg Restall (University of Melbourne)<br \/>\nDate and Time: Monday, March&nbsp;6th 2017, 16:00-17:30<br \/>\nVenue: KdVI Seminar Room F3.20, Science Park 107.<br \/>\nTitle: Proof Terms for Classical Derivations.<br \/>\nAbstract. I give an account of proof terms for derivations in a sequent calculus for classical propositional logic. The term for a derivation \u03b4 of a sequent \u03a3\u227b\u0394 encodes how the premises \u03a3 [&#8230;]<\/p>\n","protected":false},"author":11,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[4],"tags":[],"class_list":["post-3248","post","type-post","status-publish","format-standard","hentry","category-events"],"_links":{"self":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/3248","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/users\/11"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/comments?post=3248"}],"version-history":[{"count":5,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/3248\/revisions"}],"predecessor-version":[{"id":3256,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/3248\/revisions\/3256"}],"wp:attachment":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/media?parent=3248"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/categories?post=3248"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/tags?post=3248"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}