On 20 Mar 2014, at 16:50, Rob Arthan <r...@lemma-one.com> wrote:
>
> ProofPower is no different from HOL4 and HOL Light as regards substitution.
> The ProofPower documentation does include a formal specification of the logic
> and the proof system, but you would probably do better looking at the HOL4
> Logic Manual, which gives a good account based on work of Andy Pitts that
> uses traditional maths notation to define the logic including substitution.
> The primitive rules and axioms in HOL4 (and ProofPower) are different from
> HOL Light, but prove the same set of theorems.
Is this the document kanananaskis-9-logic.pdf?
If it is, I have a query: in Sec 1.1 Introduction (p9) we are shown some
properties
One is *Inhab* : U does not contain empty sets - fair enough
Another is *Pow* which says that if X is in U, then so is P(X) = { Y : Y
subseteq X }
To me this implies that P(X) may (will) contain the empty set as an element.
Is this a correct interpretation of the consequences of these rules?
Regards,
Andrew Butterfield
PS - I think a comment about this should occur on that page or the next…
--------------------------------------------------------------------
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
Director of Teaching and Learning - Undergraduate,
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------
------------------------------------------------------------------------------
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
