Stream: Beginner Questions

Topic: Mechanisms for blocking "nonsensical" statements

Patrick Nicodemus (May 07 2023 at 21:27):

One of the common criticisms of set theory is that it permits "nonsensical" sentences like "2 \in 3".
I would like to know what superficial features Isabelle has that block such things. Maybe one can use locales for this but I'm not yet experienced enough to see how one does this.
By superficial, I mean not at the level of the logic, or with subtyping, but some kind of elementary guard at the user interface level to prevent the user from writing unintended / stupid things; perhaps toggleable.

For example, suppose $A$ is a type, $a$ is a subset of $A$, and I have a binary relation $R$ that is defined on $a$. For technical convenience I have defined $R : A \to A\to \mathsf{bool}$ but I only regard $R(x,y)$ as meaningful if $x,y\in a$. I could form a true subtype from $a$ using typedef but this cannot be done if $a$ is variable rather than a constant closed term, I cannot apply theorems about all subsets of $A$ to $a$, and so on. Are there any guards I could use that prevent me from writing $R(x,y)$ unless there is a proof or assumption in the local context that $x,y\in a$?

Patrick Nicodemus (May 07 2023 at 21:32):

I am interested in developing mathematics in ZFC drawing on the ZFC in HOL AFP article and this becomes particularly important there where you have many diverse mathematical objects inhabiting one type, you would want to overload symbols for different constant terms of that type, and so on. For example if I implement ordered pairs using Kuratowski pairs I can ask whether $x\in \left\langle x, y\right\rangle$ but I'm looking for a way to stop myself from doing that in terms of rules at the user interface level without adding additional complexity to the underlying logic by working with the type of ordered pairs.

Patrick Nicodemus (May 07 2023 at 21:37):

I understand this is the whole point of type theory lol but it seems that (past a certain point?) the use of types tends to add complexity to automation.

Sławomir Kołodyńaski (May 08 2023 at 06:28):

That $2 \in 3$ is rather a bad example of a nonsensical statement in set theory. Of course in ZF for a natural number $n>0$ one has $n = \{0,1, ... n-1\}$ , hence instead of writing $k \in \{0,1, ... , n-1\}$ one can always write $k\in n$ which is shorter and does not require special syntax for those three dots. I use that fact quite often in IsarMathLib, for example recently in the statement of the binomial theorem. One person's nonsensical statement can be another person's useful fact.

Patrick Nicodemus (May 08 2023 at 12:08):

Yeah that's a stupid example. It's just the one everyone uses.

Patrick Nicodemus (May 08 2023 at 12:08):

https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems/90945#90945

Patrick Nicodemus (May 08 2023 at 12:10):

how about just apply f x where f is a function and we want x to be in the domain of f

Sławomir Kołodyńaski (May 10 2023 at 18:40):

The only related mechanism that comes to my mind is that in Isabelle/Isar definitions can have premises (see this as an example). Using such definition requires the premises to hold in the local context. This feature is orthogonal to the sets vs. types question and is not at the user interface (syntax) level. This answer suggests that the mechanism you ask about is rather difficult to implement, at least in FOL.

Last updated: Apr 27 2024 at 20:14 UTC