We often think of a proof as a list of statements, where each statement is justified by some number of previous statements via an axiom. It is shockingly useful to instead reason, not about individual statements, but about the conclusion of statements from assumptions. In such a system, the logical rules correspond to intuitive definitions of logical connectives, like implication and quantification. A more subtle advantage is that reasoning in this way allows us to restrict the structure of the sets of assumptions and conclusions. Restricting in different ways captures dozens of rich logics, including intuitionistic logic, Girard’s linear logic, and Lambek calculus. We will focus on Lambek calculus and its extensions and find that this non-commutative logic is very well-suited to linguistic analysis.
Eben Blaisdell (Univ. of Pennsylvania) – “Proof Theory and Linguistics” (see abstract)
For this week’s upcoming SIAM talk, we have a special guest speaker from the University of Pennsylvania. Eben Blaisdell will present on “Proof Theory and Linguistics” Monday, March 7, at 2 pm. Can’t wait to see you there!
