Higher-order constants can be used to prove false

[chaudhuri]

This is a slightly edited summary of an email from @gnadathur97:

---

Sebastiaan Joosten, a lecturer in my department, was able to write the following definitions in Abella without even getting a warning:

Type naive (set -> prop) -> set.

Define setmember : set -> set -> prop by
  setmember S (naive P) := P S.

Define nomember_of_itself : set -> prop by
  nomember_of_itself S := setmember S S -> false.

[T]he following clauses are instances of the clauses in these definitions:

setmember (naive nomember_of_itself) (naive nomember_of_itself) :=
  nomember_of_itself (naive nomember_of_itself).

nomember_of_itself (naive nomember_of_itself) :=
  setmember (naive nomember_of_itself) (naive nomember_of_itself) -> false.

Not surprisingly, Sebastiaan was able to generate a proof of false from the definitions.

[chaudhuri]

This is not completely fixed. Negative instances of prop can be hidden with polymorphic types.

[sjcjoosten]

I managed to minimize the script and the proof I found, the idea is still based on Russel's paradox in naive set theory (hence the names):

Kind set type.
Type naive (set -> prop) -> set.

Define nomember_of_itself : set -> prop by
  nomember_of_itself (naive S) := S (naive S) -> false.

Theorem nomember_of_itself : nomember_of_itself (naive nomember_of_itself) -> false.
  intros. case H1. backchain H2.

Theorem oops: false.
  assert (nomember_of_itself (naive nomember_of_itself) -> false) -> false.
    intros. backchain H1. apply H1 to nomember_of_itself.

(Edit: tested in commit #74770b6d1dff51084c3ec5d73b86d9293047bfaf, and as expected also this shortened proof no longer works there, unless prop is hidden inside polymorphism.)

[chaudhuri]

No, it still works if you have Type naive (set -> A) -> set.

As I understand it, @gnadathur97's suggestion is to instead prevent definitions such as nomember_of_itself because it has a parameter S whose type contains prop.

For now I will just add a warning for this kind of definition. Preventing such definitions will break some existing examples that use "higher-order" definitions that were used as a shortcut to a decent module system in Abella.

[sjcjoosten]

I'm pleased to hear that the solution will be to generate warnings somewhere along the way: it's nice to be able to experiment with parameters that contain prop.

[chaudhuri]

The new version just emits a warning and lists all the higher-order parameters. Not yet sure which scenarios are definitely errors and which are in some kind of grey area.

[chaudhuri]

Closing this. Please comment if you discover anything else strange.