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 vice versa.

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 MHonArc.