I Value of intuitionistic logic

[cianfa72]

TL;DR Summary

About the value and significance of intuitionistic logic in modeling some kind of worlds.

I'm taking a look at intuitionistic propositional logic (IPL). Basically it exclude Double Negation Elimination (DNE) from the set of axiom schemas replacing it with Ex falso quodlibet: ⊥ → p for any proposition p (including both atomic and composite propositions).

In IPL, for instance, the Law of Excluded Middle (LEM) p ∨ ¬p is no longer a theorem.

My question: aside from the logic formal perspective, is IPL supposed to model/address some specific "kind of world" ?

Thanks.

 

[gentzen]

My question: aside from the logic formal perspective, is IPL supposed to model/address some specific "kind of world" ?

Independent of whether IPL is "supposed to model", it does model various specific "kind of world(s)". Or in other words, there are a variety of semantics for IPL:

• categorical semantics
• Kripke semantics
• open subsets semantics (aka topological semantics)

Your formulation "kind of world" sounds closest to Kripke semantics:

Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics)^[1] is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal.

That semantics is useful for exploring the relation between IPL and various systems of modal logics (for example). However, even so modal logics have many important applications in mathematical logic, they are a quite technical subject.

The open subsets semantics is probably easiest to understand: Propositions are open subsets of a topological space, "A and B" is the intersection of the subsets corresponding to A and B, "A or B" is the union of the subsets corresponding to A and B, and "A implies B" is the interior (with respect to the topology) of the subset corresponding to B minus the subset corresponding to A. (Here is the first google hit for a reference.)

Before I say some words about categorical semantics, let me mention that an important common thread between all those different semantics is that one asks "Where is the proposition true?" instead of asking "Is the proposition true?".

In categorical semantics, one looks for the type of category for which a given logic is the internal language. Some simpe prototypical examples are:

Theory	Category
minimal logic	cartesian closed category
extensional dependent types	locally cartesian closed category
constructive higher order	elementary topos
linear logic	symmetric monoidal category

Minimal logic is essentially IPL, only the ex falso quodlibet rule ⊥⊢A is missing. So IPL corresponds essentially to the type of cartesian closed category. This means that any cartesian closed category is a model of minimal logic, and I guess those with an initial object will be a model of IPL.

 

[cianfa72]

Independent of whether IPL is "supposed to model", it does model various specific "kind of world(s)". Or in other words, there are a variety of semantics for IPL:

• categorical semantics
• Kripke semantics
• open subsets semantics (aka topological semantics)

That semantics is useful for exploring the relation between IPL and various systems of modal logics (for example). However, even so modal logics have many important applications in mathematical logic, they are a quite technical subject.

Ok, you said semantics (plural noun) since it refers to an entire class of semantic models/interpreations and not just a single one. So for instance we talk of Kripke semantics to mean the entire class of Kripke semantic models.

The open subsets semantics is probably easiest to understand: Propositions are open subsets of a topological space, "A and B" is the intersection of the subsets corresponding to A and B, "A or B" is the union of the subsets corresponding to A and B, and "A implies B" is the interior (with respect to the topology) of the subset corresponding to B minus the subset corresponding to A.

Ok, therefore in the open subset semantics (plural noun) as semantic models for IPL, the law of noncontradiction should holds regardless of the specific open subset interpretation (singolar) chosen -- i.e. ¬(P ∧ ¬P) is assigned the complement of the empty set which is open by definition of topology.

What about the Law of Excluded Middle (LEM) P ∨ ¬P ? It should correspond as well to the underlying entire set as above. Why isn't this a theorem of IPL ?

 

[gentzen]

Ok, you said semantics (plural noun) since it refers to an entire class of semantic models/interpreations and not just a single one.

No, "semantics" just means "theory of meaning". Even so you could talk of "theories of meaning", there is no way to put "semantics" into plural form. In logic, one contrasts syntax and semantics.

What about the Law of Excluded Middle (LEM) P ∨ ¬P ? It should correspond as well to the underlying entire set as above. Why isn't this a theorem of IPL ?

Well, take the real numbers $\mathbb R$ as your topological space, and $P:=(-\infty,0)$. Then you get $\lnot P=(0,\infty)$ and $P\lor \lnot P=(-\infty,0)\cup(0,\infty) =\mathbb R \backslash \{0\}$.

 

[cianfa72]

No, "semantics" just means "theory of meaning". Even so you could talk of "theories of meaning", there is no way to put "semantics" into plural form. In logic, one contrasts syntax and semantics.

Ah ok, so basically in logic semantic as noun doesn't exist/apply at all.

Well, take the real numbers $\mathbb R$ as your topological space, and $P:=(-\infty,0)$. Then you get $\lnot P=(0,\infty)$ and $P\lor \lnot P=(-\infty,0)\cup(0,\infty) =\mathbb R \backslash \{0\}$.

Ah, so is $\lnot P$ assigned the interior of the complement of the open subset assigned to P ?

 

[gentzen]

Ah, so is $\lnot P$ assigned the interior of the complement of the open subset assigned to P ?

Yes!