That wikipedia page would benefit from some more work. :)
I have come across and used the \exists_{\le k} notation in
(non-formalized) papers on FOL with counting.
I would agree that counting quantifiers are quite useful and natural,
including in HOL. Are they defined there?
The general pattern here is that we have a binary relation on cardinals,
say, r, and wish to abbreviate
r (card {x. P}) k
by writing something that, in latex, renders like:
\exists_{r\ k}. P
So, r can be \le, \ge, = and there are variants when k is the first
uncountable cardinal, to say, e.g. that there exist infinitely many:
https://math.stackexchange.com/questions/3383227/exists-infinitely-many-as-a-numerical-quantifier
Best regards
Viktor
On 27/04/2020 13:49, Makarius wrote:
On 27/04/2020 13:08, Lawrence Paulson wrote:
I have only recently proved a result of this sort, and thinking back, the need
to write out
!x y. P x & P y —> x=y
has always been one of my pet bugbears.
I don’t think a fancy symbol is needed for something that will be fairly
lightly used however.
So why not put it into some library theory somewhere?
There is no need to change the presentation of the core logic, just for
another variant of quantifiers.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
