Email Gateway (Aug 22 2022 at 12:05): Email Gateway (Aug 22 2022 at 12:05):From: Ken Kubota <mail@kenkubota.de>
Dear Gottfried Barrow,
There has been a misunderstanding. I claimed neither that Isabelle is
inconsistent nor the contrary.
However, a proof of Paulson's claimed theorem 'proved_iff_proved_PfP' is not
available in axiomatic (Hilbert-style) deductive systems, because in
Hilbert-style systems this claimed theorem cannot even be expressed, since it
does not contain well-formed formulae only. Therefore this claimed theorem is
not a mathematical theorem or metatheorem. For now, please allow me to focus on
this single point.
This can be demonstrated easily by looking at the structure of the claimed
theorem 'proved_iff_proved_PfP' available at
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 21)
http://www.owlofminerva.net/files/Goedel_I_Extended.pdf (p. 19)
which can be written
{} > a <-> {} > PfP "a"
if we use '>' for the deduction symbol (turnstile) and '"' for the Goedel
encoding quotes, and simplified without change of meaning to
> a <-> > PfP "a"
expressing that 'a' is a theorem if and only if there is a proof of 'a'.
Now, recalling the quotes by Alonzo Church and Peter B. Andrews available at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00018.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00042.html
in an axiomatic (Hilbert-style) deductive system, the claimed theorem
'proved_iff_proved_PfP' could be either a theorem (a theorem of the object
language) or a metatheorem (a theorem of the mathematical meta-language).
Case 1 (theorem of the object language, language level 1):
As a trivial example for a theorem of the object language, we shall use
(T & T) = T
usually written
> (T & T) = T
as presented in [Andrews, 2002, p. 220 (5211)], with the preceding deduction
symbol (turnstile) in order to express that '(T & T) = T' is a theorem.
In this notation it has, like all theorems of the object language of Q0,
exactly one occurrence of the deduction symbol (turnstile).
Hence, the claimed theorem 'proved_iff_proved_PfP', having two occurrences,
cannot be a theorem of the object language.
Case 2 (theorem of the meta-language, language level 2):
As a trivial example for a theorem of the meta-language, we shall use
If H > A and H > A => B, then H > B.
presented in [Andrews, 2002, p. 224 (5224 = Modus Ponens)], expressing that if
there is a proof of A (from the set of hypotheses H) and a proof of A => B
(from H), then there is a proof of B (from H).
Note that this example shows some of the typical formal criteria of a
metatheorem:
Use of syntactical variables (denoted by bold letters in the works of both
Church and Andrews).
Use of the informal words "If" and "then" instead of logical symbols in the
meta-language (according to Church's proposal).
It should be emphasized that metatheorems in proofs can always be replaced by
the proof of the concrete theorems (the syntactical or schematic variable
instantiated) when carrying out the proof, such that metatheorems are actually
not necessary (but reveal properties of the object language that help finding
proofs).
In the notation of Isabelle (natural deduction) this metatheorem would be
expressed by
[H > A; H > A => B] --> H > B
and, if we would add subscripts for the language levels, by
[H >1 A; H >1 A => B] -->2 H >1 B
So metatheorems infer from theorems of the object language (language level 1)
to another theorem of the object language, and this relation between theorems
of the object language is expressed at a higher level: the meta-language
(language level 2).
But the claimed theorem 'proved_iff_proved_PfP'
> a <-> > PfP "a"
cannot be a metatheorem either, since both ways of dealing with it, either
semantically (subcase a) or syntactically (subcase b), fail.
Case 2 Subcase a (semantically):
In the claimed theorem 'proved_iff_proved_PfP'
> a <-> > PfP "a"
the right-hand side (PfP "a"), expressing the provability of theorem 'a', is,
by its meaning, itself a metatheorem, not a theorem of the object language, and
we would have some kind of meta-metatheorem like
>1 a <->3 >2 PfP "a"
If we ignore the fact that his meta-metatheorem violates the language level
restrictions and nevertheless proceed further, then from a theorem of the
object language a theorem of the meta-language could be inferred and vice
versa, which would again violate language level restrictions, as for example a
metatheorem would be added to the list of theorems of the object language and
treated as such, leading to a confusion of language levels.
This is, in principle, the construction of the proofs of Andrews and Rautenberg
[cf. Kubota, 2013], in which 'proved_iff_proved_PfP' is used as an implicit
rule, not as a proven theorem/metatheorem. Of course, they both fail also
simply by not providing a proof using syntactical means only.
Case 2 Subcase b (syntactically):
In Paulson's claimed theorem 'proved_iff_proved_PfP'
> a <-> > PfP "a"
the right-hand side (PfP "a") needs to be a well-formed formula.
But the Goedel encoding in Paulson's proof is implemented by the use of means
which are not available in the object language (i.e., in mathematics).
According to Paulson at
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 16)
"[i]t is essential to remember that Gödel encodings are terms (having type tm),
not sets or numbers. [...] First, we must define codes for de Bruijn terms and
formulas.
function quot_dbtm :: "dbtm -> tm"
where
"quot_dbtm DBZero = Zero"
[...]"
Paulson's definition goes beyond the use of purely mathematical means. After
the introduction of the definition of quot_dbtm, it is used as follows:
"We finally obtain facts such as the following:
lemma quot_Zero: "'Zero' = Zero"
[...]"
But with its purely syntactical means the object language cannot explicitly
reason about its own properties directly.
Propositions in Andrews' logic Q0 have type 'o' (Boolean truth values), and one
could define a function 'foo': o -> o, o -> i, or o -> nat (with nat = (o(oi))
= (i -> o) -> o; natural numbers as "equivalence classes of sets of
individuals" [Andrews, 2002, p. 260]), etc.
But since a type "tm" (for term) does not exist in Q0 [cf. Andrews, 2002, p.
210] or R0, one cannot define a mathematical function 'quot_dbtm': dbtm -> tm.
Of course, there are rules for construing well-formed formulae (wffs), but
these (in R0 hardcoded) rules are used implicitly for construing wffs and are
not part (are not theorems) of the object language itself.
Explicit meta-reasoning as with lemma 'quot_Zero' might extend (and, hence,
violate) the object language, as it actually introduces new rules of inference
to the object language, which again may be considered as a confusion of
language levels.
Type "tm" (for term) is a notion of the (technical) meta-language, but not a
mathematical type. Therefore the function 'quot_dbtm' (type: dbtm -> tm) is not
a mathematical well-formed formula (wff), subsequently the Goedel encoding
function ('" "') and the Goedel encoding of proposition 'a' ('"a"') are not
either, and hence the right-hand side (PfP "a") is not a wff and therefore not
a proposition. Finally,
PfP "a"
or
> PfP "a"
cannot be a theorem, and for this reason the claimed theorem
'proved_iff_proved_PfP'
> a <-> > PfP "a"
cannot be a metatheorem.
Obviously the (technical) meta-language and the object language in Isabelle are
not strictly separated, since the type "tm" (for term) is treated as a
mathematical type in the construction of wffs of the object language, which is
not mathematically safe. Mathematically, a proposition has only type 'o'
(Boolean truth values), but not a type "tm" (for term).
All definitions of Q0 are only shorthands for established wffs. In my R0
implementation, a definition label added to a wff is used for input (parsing)
and output (display) only, and remains irrelevant for syntactical inference and
can be removed or replaced at any time. This means that a definition label for
Goedel encodings (in this case the quotation marks) must represent a
mathematical well-formed formula (wff) when used in 'proved_iff_proved_PfP',
which may be a function with a mathematical type as input (domain) type such as
the type of truth values (type: o -> *), but not with types of the
meta-language as input (domain) type (type: dbtm -> *, or tm -> *), as this
violates the rules for construing mathematical wffs [cf. Andrews, 2002, p. 211].
Of course, one could introduce Goedel numbering in order to arithmetize the
object language and reason about the Goedel numbers. But the reasoning would
then be restricted to these Goedel numbers, and there would be no possibility
to relate these Goedel numbers directly to theorems of the object language as
done in the claimed theorem 'proved_iff_proved_PfP'
> a <-> > PfP "a"
since the Goedel encodings in Paulson's proof (requiring a type "tm") are not
definable with purely mathematical means of the object language (e.g., in R0).
Since the proposition 'a' has only type 'o' (Boolean truth values), the logical
arithmetic is not stronger than propositional calculus, ruling out Goedel
encodings requiring a type "tm".
The concept of the Goedel encoding function generally violates the type
restrictions for construing mathematical wffs, as with the type of truth values
as input (domain) type there would be only two different Goedel numbers.
As in other claimed proofs, non-mathematical means are used in order to
establish a relation between the object language (proposition 'a') and the
meta-language (its provability: PfP "a") as the translation mechanism between
both language levels necessary for the self-reference part of the antinomy,
since Goedel's antinomy is construed across language levels. Note that the
antinomy seems to c
[message truncated]
Email Gateway (Aug 22 2022 at 12:05):From: Andrei Popescu <a.popescu@mdx.ac.uk>
Dear Ken,
Please forgive me if my tone may seem condescending. I am not an expert in Goedel's theorems, but I have a lot of experience with Isabelle and I have looked at the incriminated proofs.
First, please let me assure you of the following, concerning Larry’s proofs: The employed concepts and the proved theorems do not suffer from any consequence of Isabelle/HOL being based on a meta-logic or featuring a natural deduction system. These concepts and theorems are easily reproducible in "pure" systems, lacking a logical framework on top of them – including all the HOL and ZF systems, be they based on natural deduction, sequent calculi or Hilbert systems. Any person having experience with logical frameworks and with Isabelle would give you this assurance after superficially inspecting these proofs. The logical framework merely offers some convenience.
Now, I say let’s not be dogmatic about how Goedel’s Second has been proved. The fact that Larry and authors before him took some shortcuts, working at an outer level for as much as possible, is perfectly legitimate. It forms the beauty of taming a proof of huge complexity. Again, I ensure you that there is nothing exotic with the employed primitives that led to the stated theorem. In my opinion, the only question worth asking is if the end statement is truthful:
theorem Goedel II:
assumes "¬ {} ⊢ Fls"
shows "¬ {} ⊢ Neg (PfP ⌈Fls⌉)"
I hope we agree that the conclusion of the theorem (the "shows" part above) should be "¬ {} ⊢ Neg phi" where phi is a formula that captures the notion "False is provable in the first-order logic of HF," as represented in the language of HF itself. Here, one may argue that taking phi to be "PfP ⌈Fls⌉" is not a priori convincing, especially since the definitions leading to PfP are very technical and are spanning two levels. These aspects could be clarified by unfolding the definitions and performing some simplifications that "reify" this term. But I am not sure: Is this what you are arguing?
With best wishes,
Andrei
Email Gateway (Aug 22 2022 at 12:05):From: Ramana Kumar <rk436@cam.ac.uk>
Hi Ken,
There are a few points in your email where I believe what you are saying is
simply mistaken. I have pointed a couple of them out below.
On 22 December 2015 at 20:03, Ken Kubota <mail@kenkubota.de> wrote:
In the claimed theorem 'proved_iff_proved_PfP'
> a <-> > PfP "a"the right-hand side (PfP "a"), expressing the provability of theorem 'a',
is,
by its meaning, itself a metatheorem, not a theorem of the object language,
That is incorrect. (PfP "a") is an object-language statement. I think you
may have been confused by what it represents. Indeed, the only reason you
want to claim it is a metatheorem is because of "its meaning". But if you
simply ignore its meaning, it is clearly and syntactically an object-level
statement.
If you disagree, I press you to argue your point further and concentrate
only on this example until we can clear up the disagreement about this
point.
Propositions in Andrews' logic Q0 have type 'o' (Boolean truth values),
and one
could define a function 'foo': o -> o, o -> i, or o -> nat (with nat =
(o(oi))
= (i -> o) -> o; natural numbers as "equivalence classes of sets of
individuals" [Andrews, 2002, p. 260]), etc.
But since a type "tm" (for term) does not exist in Q0 [cf. Andrews, 2002,
p.
210] or R0, one cannot define a mathematical function 'quot_dbtm': dbtm ->
tm.
The type "tm" is not a primitive type, but it can be defined, just as you
defined "nat" above. Paulson defined the type before using it. It is
incorrect to say that the type "tm" does not exist in Q0, if we allow Q0
type definitions.
Email Gateway (Aug 22 2022 at 12:05):From: Gottfried Barrow <igbi@gmx.com>
Ken,
I email this to you also, to try and be civilized, but you shouldn't
email me back. I'm happy to let Popescu and Kumar finish it all.
But you did address this to me. I stated my rules, but rules require the
use of discretion, or being ignored and broken.
If you don't diss the team on the team's turf, in a way that makes me
feel I should defend the team, and you don't address emails to me,
there's no reason for me to keep showing up.
To try and add some concrete value, I include a base 10 datatype that's
bijective with 'nat':
https://gist.github.com/GezzMC/125ce3352966ec7f7e6c
I did that based on Num.thy, by Florian Haftmann and Brian Huffman. For
the proofs, I brute forced them with a combination of 'auto', 'induct',
and Sledgehammer. I've never before or since been willing to wait so
long on Sledgehammer.
I suppose I should tie that into this thread.
I think I'm starting to remember its purpose for here.
We can consider any person an archetype of some class of people. An
archetype at hand is Larry Paulson, and you're another archetype. To
call myself an archetype, that would mean I'm (willing to admit I'm)
full of myself.
NO FANBOY, NO LOYALTY
In this thread of emails (made up of multiple subject lines), Larry
Paulson is getting mentioned a lot, and I'm defending him.
I could say, "And obviously, Larry Paulson doesn't need me to defend
him". It's not the need. I think it's the value of someone knowing that
their stuff is getting used.
The gist link also shows that something is being looked at and used.
However, it also reflects that Isabelle/HOL isn't some perfect work
where I'm saying, "I have a testimony for the world. Isabelle? Pure
bliss, all the time, 24/7."
Where's the base 10 type? Where are the vectors? And don't tell me to
look outside of 'Complex_Main'.
Criticism? Absolutely, to show I'm no fanboy, but in the end, it happens
to be that Isabelle/HOL is good, as far as I can tell.
ISABELLE/HOL: HAVE YOU, KEN, AND JAMES MEYER EVEN USED IT?
This falls under the "if you're so smart" category.
I've always considered that I would need a better understanding of logic
to work at the "meta-logic" or "metalanguage" level. Briefly here, you
challenge the top dogs at the meta-logic level, but nothing I've seen
indicates that you have any decent ability to use Isabelle/HOL.
Shouldn't a smart person be able to blow through the easy stuff?
Previously, I kept James Meyer out of this, who was in your first
address list. In reviewing your emails, I paid more attention to your
reference to him, particularly to his remark about Paulson. Based on
that, I then looked at Meyer's PDF on his site. Keep that in mind.
MISUNDERSTANDING? NO, NON-VERBOSENESS
You say this time:
Email Gateway (Aug 22 2022 at 12:05):From: Gottfried Barrow <igbi@gmx.com>
Greetings,
There's a very narrow purpose to this email. I accomplish that purpose
by what I say in the first few sentences, which is not intended to
create any debate.
Picking a nice number, 50, I'll say that at least 50% of what I've said
in the past, on technical matters, has been wrong. But taking a position
can be the first step in working out ideas, though one person working
out an idea can be everybody else getting spammed.
While not technically wrong, since close enough can be good enough,
"monolithic logic" wasn't the right choice. A better choice would "black
box logic". It's based on a hardware perspective, which I believe is the
correct "ultimate view of things" for mechanized proofs. Hex was my
friend when looking at address and data buses with a logic analyzer.
There's Wikipedia, even when no one needs it:
https://en.wikipedia.org/wiki/Black_box
Related to my "minimal black box interpretation", for an overall view,
is my "minimal syntactic interpretation", for logic as strings of
characters. For things like this:
term "THE x. x \<in> {}" (Do not think beyond the string.)
lemma "EX! y. y = (THE x. x \<in> {})" (*Totalitarianism. HOL is a
tyrant.*)
by(rule HOL.ex1_eq(1))
Asking no one in particular, I ask and say, "Do you know how annoying it
is to read Isabelle list emails on the web archive? Graphical symbols,
for \<Rightarrow> and \<Longrightarrow>, get converted to funny looking
'a' symbols."
There is always this open question for me: Do I know enough to do a
major disconnect? Being connected can result in more sophistication, but
there also should be a fixed foundation. People have been working off of
ZFC, for how many years?
Here's a polymorphic vector:
datatype ('a,'size) vD = vC (vG: "'a list")
The problem of length reflects the general problem of HOL functions
being total, and that domains aren't easily restricted, by defining new
types. What I have in mind is fixing the problem, in general, by working
in null space, which will get lifted to option space. You heard it here
first.
The sophistication comes from its use with 'CARD(n)', thanks to a
pointer by Manuel Eberl.
I do pull from 'src/HOL/Library', but I stick it all in one file. 'CARD'
is thanks to 'Phantom_Type' by Andreas Lochbihler, 'Cardinality' by
Brian Huffman & Andreas Lochbihler, and 'Numeral_Type' by Brian Huffman.
Lars Noschinski deserves thanks for some other things.
With the new datatype, thanks to Blanchette and Traytel, and whoever
else I'm missing, I guess Popescu, there are so many possibilities they
become uninteresting, due to the shear number of them.
The 'datatype' keyword itself encapsulates what can be a beautiful form
of math, a statement so devoid of detail, it's hard to get the meaning.
The vector is above. Here, possibly, are nested countable and nested
finite sets:
datatype 'a csetD = Atom 'a | csetC "'a csetD cset"
datatype 'a fsetD = Atom 'a | fsetC "'a fsetD fset"
Here is a possible generalization of nested multisets (using lists):
datatype 'a msetD = Atom "'a * nat" | msetD "'a msetD list"
Here is what I'm really interested in. Nested sum sets and factor sets
combined:
datatype 'a sumfacD = Atom 'a | sumC "'a sumfacD list" | facC "'a
sumfacD list"
It uses lists, but why use sets when I can use lists with an equivalence
relation, which may lead back to using sets. I don't care about sets
anymore, unless I need to. I care about lists, to be used as finite sets.
What's it all worth? Nothing much in an email. The definitions might
need to be tweaked, and the devil is in the details.
Consider a quote from Carl Friedrich Gauss:
I confess that Fermat's Theorem as an isolated proposition has very
little interest for me, because I could
easily lay down a multitude of such propositions, which one could
neither prove nor dispose of.
http://www-groups.dcs.st-and.ac.uk/history/Quotations/Gauss.html
Finishing up unfinished business while the gettin' is good, to put it in
amongst a collective gettin'.
Regards,
GB
Last updated: Nov 21 2024 at 12:39 UTC