Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem
On 7/20/2012 9:34 AM, Makarius wrote:
On Fri, 20 Jul 2012, Gottfried Barrow wrote:
Quantifying over functions has me a little worried.
Why? Semantically a function is just a set, and in mathematics you
qantify over collections of sets all the time.
Because I read things that I don't completely understand that make me
worry, such as that certain things can be proved about FOL that can't be
proved about HOL. Was that "completeness" that I read about? I don't
even look it up.
Until recently, I made my money as a technician working in telecom. I've
seen it over and over again. The best educated and hardest working
engineers don't typically make fundamental mistakes, because they
understand the fundamentals. Those with an inferior education, even if
they work hard, make fundamental mistakes that doom their designs.
You understand foundations all the way to the bottom. I try to
understand what I don't understand to not be the guy who makes the most
fundamental of mistakes. A healthy amount of worry keeps me on my toes.
You can take HOL is a simplified version of FOL + set theory, but with
an explicit type system. Paradoxically HOL is weaker that FOL + ZF set
theory, despite arbitrary abstraction and quantification in HOL.
Here, I don't even know what "weaker" means because I've found no
standard definition anywhere for "logically weaker".
However, I've found enough information to assume that it means that
everything you can prove with HOL can be proved with FOL+ZF, but not
Immediately, I ask the question, "How can what each logic proves be
compared? They're two different logics, with two different sets of
primitive symbols, with two different rules for combining the symbols".
I answer my question and say, "Ah, those logicians, they must have
formalized the study of translating statements from one logic into another."
> Anyway, in practice you don't need to worry about the foundations and
> their relative logical strenth.
Well, I think you're projecting your understanding of foundations onto
me. You see clearly to the bottom. I see through a glass darkly.
You just do your applications with
high-level specification mechanims in Isabelle (datatype, function,
inductive, locale etc.), better not axiomatization.
And so I'll make the switch as soon as possible, and either redo
everything based on some sort of definition, or I'll maintain two
different versions. I'm jumping to conclusions here about me being able
to achieve overall success with my current idea.
This archive was generated by a fusion of
Pipermail (Mailman edition) and