Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?

Marco B. Caminati, Manfred Kerber, Christoph Lange +1

When faced with the question of how to represent properties in a formal proof system any user has to make design decisions. We have proved three of the theorems from Maskin's 2004…