Andrew,
On 21 Mar 2014, at 09:13, Andrew Butterfield <andrew.butterfi...@scss.tcd.ie>
wrote:
>
> 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?
>
Yes. I should have given this link:
http://hol.sourceforge.net/documentation.html.
> 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?
Yes. In this description, the universe U provides the possible semantic values
for types and types in this logic are not allowed to denote empty sets.
That said, I don’t think that Pow actually plays any role other than to
show that function spaces exist (property Fun). So as the function space
X -> Y is not empty if Y is not empty, it doesn’t really matter
whether Pow contains the empty set or not.
Regards,
Rob.
------------------------------------------------------------------------------
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
