[isabelle-dev] [isabelle] Tiny minor backward-compatible changes to IFOL

[Viktor Kuncak]

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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>