I'm doing a project relating a logic topic. I chose cut-elimination and, although the topic seems quite interesting, my proffessor is asking us for applications, hopefully on other areas non related to logic. However I don't seem to find any articles relating this topic.
Could anybody provide me any reference to an application of cut-elimination?
On
That's a great question that..as someone who is trying to find an excuse to make a living out of studying formal logic...I should be asking myself.
Ever looked at linear logic?...And the cut elimination associated with that?...which SURPRISINGLY follows the Cut-Elimination Theorem?
But here's another surprise: It generalizes your standard classical/intuitionistic treatment of Gentzen Calculus, into a more general propositional language, that gets ugly in terms of its properties and semantics but it's actually getting a bit of hype from the computer science community as a good way to formalize programs mathematically. Here is a (quite dense) paper on this sort of thing for some inspiration.
Not sure how "non-related to logic" he wants the application to be, as computer science is a very logic-oriented discipline. But at least it's application to something outside the confinements of its own branch of mathematics.
The Prolog programming language depends on Gentzen's theorem in some ways.