{"id":98,"date":"2024-05-15T03:37:32","date_gmt":"2024-05-15T03:37:32","guid":{"rendered":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/?p=98"},"modified":"2024-05-15T03:37:32","modified_gmt":"2024-05-15T03:37:32","slug":"discussing-an-algebraic-and-kripke-style-approach-to-a-certain-extension-of-intuitionistic-logic","status":"publish","type":"post","link":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/05\/15\/discussing-an-algebraic-and-kripke-style-approach-to-a-certain-extension-of-intuitionistic-logic\/","title":{"rendered":"Discussing \u201cAn algebraic and Kripke-style approach to a certain extension of intuitionistic logic\u201d"},"content":{"rendered":"\n

(Link)<\/a><\/p>\n\n\n\n

Author:<\/strong> Cecylia Rauszer (University of Warsaw)<\/p>\n\n\n\n

Reference:<\/strong> Rauszer, Cecylia (1980). An algebraic and Kripke-style approach to a certain extension of intuitionistic logic. Dissertations Mathematicae, Polish Scientific Publishers, pp. 1\u201367.<\/p>\n\n\n\n

Why this paper?<\/strong> Cited by Rules of Explosion and Excluded Middle: Constructing a Unified Single-Succedent Gentzen-Style Framework for Classical, Paradefinite, Paraconsistent, and Paracomplete Logics<\/a> and Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents<\/a><\/p>\n\n\n\n

Heyting-Brouwer logic (more commonly known now as bi-intuitionistic logic) has fascinated me since I first learned of it. The idea is beguilingly simple: extend intuitionistic logic with a new connective that makes it completely symmetrical. The \u2018symmetry\u2019 I am thinking of (perhaps better called \u2018duality\u2019, but not quite the same thing as De Morgan duality) is already exhibited by most of the propositional connectives: truth, which is entailed by everything, is dual to falsity, which entails everything; conjunction, which is a sort of greatest lower bound, is dual to disjunction, which is a least upper bound. But implication (and hence negation, which is definable via implication and false) has no dual in this way. What happens if we \u2018fix\u2019 this?<\/p>\n\n\n\n

We get a new binary connective which Rauszer writes \u2018\u2238\u2019 and calls \u2018Brouwerian implication\u2019 and \u2018pseudo-difference\u2019. It has gone by various symbols and names over the years including \u2018subtraction\u2019, \u2018coimplication\u2019, and \u2018exclusion\u2019; I have taken to pronouncing p \u2238 q as \u2018p without<\/em> q\u2019 because that is the best fit in natural language I can make with my intuition (warning: this is purely my invention and does not appear in the literature!). It is not hard to define via symmetry: just as implication can be defined\u00a0 by \u2018residuation\u2019 with conjunction, \u2018p and q entails r\u2019 exactly if \u2018p entails q implies r\u2019, we use disjunction: \u2018p \u2238 q entails r\u2019 exactly if \u2018p entails q or r\u2019. Now just as we can define negation from implication, with \u2018not p\u2019 and \u2018p implies false\u2019, we can define another notion of negation on p as \u2018true \u2238 p\u2019.<\/p>\n\n\n\n

It’s worth taking a moment to enjoy some of the odd properties of this logic. First, the usual negation of p implies the dual negation of p, but not vice versa; for this reason, the dual negation is now often called \u2018weak negation\u2019. Weak indeed, because weak negation is not \u2018explosive\u2019: there is no contradiction in general between p and weak-not p. Weak negation instead satisfies the law of the excluded middle! Have we collapsed to classical logic, then? One of the contributions of this paper (already known from earlier work by Rauszer I believe, but with a particularly pleasant proof here) is that bi-intuitionistic logic is in fact conservative over intuitionistic logic, so any theorem of this logic that does not use \u2238 holds exactly if it holds in intuitionistic logic. Therefore while bi-intuitionistic logic is clearly not a constructive logic \u2013 its weak law of the excluded middle contradicts the disjunction property \u2013 is it has constructive logic nicely contained inside it. If we do collapse to classical logic then \u2018p \u2238 q\u2019 collapses to \u2018p and not q\u2019 (just as \u2018p implies q\u2019 collapses to \u2018not p or q\u2019).<\/p>\n\n\n\n

So much for the syntactic view \u2013 what does this new connective mean<\/em>? This paper gives answers in both algebraic and Kripke style; I will focus on the Kripke frames approach. In fact bi-intuitionistic logic can be interpreted in the exact same models as the usual intuitionistic logic (making the conservativity result obvious). We have a set of \u2018possible worlds\u2019 with a reflexive and transitive relation between them, and all propositions are preserved by this relation. We think of the relation as moving from one state of knowledge to another, learning new facts but never forgetting old ones. In this setting \u2018p implies q\u2019 asks that for all future<\/em> worlds, either p fails, or q holds. By duality p \u2238 q means that there exists<\/em> a past<\/em> world where p holds and q fails. Similarly, the usual negation of p asks that p fails in all future worlds, whereas the weak negation of p says that p fails in some past world. We can now see why the weak negation is not explosive (it could be that p failed in the past, but now holds), and satisfies excluded middle (if p does not currently hold, it fails at a past world \u2013 by reflexivity, the current world will do as a witness). This also gives a different view of how the logic is not constructive; p \u2238 q holds if we can construct p in a way that does not require q be constructible, but the latter notion is not itself a construction.<\/p>\n","protected":false},"excerpt":{"rendered":"

Heyting-Brouwer logic (more commonly known now as bi-intuitionistic logic) has fascinated me since I first learned of it. The idea is beguilingly simple: extend intuitionistic logic with a new connective that makes it completely symmetrical. The \u2018symmetry\u2019 I am thinking of (perhaps better called \u2018duality\u2019, but not quite the same thing as De Morgan duality) is already exhibited by most of the propositional connectives: truth, which is entailed by everything, is dual to falsity, which entails everything; conjunction, which is a sort of greatest lower bound, is dual to disjunction, which is a least upper bound. But implication (and hence negation, which is definable via implication and false) has no dual in this way. What happens if we \u2018fix\u2019 this?<\/p>\n","protected":false},"author":10,"featured_media":99,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":"","_share_on_mastodon":"0","_share_on_mastodon_status":"Today's #blog looks at a quirky and fascinating extension of intuitionistic #logic, introduced by Polish mathematician Cecylia Rauszer in the 70s. %permalink%"},"categories":[5],"tags":[129,130,126,128,127],"class_list":["post-98","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-summaries","tag-129","tag-bi-intuitionistic-logic","tag-cecylia-rauszer","tag-dissertations-mathematicae","tag-university-of-warsaw"],"share_on_mastodon":{"url":"https:\/\/fediscience.org\/@RanaldClouston\/112443015340940121","error":""},"_links":{"self":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/98","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/users\/10"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/comments?post=98"}],"version-history":[{"count":1,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/98\/revisions"}],"predecessor-version":[{"id":100,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/98\/revisions\/100"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/media\/99"}],"wp:attachment":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/media?parent=98"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/categories?post=98"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/tags?post=98"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}