Thanks for correcting my typed LC, Ramana: no Y combinator (that makes sense, as Y sorta comes from Russell's paradox, which typing was designed to prevent), and it's "simply typed LC". My "heavy" was just slang, and "generated" is from Hales's Notices article. Maybe I wasn't clear about syntax and semantics, so I'll try again. Let me first disagree with your comparison between FOL & HOL, in my case where FOL means ZC/FOL: (semantics) | (semantics) domain | type interpretation | definition of constants I say the semantics for both is mostly a model of ZC, i.e. a huge collection of sets, as the HOL Logic manual explains at the very beginning. I want to reserve the word type to mean syntax as you wrote yourself: (typed) variables. Then the semantics must interpret the syntax (including types) in terms of sets.
Types are not sets! That's what I didn't understand. ind->bool is a type, and terms can have this type, but ind->bool is not a set. The semantic function M take this type to a set, quite likely the power set of the natural numbers P(N), which is more or less the set of real numbers R. You this distinction on p 15 of the Logic manual: The terms of the HOL logic are expressions that denote elements of the sets denoted by types. So P(N) is the set denoted by the type ind->bool, and if the variable x has type ind->bool, the semantic function maps x to an element of the set P(N). Surely the HOL experts know this (obvious Michael & Konrad do), and I can understand the experts blurring the distinction between syntax and semantics in an effort to explain HOL, but it's this blurring will I think be very confusing to mathematicians trying to understand HOL in terms of what they learned from e.g. Enderton's Mathematical Logic. It certainly confused me, but I'm fine now. HOL and a ZC/FOL proof assistant both construct syntactic proofs. We need semantics in order for these syntactic proofs to "mean" anything. To prove theorems about actual sets, we take a semantic function like M of the Logic manual and apply it to our HOL syntactic proofs. But we're not required to use the semantic function M of the Logic manual. If we come up with a different semantic function, that's fine too. The theorems that HOL proves for us will then have a (very slightly I'm bet) different meaning. An important things I think missing from your analogy (or comparison), though, is the definition of types and constants. I don't understand the question. You know more than I do about types & constants in HOL than I do, and I think these don't exist in FOL. I tried to explain that much of the ZC/FOL axioms (power set, products...) are encoded in the HOL type system (->, prod/#). The property of product types you wrote above is guaranteed by the definition of product types. It is not part of the logical foundation, but rather is carefully ensured by JRH or whoever wrote the theory of pairs as definitions of new types and constants above the basic logical foundation. Ah, so I wouldn't have found it in the Logic manual. Thanks. Can you tell me where HOL4 defines the product type `prod'? John certainly explains how to use his product type # and pairs. > but HOL could easily be explained without this cool typed LC. Certainly you don't have to mention "lambda calculus", but you're going to have to describe something isomorphic to it in explaining what the terms of your proof system are. No, LC is a deep theory which e.g. explains how to define the logical operators and, not, forall, exists, implies etc, which Enderton would take to be fundamental notions. One kind of term is a lambda abstraction, which use the symbol lambda (λ or \). But that's not a serious use of LC. -- Best, Bill ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
