City University of New York, USA
City University of New York, USA
"A Few Intuitionistic Logics"
"A Few Intuitionistic Logics"
Embedded Files
Intuitionistic logic was formulated in the 1930’s by Arend Heyting, and was designed to embody the reasoning of an intuitionistic mathematician (HPC, for “Heyting Predicate Calculus”). A rough equivalent to “intuitionist” here is “constructivist”. HPC has been much studied ever since for a surprisingly broad range of reasons, but that does not concern us here. In the 1960’s Saul Kripke introduced the now standard possible world semantics for intuitionistic logic, formally capturing the ideas embodied in intuitionistic reasoning though it requires classical mathematics to show that it is Heyting’s calculus that it captures.
Intuitionistic logic was formulated in the 1930’s by Arend Heyting, and was designed to embody the reasoning of an intuitionistic mathematician (HPC, for “Heyting Predicate Calculus”). A rough equivalent to “intuitionist” here is “constructivist”. HPC has been much studied ever since for a surprisingly broad range of reasons, but that does not concern us here. In the 1960’s Saul Kripke introduced the now standard possible world semantics for intuitionistic logic, formally capturing the ideas embodied in intuitionistic reasoning though it requires classical mathematics to show that it is Heyting’s calculus that it captures.
As a matter of fact, a person with constructivist motivations does not exclusively reason about mathematics. The real world is doubtless a subject of interest too. But concerning the real world, we may have gaps in our knowledge. Or we may have contradictory information to work with, often called gluts. Relatives of classical logic have been introduced for such reasoning. Perhaps the most common are the logic of paradox, LP, for gluts; Kleene’s strong three-valued logic, K3, for gaps, and first-degree entailment, FDE, for both. But these do not take constructivist motivations into account.
As a matter of fact, a person with constructivist motivations does not exclusively reason about mathematics. The real world is doubtless a subject of interest too. But concerning the real world, we may have gaps in our knowledge. Or we may have contradictory information to work with, often called gluts. Relatives of classical logic have been introduced for such reasoning. Perhaps the most common are the logic of paradox, LP, for gluts; Kleene’s strong three-valued logic, K3, for gaps, and first-degree entailment, FDE, for both. But these do not take constructivist motivations into account.
It turns out there are intuitionistic analogs of the logics just mentioned, LP, K3, and FDE. These are what I will discuss. Intuitionistic versions have a Kripke-style semantics, natural tableau proof systems, and share many of their fundamental properties with Heyting’s calculus. But much is still unknown, since this is all rather new.
It turns out there are intuitionistic analogs of the logics just mentioned, LP, K3, and FDE. These are what I will discuss. Intuitionistic versions have a Kripke-style semantics, natural tableau proof systems, and share many of their fundamental properties with Heyting’s calculus. But much is still unknown, since this is all rather new.
For background, Heyting’s own explanation is still good reading: Intuitionism: An Introduction, North-Holland Publishing Co, 1956, revised edition 1971. Kripke’s paper on intuitionistic semantics is of historical importance, but a more friendly discussion can be found in Wikipedia’s article, Kripke Semantics. My own work has partly appeared. A background paper appeared in Notre Dame Journal of Formal Logic earlier this year, Simple tableaus for simple logics. The main material discussed in my talk will appear in the same journal as Simple tableaus for simple intuitionistic logics. It may even be out by the time I give my talk.
For background, Heyting’s own explanation is still good reading: Intuitionism: An Introduction, North-Holland Publishing Co, 1956, revised edition 1971. Kripke’s paper on intuitionistic semantics is of historical importance, but a more friendly discussion can be found in Wikipedia’s article, Kripke Semantics. My own work has partly appeared. A background paper appeared in Notre Dame Journal of Formal Logic earlier this year, Simple tableaus for simple logics. The main material discussed in my talk will appear in the same journal as Simple tableaus for simple intuitionistic logics. It may even be out by the time I give my talk.
Google Sites
Report abuse