John, it sounds like you solved my locales problem:
you can just define a constant "TarskiModel" to indicate that two
arbitrary predicates "===" and "Between" satisfy the axioms,
something like this
TarskiModel((===),Between) <=>
(!a b. a,b === b,a) /\
....
(!a b p q z.
Between(a,p,z) /\ Between(b,q,z)
==> ?x. Between(p,x,b) /\ Between(q,x,a))
Then every theorem would become |- TarskiModel((===),Between) ==> P
instead of just |- P. If I understand your Mizar code correctly, this
pretty much matches what you are doing there.
That sounds perfect! I can see why Tom Hales wanted to work with
you! Uh, I don't even know what a constant is.
That's fabulous that we can change the automation. For now let's go
with Freek's. I'll try to read Piotr Rudnicki's paper.
The first thing I did with your Mizar code was to remove them.
Wow, you were really working, I feel guilty. The file joe.miz has the
fancy character turned into Mizar, for, ex, st, implies, etc.
| It sure makes the code more readable.
That's a matter of opinion.
It's definitely my opinion, and I know when I came to it. I was
staring at my proof of Gupta's theorem and I said to myself, I can't
read this, I have no idea what I'm writing. After I wrote my Emacs
code and stuck in (the top-level bits?) ⇒, ¬, ∨, ∧, ≡, ∀, ∃ and ⇔, it
was so much more readable. That's the way mathematicians actually
write, of course, so it's hard for me to read anything else.
I would discourage it and advise you to set up some additional
interface layer.
I'll do it your way, you're the expert. What do you mean? Something
like my Emacs stunt to rewrite the file before compiling it? Is there
a clean way to do that? I wasn't too happy with my solution.
I think you're saying that your earlier comment is true for me:
| I suppose that most geometric problems are purely universally
| quantified so the extra structuring steps are not as important.
That's good I'm in the shallow end of the pool. I like this:
This reminds me of something Andrzej Trybulec said about automated
theorem provers: why should we let the machine deprive us of the
pleasure of proving things?
That's great, and I modified Andrzej Mizar code to write mine. , We
should use the machine to enhance the pleasure of proving things. I
get a great rush when Mizar says I have a correct proof. There's a
democracy/PoMo angle: I haven't yet talked to a grownup about Tarksi
axiom proofs, and I completely believe my proofs, because Mizar
checked them. I don't need to be part of a system that tells me I'm
right. And there's no Post Modernist talk about how proofs are social
constructs, it's up to every community to decide what a proof is.
The middle school math coordinator where I live told me to read an
article by an education prof Stylianides
The Notion of Proof in the Context of Elementary School Mathematics
who claimed that a 3rd grade girl Betsy failed to give a proof that
odd + odd = even, on the grounds that the other 3rd graders didn't buy
her proof. Betsy's proof was fine, and the objections were silly (you
can't even say all the numbers!). If Betsy has a` good proof
assistant to code her proof in, these PoMo objections disappear.
--
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
