On Tue, Sep 4, 2012 at 5:54 AM, Bill Richter
<[email protected]>wrote:
> 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/#).
>
Constants do exist in FOL: they are called function/relation and predicate
symbols. In ZC/FOL you have constants like set-membership and equality
(both relations). But you can be more or less formal about how you define
new constants. In HOL, since we actually define things like the logical
connectives and quantifiers (and,or,not,forall,etc.) rather than having
them built into the syntax, we have principles of definition.
>
> 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.
>
In HOL4 it's src/pair/src/pairScript.sml
In HOL Light it's pair.ml.
Logically, the definition of the product type in both systems is the same:
do you understand what prod_tybij is doing in the HOL Light pair.ml script?
>
> > 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
