On 11/08/2012, at 17:05, Bill Richter <[email protected]> wrote:
> My main problem is that I don't understand HOL, so I don't know what theorems > HOL Light is proving for me. The HOL4 Logic manual looks like a very > respectable CS document, but I haven't been able to read it yet, and it's not > a HOL Light document. HOL Light and HOL4 implement the same logic by design. For this reason, the Logic Manual is the best reference describing the HOL Light logic's semantics. > With my Tarski code, I would be happy to say (though I don't quite understand > it) that HOL Light was verifying my FOL proofs using Tarski's geometry > axioms. But there's real HOL in my Hilbert code funneled through sets.ml. > Of course I know what results I meant to prove, and my results use sets as > mathematicians customarily use sets. I figure that's the result that HOL > Light proved for me, but I'm missing the translation. Sets in HOL Light and HOL4 are predicates over their respective types. Types correspond to non-empty sets (as already discussed). So, because any predicate bounded above corresponds to a ZFC set, the sets in HOL do also correspond to ZFC sets. Michael ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
