Value of intuitionistic logic

[cianfa72]

TL;DR

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 united with the complement of 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!

 

[cianfa72]

Ah yes, indeed thinking about it ¬P is defined as
¬P := P → ⊥
and any topological model/interpretation maps ⊥ to the empy set. Then, by using the definition of → logic connective in any topological model, one gets the result.

 

[cianfa72]

In any topological model for IPL, propositions are assigned open subsets of an underlying topological space by induction starting assigning open subsets to propositional variables (i.e. to atomic propositions). This semantics do not assign any binary truth-value to propositions, i.e. one can't say whether an atomic or a composite proposition is True or False in a given topological model/interpretation. The claim we can make is that a given IPL's wff (proposition) is valid iff its assigned open set is the entire space (that's open by definition of topology).

In case of first-order intuitionistical logic, the above extends to closed wffs.

 

[gentzen]

This semantics do not assign any binary truth-value to propositions, i.e. one can't say whether an atomic or a composite proposition is True or False in a given topological model/interpretation.

Well, we still say that a proposition which is True everywhere is just True (or top ⊤), and a proposition which is True only on the empty set (or bottom ⊥/initial object) is False.

The claim we can make is that a given IPL's wff (proposition) is valid iff its assigned open set is the entire space (that's open by definition of topology).

You can say that the wff is valid, if you want, but you can also just say that it is True.

In case of first-order intuitionistical logic, the above extends to closed wffs.

Yes. No need to force this open subsets semantics over to first-order logic. The first google hit for a reference described it only as a semantics for IPL, and most other references you will find restrict themselves in the same way.
The case of first-order intuitionistical logic is of historical interest, when Gödel, Gentzen, and Heyting studied the consistency of Peano arithmetic, or rather its provability. Well understood topics in that context are Double-negation translation, Heyting arithmetic, and Brouwer–Heyting–Kolmogorov interpretation.

The relevance of intuitionistic logic today comes more from higher-order logic and type theories. Basically, the split into first-order logic and ZFC as an axiomatic first-order logic theory only works well for classical logic. For intuitionistic logic, a tighter integration between logic and set theory makes more sense.

 

[cianfa72]

Well, we still say that a proposition which is True everywhere is just True (or top ⊤), and a proposition which is True only on the empty set (or bottom ⊥/initial object) is False.

Ok, you mean that a proposition is True on the elements of the topological model assigned open subset. Then if such a set is the entire space we can just say it is True, contrasts with the case of empty set when it is False.

You can say that the wff is valid, if you want, but you can also just say that it is True.

Better, I'd say it is valid when it is True (in the above sense) regardless of the specific topological model/interpretation.

 

[gentzen]

Ok, you mean that a proposition is True on the elements of the topological model assigned open subset. Then if such a set is the entire space we can just say it is True, contrasts with the case of empty set when it is False.

Yes.

Better, I'd say it is valid when it is True (in the above sense) regardless of the specific topological model/interpretation.

Yes, good point: True is used with respect to a specific model. For statements concerning all models, a different terminology is used. When coming from the syntax side, one could just say provable. I don't remember the terminology when coming from the model/semantics side, but valid sounds right to me.

 

[cianfa72]

When coming from the syntax side, one could just say provable. I don't remember the terminology when coming from the model/semantics side, but valid sounds right to me.

Yes, valid is understood as semantically valid.