Email Gateway (Aug 18 2022 at 20:33): Email Gateway (Aug 18 2022 at 20:33):From: Gottfried Barrow <gottfried.barrow@gmx.com>
By asking questions here, it makes me think harder and work harder, to
try and keep from saying something that's wrong.
First, one of the biggest things I got out of this is the idea of
running Nitpick on both a theorem and it's negation. I'm thinking that
if both a "theorem" and its negation are both false, then that's a
problem. I'd still like to ask that question, "Uh, if Nitpick finds a
counterexample, does that mean..." Negative logic can mess me up.
"Inconsistent" isn't part of the vocabulary of a typical math education.
I have to deprogram myself.
I have just now had a revelation. If I can run Nitpick on a theorem and
its negation, then I can run Sledgehammer on a theorem and its negation.
I'll need to write some macros so I don't spend my life cutting,
pasting, and typing, and eventually get that quad core notebook. I see
that dummy_thf prover again. It never proves a thing.
My more-flexible solution is to not use the HOL "=", but use my own
undefined "EQ", like this:
consts eqS::"[sT,sT] => bool" (infixl "EQ" 51)
Of course, I still want to make it easy to experiment, and switch in and
out the HOL "=", so I comment out eqS, and use:
abbreviation eqS::"[sT,sT] => bool" (infixl "EQ" 51) where "x EQ y == x = y"
My constant eqS is more conceptually satisfying because it doesn't make
any sense to use it if it hasn't been defined in any way. If I use it
without defining it, I end up with that same inconsistency that I get
when I use the HOL "=", but the HOL "=" is defined, though it still
might not make sense to use it the way I was using it.
I also get an <-> that's not identical to my equal operator. As to how
easy or hard it makes things to prove, I don't anything about that yet.
Regards,
GB
Last updated: Nov 21 2024 at 12:39 UTC