16 views

Skip to first unread message

Sep 20, 2014, 9:08:03 PM9/20/14

to ghil...@googlegroups.com

Hi all:

Some years ago Raph and I had a few exchanges on the AsteroidMeta wiki about "hcode" and its potential relationship to Ghilbert. At the time, hcode was more or less vaporware -- but I think it is starting to distill into something. I now have some time to think about this more, I'm wondering whether it's reasonably possible to compile from hcode to Ghilbert. A developing spec is here: http://metameso.org/~joe/math/hcode.pdf

I'm encouraged by noticing some recent additions to the Metamath repository that are very recognizable as the kind of thing I might want to prove. http://de.metamath.org/mpeuni/cncfss.html is one example.

Here, below, is a sketch of a proof represented in hcode. Could we translate this to Ghilbert? Please keep in mind that at the moment hcode is just a representation language: it doesn't "do" anything. I've spelled out some inferences in comments that would have to be made explicit in a more formal system and I don't know how much, if any, could be picked up from context. I'm not attached to any such "magic".

Many of your examples look "close" -- though I don't know why you've dropped the outer parentheses on your s-exps. Maybe hcode could be understood to be syntactic sugar over Ghilbert. I have many addition definitions and theorems, and all-too-few proofs written down. I'd like to be able to just sit and "transcribe" mathematical texts into a format like what follows, and much better if it actually runs somehow.

I'll start off with a simple example, if the prospects here are looking good I'll follow up with something more complicated next.

Cheers,

Joe

(defn topological-space (X T)

(set X)

;; T is a set of subsets of X

(subset T (setof Y :st (subset Y X)))

(elt empty-set T)

(elt X T)

;; closed under finite intersections

(forall V :st (if (countable-subset V T)

(elt (intersection (setof v :st (elt v V)))

T)))

;; closed under unions

(forall W :st (if (subset W T)

(elt (union (setof w :st (elt w W)))

T))))

(defthm elements-in-open-subsets-means-set-is-open

(X T A)

(topological-space X T)

(subset A X)

(forall a :in A :st (exists B :in T

:st (and (elt a B)

(subset B A))))

(elt A T))

(defproof

PR:elements-in-open-subsets-means-set-is-open (X T A)

;; we can make use of the main assumption

(forall a :in A

(bind (sub B a)

(some B :in T

:st (and (elt a B)

(subset (sub B a) A)))))

;; per `topological-space' closure under unions,

;; the union of our chosen open sets is open

(implies (forall W :st (if (subset W T)

(elt (union (setof w :st (elt w W)))

T)))

(elt (union (setof (sub B a))) T)) ; [i]

;; the union of subsets is a subset

(implies (subset (sub B a) A)

(subset (union (setof (sub B a))) A))

;; And if each element of a set is contained in

;; an element of a cover, the set is contained

;; in the union of covering sets

(implies (forall a :in A (exists (sub B a)

:st (elt a (sub B a))))

(subset A (union (setof (sub B a)))))

;; So we have containment in both directions and

;; can conclude:

(eq A (union (setof (sub B a)))) ; [ii]

;; and [i] showed that this union is in T

;; so this concludes the proof

)

Some years ago Raph and I had a few exchanges on the AsteroidMeta wiki about "hcode" and its potential relationship to Ghilbert. At the time, hcode was more or less vaporware -- but I think it is starting to distill into something. I now have some time to think about this more, I'm wondering whether it's reasonably possible to compile from hcode to Ghilbert. A developing spec is here: http://metameso.org/~joe/math/hcode.pdf

I'm encouraged by noticing some recent additions to the Metamath repository that are very recognizable as the kind of thing I might want to prove. http://de.metamath.org/mpeuni/cncfss.html is one example.

Here, below, is a sketch of a proof represented in hcode. Could we translate this to Ghilbert? Please keep in mind that at the moment hcode is just a representation language: it doesn't "do" anything. I've spelled out some inferences in comments that would have to be made explicit in a more formal system and I don't know how much, if any, could be picked up from context. I'm not attached to any such "magic".

Many of your examples look "close" -- though I don't know why you've dropped the outer parentheses on your s-exps. Maybe hcode could be understood to be syntactic sugar over Ghilbert. I have many addition definitions and theorems, and all-too-few proofs written down. I'd like to be able to just sit and "transcribe" mathematical texts into a format like what follows, and much better if it actually runs somehow.

I'll start off with a simple example, if the prospects here are looking good I'll follow up with something more complicated next.

Cheers,

Joe

(defn topological-space (X T)

(set X)

;; T is a set of subsets of X

(subset T (setof Y :st (subset Y X)))

(elt empty-set T)

(elt X T)

;; closed under finite intersections

(forall V :st (if (countable-subset V T)

(elt (intersection (setof v :st (elt v V)))

T)))

;; closed under unions

(forall W :st (if (subset W T)

(elt (union (setof w :st (elt w W)))

T))))

(defthm elements-in-open-subsets-means-set-is-open

(X T A)

(topological-space X T)

(subset A X)

(forall a :in A :st (exists B :in T

:st (and (elt a B)

(subset B A))))

(elt A T))

(defproof

PR:elements-in-open-subsets-means-set-is-open (X T A)

;; we can make use of the main assumption

(forall a :in A

(bind (sub B a)

(some B :in T

:st (and (elt a B)

(subset (sub B a) A)))))

;; per `topological-space' closure under unions,

;; the union of our chosen open sets is open

(implies (forall W :st (if (subset W T)

(elt (union (setof w :st (elt w W)))

T)))

(elt (union (setof (sub B a))) T)) ; [i]

;; the union of subsets is a subset

(implies (subset (sub B a) A)

(subset (union (setof (sub B a))) A))

;; And if each element of a set is contained in

;; an element of a cover, the set is contained

;; in the union of covering sets

(implies (forall a :in A (exists (sub B a)

:st (elt a (sub B a))))

(subset A (union (setof (sub B a)))))

;; So we have containment in both directions and

;; can conclude:

(eq A (union (setof (sub B a)))) ; [ii]

;; and [i] showed that this union is in T

;; so this concludes the proof

)

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu