Lehman College - CUNY Graduate Center
Gödel inaugurated a project of finding an arithmetic semantics for intuitionistic logic, but did not complete it. It was finished by Sergei Artemov, in the 1990’s. As part of this work, Artemov introduced the first justification logic, LP, (standing for logic of proofs). This is a propositional modal-like logic, with an infinite family of proof or justification terms, and can be seen as an explicit version of the well-known modal logic S4. There is a possible world semantics for LP (due to me). Since then, many other justification logic/modal logic pairs have been investigated, and justification logic has become a subject of independent interest, going beyond the original connection with intuitionistic logic. It is now known that there are infinitely many justification logics, but the exact extent of the family is not known. Justification logics are connected with their corresponding modal logics via Realization Theorems. A Realization Theorem connecting LP and S4 has a constructive proof, but there are other cases for which realization holds, but it is not known if a constructive proof exists. More recently, a first order version of LP has been developed, but I will not talk about it in detail. I will present a sketch of the basic propositional ideas.
Lehman College Professor Melvin Fitting received the Herbrand Award of 2012 for his groundbreaking contributions to the field of automated theorem proving, which focuses on getting computer programs to prove logical and mathematical deductions.