Bill:
> On p 29 of LOGIC, you write that there are constants
> Tbool, ∀(α→bool)→bool etc. Why aren't there colons? I would have
written that as
> T:bool and ∀:(α→bool)→bool
> Are the apparent subscripts supposed to indicate colons, or does HOL4 not
use colons for type annotations?
Throughout the LOGIC document, subscripts are supposed to indicate colons.
See the comment on p. 15.
> I'm having trouble seeing your derivation of the expected FOL-like rules
in HOL Light. Is there a paper where somebody
> explained these HOL derivations, or is it perhaps easier to understand in
HOL4?
This was done in the early days of HOL. In Chapter 22.3 of "Introduction to
HOL", by Gordon and
Melham, the standard rules are derived, and a fascinating business it is.
In HOL4, the file src/bool/boolScript.sml is largely made up of such
derivations. Here's an
example:
(*
-------------------------------------------------------------------------*)
(* NOT_FORALL_THM = |- !P. ~(!x. P x) = ?x. ~P x *)
(*
-------------------------------------------------------------------------*)
val NOT_FORALL_THM =
let val f = ``P:'a->bool``
val x = ``x:'a``
val t = mk_comb(f,x)
val all = mk_forall(x,t)
and exists = mk_exists(x,mk_neg t)
val nott = ASSUME (mk_neg t)
val th1 = DISCH all (MP nott (SPEC x (ASSUME all)))
val imp1 = DISCH exists (CHOOSE (x, ASSUME exists) (NOT_INTRO th1))
val th2 =
CCONTR t (MP (ASSUME(mk_neg exists)) (EXISTS(exists,x)nott))
val th3 = CCONTR exists (MP (ASSUME (mk_neg all)) (GEN x th2))
val imp2 = DISCH (mk_neg all) th3
in
GEN f (IMP_ANTISYM_RULE imp2 imp1)
end;
Konrad.
On Fri, Mar 21, 2014 at 1:18 AM, Bill Richter <rich...@math.northwestern.edu
> wrote:
> Thanks, Konrad! You seem to agree with me here, that the
> typed-LC-implies-FOL isn't actually important:
>
> My personal feelings on this foundational aspect are that the
> actual set of axioms isn't that important provided the usual
> introduction and elimination rules of predicate calculus can be
> derived from them.
>
> Now you're encouraging me to go read Church's typed LC paper more
> carefully, and see if I can work out the apparent difference between Church
> and what I quoted Andrews as saying about Church:
>
> My recollection (don't have citations to hand) is that Church
> originally wanted the untyped lambda calculus to serve as a
> foundation for logic, but that was discovered to be
> inconsistent. Something like Russell's paradox would be easy to
> code up in it. However, the simply typed lambda calculus worked
> better, i.e., it supports the derivation of the expected FOL-like
> rules, as we see in HOL theorem provers, and it is sound.
>
> Here's a some dumb questions about HOL4 and HOL Light.
>
> On p 29 of LOGIC, you write that there are constants
> Tbool, ∀(α→bool)→bool etc. Why aren't there colons? I would have written
> that as
> T:bool and ∀:(α→bool)→bool
> Are the apparent subscripts supposed to indicate colons, or does HOL4 not
> use colons for type annotations?
>
> I'm having trouble seeing your derivation of the expected FOL-like rules
> in HOL Light. Is there a paper where somebody explained these HOL
> derivations, or is it perhaps easier to understand in HOL4?
>
> Tom Hales writes on p 6 of
> http://www.ams.org/notices/200811/tx081101370p.pdf
>
> The system [HOL Light] has only two primitive constants. One of them is
> the equality symbol (=) of type :A->A->bool. So = is primitive, and p 5
> lists the HOL Light axioms about the properties of =. Let's try to find
> this in the HOL Light sources. In
> hol_light/bool.ml
> it seems to me that first the type bool is defined,
> then = and <=> are defined to have type bool->bool->bool and to be the
> same as each other,
> then T is defined as
>
> let T_DEF = new_basic_definition
> `T = ((\p:bool. p) = (\p:bool. p))`;;
>
> That's your first HOL axiom on p 29 (again without colons):
>
> T = ((λxbool . x) = (λxbool . x))
>
> So it looks to me that HOL Light is defining Tom's primitive = in terms of
> the Ocaml =. Is that correct? And maybe that just means that the HOL
> Light primitive = is "represented" in Ocaml as the ordinary =?
>
> --
> Best,
> Bill
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
