Sur les quantificateurs pour le raisonnement quantitatif

Nous explorons un type de logique des prédicats du premier ordre avec une sémantique intended dans les réels. Par rapport à d'autres approches dans la littérature, nous travaillons principalement dans les réels multiplicatifs 0, , montrant qu'ils supportent trois générations de connecteurs, que nous appelons non-linéaires, additifs linéaires et multiplicatifs linéaires. Les moyennes et les moyennes harmoniques émergent comme des candidats naturels pour les quantificateurs existentiels et universels bornés, et en fait nous voyons qu’ils se comportent comme prévu par rapport aux autres connecteurs logiques. Nous expliquons ce fait par le fait bien connu que min/max et moyenne arithmétique/moyenne harmonique se situent à des extrémités opposées d'un spectre, celui des moyennes p. Nous donnons une syntaxe et une sémantique pour cette logique des prédicats quantitatifs, et en tant qu'applications d'exemple, nous montrons comment softmax est la sémantique quantitative d'argmax, et l'entropie de R\'enyi/nombres de Hill sont des sémantiques additifs/multiplicatifs de la même formule. En effet, les réels additifs s'intègrent également dans l'histoire en exploitant la dualité Napierienne -log 1/exp, ce qui met en évidence une distinction formelle entre les quantités «additives» et «multiplicatives». Enfin, nous décrivons deux tentatives de sémantique catégorique via des hyperdoctrines enrichies. Nous discutons pourquoi les hyperdoctrines sont en fait probablement inadéquates pour ce type de logique.