Email Gateway (Aug 22 2022 at 13:44): Email Gateway (Aug 22 2022 at 13:44):From: Ken Kubota <mail@kenkubota.de>
Dear Andrei Popescu, dear Ramana Kumar,
dear Members of the Research Community,
As a matter of fairness, I have to correct one of my earlier statements.
Andrei Popescu correctly pointed out at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00059.html
that neither "being based on a meta-logic" (i.e., a logical framework) nor
"featuring a natural deduction system" creates a problem.
There has been a misunderstanding on my part.
However, I have to say that Paulson's definition of the turnstile as a symbol
for the predicate "hfthm" in
"inductive hfthm :: "fm set => fm => bool" (infixl "⊢" 55)"
https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html
somewhere hidden in the proof files without being prominently announced in his
articles is strongly misleading and inevitably creates misinterpretations.
Usually (such as in [Andrews, 2002]), the turnstile is used to indicate the
provability of a theorem of the logic in which the proof is undertaken, not the
provability of theorems of the embedded logic. Also, for the predicate of
provability of theorems of the embedded (represented, formalized) logic, a
label is usually used, not a symbolic notation (e.g., Goedel uses "Bew" - for
"beweisbare Formel", the German expression for "provable formula" -, and
O'Connor in Coq uses "SysPrf"). Moreover, without some short introduction to
the notation and the type system it is nearly impossible to analyze the proof
in detail unless one has advanced experience with the Isabelle proof assistant,
leaving aside that with a logical framework there are not only three, but four
language levels involved, all of which one would ideally need to understand in
order to verify the proof.
The result of the formal proof
~Bew(g) /\ ~Bew(not g)
can be interpreted in the sense that it is possible to construe a formula with
the form of a sentence (i.e., a boolean-valued well-formed formula with no free
variables) neither provable nor refutable.
Nevertheless, the claim of "incompleteness" depends on a philosophical
assumption.
One who shares the semantic view (model theory) will conclude that there is a
meaningful (and true) sentence that is neither provable nor refutable, and will
call the discrepancy between syntax and semantics "incompleteness".
But one who shares the syntactic view will conclude that it is possible to
create a meaningless formula which has the form of a syntactically correct
sentence (similar, in natural language, to a grammatically correct but
meaningless statement like "mathematics is liquid").
Concerning the two objections of Ramana Kumar at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-December/msg00061.html
the first one was a misunderstanding clarified at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-January/msg00029.html
But the second, Ramana Kumar's claim that type "tm" can be defined like type
"nat", is not correct. Andrews' logic Q0, being an improved variant of Church's
original simple type theory, only allows the types iota (i) and omicron (o),
and combinations of them.
Andrews' type "nat" is such a combination ( nat := (o(oi)) ). On the contrary,
Paulson's type "tm" is an inductively defined type, which is not possible in Q0:
"nominal_datatype tm = Zero | Var name | Eats tm tm"
https://www.isa-afp.org/browser_info/current/AFP/Incompleteness/SyntaxN.html
In an e-mail, Paulson basically argued that there should be ways to introduce
further types (instead of restricting oneself to combinations of 'i' and 'o').
This is, of course, correct, but doesn't justify the specific mode of type
introduction used here, namely the Backus-Naur form (BNF). The BNF was designed
to specify formal grammars in computer science, but (mathematical) types are
objects that must have certain logical properties, such as being non-empty.
Thus the introduction of additional mathematical types should be subject to
proof, and not a matter of mere declaration via the BNF.
With some more knowledge about the concept of the current proof assistants, I
can answer Ramana Kumar's question at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00149.html
concerning the motivation of my project announcement at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
from his perspective now.
Current proof assistants seem to follow the semantic approach, in which the
theory is distinguished from a specific linguistic (formal) formulation, or use
of model theoretic notions like satisfiability is made. For example, in
Isabelle there are implementations of both axiomatic set theory (Isabelle/ZF)
and type theory (Isabelle/HOL), but neither one is explicitly preferred, and
the question of which is more adequate for representing mathematics is not even
raised. (Although, unlike in informal mathematics, in formalized proofs type
theory seems to prevail, e.g., within Isabelle the logic Isabelle/HOL, a
polymorphic version of Church's simple type theory.)
If one follows the syntactic approach, then there is a desire for something
like the ideal formulation or the natural language of formal logic and
mathematics. The main criterion is expressiveness [cf. Andrews, 2002, p. 205],
or, vice versa, the reducibility of mathematics to a minimal set of primitive
rules and symbols. If we leave away for a moment the restrictions of Q0 of
still being a formulation of simple type theory (i.e., without type variables
and dependent types), all of formal logic and mathematics can be expressed on
the basis of only a "single rule of inference (substitution, from which the
rule of modus ponens is derived)" and "only two basic types (individuals and
truth values) and only two basic constants (identity/equality and its
counterpart, description)"
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html
Paulson argued that natural deduction is far superior to Hilbert-style systems
for automated proof. This is, of course, correct, since Hilbert-style
metatheorems become symbolically representable in natural deduction as regular
theorems (and not just metatheorems), but this only reflects the engineer's
perspective with the pragmatic aim of quickly obtaining proofs. For the
philosopher it is not proof automation but expressiveness that is the main
criterion, such that the method with the least amount of rules of inferences,
i.e., a Hilbert-style system, is preferred, and all other rules become derived
rules.
Hence, from the perspective of the syntactic view, Andrews' elegant logic Q0 is
the natural point to start with. Overcoming its restrictions by extending it to
a polymorphic (with type variables) and dependent type theory (with dependent
types) is the motivation of my logic R0, which I hope to be able to publish
soon. A preliminary excerpt with some definitions and a sample proof is
available online at
http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf
Kind regards,
Ken Kubota
Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100
Email Gateway (Aug 22 2022 at 13:44):From: Gottfried Barrow <igbi@gmx.com>
In particular, there is this sentence of yours: "...this only reflects
the engineer's perspective with the pragmatic aim of quickly obtaining
proofs. For the philosopher it is not proof automation but
expressiveness that is the main criterion..."
I completely understand the issue of low status vs. high status, and the
importance of trying to assert one's status, by bandying about labels,
with the hopes that labels will stick.
I myself, at one time, aspired to be a philosopher, and mind you, no
mere philosopher, but the mother-of-all-philosophers, as this would give
me the ability to bandy about the mother-of-all-condensations, along
with, certainly, the mother-of-all-condescensions.
Having aspired, I steeled myself, and struck the philosopher's pose,
after which, my arm fell asleep. Surely, if I could have endured even 5
more minutes, the answer would have come, "42", and therefore, the
prize. It was not to be.
Reevaluating my aspirations, I lowered them, and aspired to be an
engineer, so that I could at least condescend to technicians.
Being a man of action, I went out and bought a little train set, and
spent hours and hours painting the little cars, in intricate detail.
But one day, when I was engineering my little train set, saying, "choo,
choo, choo" to the little train cars, the little kids next door heard
me, because the window was open, and they started laughing at me.
Do you know how bad it hurts to have little kids laugh at you, when
you're saying, "choo, choo, choo"?
So in one massive swoop, I destroyed my little train set, to show those
little kids what a bad martial artist I was, MMA style.
They just kept laughing.
It was no great loss. I was actually only aspiring to be a bad martial
artist, MMA style.
--
GZ
--
Email Gateway (Aug 22 2022 at 13:45):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
The difference seems that between "What" and "How" rather.
Email Gateway (Aug 22 2022 at 13:46):From: Gottfried Barrow <igbi@gmx.com>
No serious discussion what supposed to ensue, and it's not supposed to
start with my reply here. Your short sentence tells me that maybe you
didn't focus on my jokes.
Any seriousness was supposed to get swamped by my attempt at creative
writing. The attempt at creativity was for the purposes of ridiculing an
idea. There was actually no need for a defense to be made. Writing
nothing would have been better, maybe.
Ken wants to compare his raw ideas, valid or not (I wouldn't know), with
Larry Paulson's work, which is the foundation for what has ended up
being more than 30 years work, founded on Robin Milner's ML, drawing
from Mike Gordon's work, propelled further by Tobias Nipkow et al.
I'm nobody's friend here, but I gotta figure that Isabelle, its logic
included, simply represents what Larry Paulson decided to commit to as a
public work, that its not the totality of his mind.
As to "what", "how", and "why", it's not like he hasn't been exposed to
a full gamut of ideas, including that which is pure and impractical.
People want to attack the purity of Isabelle/Pure, but without providing
a serious alternative. Maybe it's the "30 years work thing", that a
serious work takes.
GZ
Email Gateway (Aug 22 2022 at 13:47):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
On 12.07.2016 02:19, Gottfried Barrow wrote:
On 7/11/2016 2:57 AM, Andreas Röhler wrote:
On 09.07.2016 05:05, Gottfried Barrow wrote:
On 7/7/2016 11:26 AM, Ken Kubota wrote:
Paulson argued that natural deduction is far superior to
Hilbert-style systems
for automated proof. This is, of course, correct, since Hilbert-style
metatheorems become symbolically representable in natural deduction
as regular
theorems (and not just metatheorems), but this only reflects the
engineer's
perspective with the pragmatic aim of quickly obtaining proofs. For
the
philosopher it is not proof automation but expressiveness that is
the main
criterion, such that the method with the least amount of rules of
inferences,
i.e., a Hilbert-style system, is preferred, and all other rules
become derived
rules.In particular, there is this sentence of yours: "...this only
reflects the engineer's perspective with the pragmatic aim of
quickly obtaining proofs. For the philosopher it is not proof
automation but expressiveness that is the main criterion..."I completely understand the issue of low status vs. high status [ ... ]
The difference seems that between "What" and "How" rather.
No serious discussion what supposed to ensue, and it's not supposed to
start with my reply here. Your short sentence tells me that maybe you
didn't focus on my jokes.
Indeed.
Any seriousness was supposed to get swamped by my attempt at creative
writing. The attempt at creativity was for the purposes of ridiculing
an idea. There was actually no need for a defense to be made. Writing
nothing would have been better, maybe.Ken wants to compare his raw ideas, valid or not (I wouldn't know),
with Larry Paulson's work, which is the foundation for what has ended
up being more than 30 years work, founded on Robin Milner's ML,
drawing from Mike Gordon's work, propelled further by Tobias Nipkow et
al.
Well, "valid or not" is indeed the question, nothing else.
Last updated: Nov 21 2024 at 12:39 UTC