James Hanson (May 28 2024 at 15:17): James Hanson (May 28 2024 at 15:17):Is there an existing Isabelle/HOL library for first-order logic syntax and semantics that supports contexts with uncountably many variables? I've been playing around with trying to formalize some model theory and uncountable contexts show up semi-frequently once you get to more advanced model theory. Looking around, though, it seems like most of the libraries end up hard coding natural-indexed variables. (I've also tried to write this myself, but I think it's a bit beyond my ability to do robustly at the moment.)
Jonathan Julian Huerta y Munive (May 28 2024 at 16:39):Does trm in this AFP entry represent what you are searching for?
Jonathan Julian Huerta y Munive (May 28 2024 at 16:40):(see Formula > datatype trm)
Last updated: Dec 21 2024 at 16:20 UTC