Re: [isabelle] Some remarks on natural deduction and axiomatic set theory


I am addressing you some, but not soley. I think I've said enough to make it clear that I'm not a representative, in any way, of the professional community that surrounds Isabelle.

It is my goal to follow through and not have my name end up here much, but everyone serves their purpose, and there are things of value I can bring attention to, even if it's mixed in with a lot of noise. The existence of a meta-logic and object-logic in Isabelle is an endless source of confusion for newcomers, and a few basics can clear that up. My last email served to bring attention to that once again, along with the reference to "Logic and Computation", by Paulson.

Here is the thesis of this email: proof assistants are a game-changer. I will try to bring my points back around to that.

Ken, please don't miss the part below, in my lecture on etiquette,where I say this:

If, in a reply to me, you add emails to people who weren't party to the discussion, you are a gross violator of decent etiquette.


The last email, I thought that I bordered on being rude, relative to the normal professionalism here, but it didn't get through to you.

With proof assistants, for formal logic it now becomes "deeds not words". I say that as a buffer to the rude form: "put up or shut up". It could be my "put up or shut up" theme doesn't deserve to get through to the mailing list.

When we criticize someone's software, there's a simple comeback for the author, which is some variation of "If you're so smart, then why don't you go ahead and fix it?"

If you're so bold as to say that the logic of Isabelle may be inconsistent, then why don't you "put up" by showing that it's inconsistent. Otherwise, "shut up" about it. Deeds not words.

Meta-think is obviously needed to set up or analyze an object language or an object-logic (and even a meta-logic). Consequently, it may appear that the domain of the meta-think remains domain of the human mind.

Not at all. (I'm polluting my point somehow. Semantics anyone? But for meta-thinkers only. Syntax is sufficient for object-think.) Any smart meta-thinker who can program should be able to code up the meta-ideas, and proof assistants move the expectations to "You're boring me with your talk. Code it up, so we have something fixed to talk about".

If you're so bold as to claim that Isabelle is imperfect, then "put up" and implement the perfect logic. Well, you appear to have coded up the basics of something. And the world now is supposed to stop and jump on your logic wagon?

The problem with "put up" is that it's subjective. I'll state my opinion. You haven't. I'll leave the "shut up" as implied.

What I say now is at least as important as what I just said.

I myself abuse etiquette, but I don't add email addresses in a reply to people who haven't been party to a thread.

Your first email was to 6 people plus the user list. I responded back only to the user list address. That was a very intentional act on my part.

You could have at least addressed it to "Dear List Members and Gottfried Barrow".

I am not in the same class as "List Members". List members in general most likely have a PhD and are qualified, or more qualified than me to be meta-thinkers. I have a B.S. in math and am qualified to potentially be a respectable object-thinker.

We're all a team, and we don't even have to like each other. It's object-think-users who are needed here, not meta-thinkers.

But even object-thinkers can recognize basic mistakes in thinking, like a person making a big deal about a theorem holding under one set of axioms, but not under another set of axioms, where I'm assuming I don't have a total misunderstanding of what you've said.

There is no need for me to be a meta-thinker. I want to do math, not forever be bogged down in foundations. First-order logic comes for free with HOL. With functional-prog-logic, I'm way ahead of the Z-Crowd already, with their 5 millimeters. I need true, false, and the Law of Excluded Middle. The Axiom of Choice? Of course. But your stuff? I need it?

Don't diss the team, dude, and don't spam the team leaders, or those external, while also making me a part of it.But don't worry, I'm a nobody. Nothing will be lost by not including me with all the other people.

If, in a reply to me, you add emails to people who weren't party to the discussion, you are a gross violator of decent etiquette. (I heavily watered that sentence down, to also try and respect the professionals here.)


I guess I had a point to make. I'll go ahead and pull a quote of yours, after all:

"Since my philosophical background rejects any sort of metatheories... "

Hmm. Sounds like a heavy burden to carry. My philosophical background is the extent to which I've spoken philosophically, and I only require that to the extent I've said stupid things, I don't say them again.

So you're talking about purity. I guess I don't care here, so I don't need to speak for Larry Paulson, and say whether he is or isn't a purist.

I do know he takes practical things into consideration, as demonstrated by a recent comment he made on the FOM mailing list, which I link to below.

Where is there room here for me to speak of the "all-or-nothing-requirement", for people more picky than me, about what they need to get them to abandon their 5 millimeter mechanical pencils? It all has to be good.

For mechanized proof, where math is literature, a great logic is useless without the-rest-of-it, which you ain't got.

If you want purity, in the way you want purity, code it up, and suffer the impracticalities of your own product. But syntactically, how can anything be pure, when programming languages have to be used, with the thousands of details involved? The absence of details is actually part of the current illusion-of-elegance for traditional logics, as if there's more than one in force.


Pay attention, or not, to Larry Paulson:

  It looks like I need to clarify my remark about âimposing unreasonable costsâ.
  Under this I do not include the difficulty of implementing a proof assistant,
  because our job is to build things and let the computer do the work. The costs
  rather are those imposed on users who have to work within the free logic. I
  often compare theorem proving in a formal logic to building a ship in a bottle,
  and nobody wants to make the bottle any smaller, or the ship any bigger. To be
  more precise, I have seen proof-theoretic work showing that very small changes
  to a proof calculus can increase the length of a formal proof, in the worst case,
  by a non-elementary factor. It isnât obvious that the use of a free logic would
  be as costly as that, but I get the impression that users who have tried such
  systems have not been happy with the effort involved. I donât believe that good
  automation could entirely eliminate this effort.

I forgot how I was supposed to use this, but it's about Robert M. Solovay.

Steven Obua published "Partizan Games in Isabelle/HOLZF":

In it, he references Robert Solovay as saying that axioms added to Isabelle/HOL will be consistent. That gave me enough confidence to consider it wouldn't be a waste of my time to mess around with adding the axioms, similar to how Obua does it.

Initially, I couldn't find the reference, then one day, I searched again, and it came up:!msg/fa.isabelle/fKOEdb7uqJk/qYY1-MNxwSsJ

Solovay writes:

This alternative is certainly possible, but [if I understand it correctly]
  is not what I'm interested in.

  Your version: [HOL in ZFC] has the same consistency strength as ZFC.

  My version [ZFC in HOL] would have consistency strength considerably
  greater than ZFC [just a shade less than Zermolo + Choice + "There is an
  inacessible cardinal].

How can I tie this into you, Ken?

You think you're the only one with ideas? Ideas are a dime a dozen. Ideas aren't a problem. Time is a problem, with the upper limit of mortality being the ultimate arbiter of time.

In overstating things, I said no one cares about a raw logic. I can also say that I'm interested in everything, but have time for nothing.


The new game for logic will be proof assistants. The game will not be played in full force until people can get educated in the rules of the game, in a reasonable amount of time.

When the game is in full force, cheap talk won't be tolerated much, but then, the idea of wanting to engage in cheap talk will be foreign to the vast number of people who want to play the game of logic.

These days, find a bunch of programmers, doing meta-talk. In general, they're doers. They all write programs. They talk about what others have done, or what they've done. Talk and do. They do them both.

That'll be the future of the game of mathematics. Whether low or high, there will be no place for cheap and undeserved glory.


I hate giving away my potential secrets to success, but I'm a benevolent person.

Logic? Meta-think? Definitely crowded games to play, since the last mods for fixing naive sets was, when? Yea, not recent.

Hopeless situation? No, not with the trifecta-of-potential-success for True Artistes: dance, trance, and disco.

That's not to say that some things don't stay the same.

For example, you never want show up on the dance floor and start dissin' John Travolta, and not have, at least, disco moves that are as good as John's in Saturday Night Fever.

Suppose you put your platform shoes on, your bell bottoms, your polyester shirt on, and have your shirt unbuttoned with your gold chain showing. Absolutely necessary, but if you ain't got no impressive disco moves, after dissin' John, what you got ain't nothin' to nobody nowhere, especially right there beside the dance floor, with everybody and his brother wannabe Disco John watchin'.

Suppose you wax long about the optimal angle at which the index finger should be pointing at the ceiling. And after dissin' John? At that point, it becomes obvious what you got, which is a spot beside the dance floor, wearing platform shoes, bell bottoms, and a polyester shirt, unbuttoned to show your gold chain. That, my friend, ain't a good situation to be in, since disco garb with no disco moves is, uh, not good.

Oh, you're the martial artist type, kung fu maybe?

What I can say about that is you don't want to show up at the dojo and start dissin' Bruce Lee. Suppose you strike your best kung fu pose...

Well, you get the picture. Or maybe you don't.


On 12/16/2015 12:29 PM, Ken Kubota wrote:
Dear Gottfried Barrow and List Members,

Thank you for your comment at

concerning my note available at

Let me respond to the last three paragraphs of your comment quoted below which
summarize the most important questions.

1. There is no relation between a simple minimum core logic and the
expressiveness of the formal language. A modular software design guarantees a
clear separation of functionality such that the logic is concentrated in the
logical core and no enhancements of other software layers (i.e., user
interface, proof tactics) will have an effect on the correctness of the logic.
This concept is, according to Andrei Popescu, shared by all implementations in
discussion here: "A small logic kernel is an implementation-independent virtue
of Isabelle/HOL as well as of all the Gordon-HOL systems."

"It is the logical reliability due to reduction that builds the core of the
LCF-approach to theorem proving (or LCF-style full expansiveness [cf. Gordon,
2000, p. 178]): 'All proofs are ultimately performed in terms of a small set of
primitive inferences, so provided this small logical kernel is correct the
results should be reliable.' [Harrison, 2009, p. 60]" [Kubota, 2015a, pp. 12 f.]

The idea behind the LCF-approach appealing also to those who do not share
metatheoretical concepts such as the semantic approach (model theory) is to
reduce the set of rules and elements, such that the logical core is minimized
without loss of expressiveness. I called it the "The Principle of Reductionism"
[Kubota, 2015a, p. 11].

In Peter B. Andrews' logic Q0 this principle is - by the use of syntactical
means only - consequently carried out, such that the basic means of the
language are reduced without loss of expressiveness to
- a single rule of inference,
- a single variable binder,
- only two constants and
- only two types,
obtaining "definability of all of the propositional connectives, as well as all
of the quantifiers (universal, existential and uniqueness quantifier)" and
derivability of all other rules including the rule of modus ponens as mentioned
earlier at

In other words, with this simple minimum core logic of Q0 all of formal logic
and large parts of mathematics, and with type variables (polymorphic type
theory) and the binding of type variables with lambda (dependent type theory),
presumably all of mathematics can be construed, expressed and proved purely
syntactically. Due to its simplicity, the logical kernel becomes extremely
small and logically robust, i.e., mathematically safe.

In the R0 implementation, the propositional connectives therefore are not part
of the logical core, but their definitions are "outsourced" into a file and,
for example, the rule of modus ponens into a separate proof template file. In
fact, the expressiveness of R0 as a logistic system is stronger than that of
Isabelle/HOL. Isabelle/HOL allows for type variables and therefore has the
expressiveness of polymorphic type theory, but only R0 allows, in addition to
that, the binding of type variables with lambda as abstraction operator and
therefore enables the construction of types required for dependent type theory.

2. Any axiom schema requires a meta-level for instantiation. Since my
philosophical background rejects any sort of metatheories (I prefer to speak of
arithmetization of mathematics instead of metamathematics, refuting any
foundational or legitimating role of metatheories), an axiom schema - like any
other meta-construction - always reveals a deficit. Whereas Andrews' logic Q0
requires an "Axiom Schema 3" [Andrews, 2002, p. 213] (with "syntactical
variables ranging over type symbols" [Andrews, 2002, p. 210]) for the Axiom of
Extensionality, R0 uses regular type variables for this axiom [cf. Kubota,
2015a, pp. 39, 351], which were not available in Q0 being a simple type theory,
i.e., without type variables.

Moreover, axiomatic set theory as a whole is subject to critique: "Axiomatic
set theory uses axioms to justify the existence of certain sets. Unless the
proof of existence from these axioms is provided, any construction cannot be
introduced into the domain of discourse. This approach, however, is not
systematic and subject to arbitrary conditions. For example, the most common
formulation, the Zermelo-Fraenkel set theory with the Axiom of Choice (ZFC),
comprises axioms for the empty set, union, one-element sets, power sets etc.,
trying to cover the standard sets used in mathematics. But there always remain
legitimate sets not contained by these axioms; for example it is well known
that large cardinal numbers and certain universes cannot be treated within ZFC
(without assuming additional axioms), although from a purely logical point of
view there is no difference between the mathematical objects covered by ZFC and
those not covered.

This problem has its origin in the approach itself, as axiomatic set theory
makes use of non-logical axioms to establish sets, thus trying to avoid
paradoxes via content restrictions instead of the proper specification of the
formal language. Opting this method, axiomatic set theory including ZFC is
bound to remain a preliminary and auxiliary approach, but not the foundation of
mathematics." [Kubota, 2015a, p. 18].

3. Russell's paradox ("the set of all sets that are not members of themselves",
or originally: "Let w be the predicate: to be a predicate that cannot be
predicated of itself. [...] Likewise there is no class (as a totality) of those
classes which, each taken as a totality, do not belong to themselves."
[Russell, 1902, p. 125]) with the two constitutive properties of antinomies,
self-reference and negativity (negation), ruled out Cantor's naive set theory
as a foundation of mathematics. If Goedel's construction of a proposition
involving self-referencing negativity ("I am not provable", or originally: "We
therefore have before us a proposition that says about itself that it is not
provable" [GÃdel, 1931, p. 598]) has to be considered as an antinomy, further
research will have to find out whether it rules out natural deduction
(including sequent calculus) for the foundation of mathematics as a whole or
whether a clear distinction of the object language and the meta-language can be
introduced into natural deduction.

The strict distinction of the object language and the meta-language was so
important to Church that he emphasized it a second time in his article: "We
must, of course, distinguish between formal theorems, or theorems of the
system, and syntactical theorems, or theorems about the system, this and
related distinctions being a necessary part of the process of using a known
language (English) to set up another (more exact) language." [Church, 1940, p.

In natural deduction, as for example in Isabelle, metatheorems (in terms of
Hilbert-style systems) become part of the formal language (the object language)
itself. So from the point of view of axiomatic (Hilbert-style) deductive
systems, the expressiveness in natural deduction is shifted towards the
meta-level, possibly at the cost of expressiveness at the object level. This
caused me to introduce an own terminology with the notions of "object logic"
and "meta-logic" in my second publication on Goedel [cf. Kubota, 2015] until
realizing that the definitional line between "object logic" and "meta-logic" is
identical with that between axiomatic (Hilbert-style) deductive systems and
natural deduction, having found the number of allowed occurrences of the
deduction symbol (turnstile) in a theorem as a formal criterion. The
translation mechanism from a theorem to the existence of its proof (or vice
versa) in Goedel's First Incompleteness Theorem is in Paulson's presentation
his theorem 'proved_iff_proved_PfP' - called (P) in my article -, in Andrews'
presentation the implicit rule used for step 7101.4. Whereas in Andrews' system
this implicit rule immediately results in inconsistency [cf. Kubota, 2015, pp.
10 f.], I am not sure whether this applies to natural deduction, too. Because
of a limited expressiveness at the object level, the antinomy might be
construed without causing an openly visible inconsistency in the formal
language, since "the two occurrences of the deduction symbol [...] remain an
obstacle for obtaining a paradox [i.e., an inconsistency] in the metalogic
[i.e., in natural deduction]" [Kubota, 2015, p. 14]. Then, "GÃdel's first
incompleteness theorem: If consistent, our theory is incomplete." (Paulson) is
rendered from a hypothetical judgement to a trivial tautology in the form of a
conclusio ex falso, since the theory under consideration is actually
inconsistent. However, an antinomy (paradox) should not be expressible at all
(in formal logic and mathematics).

If natural deduction is ruled out for the foundation of mathematics, there
would be no other "fix" for Isabelle than switching to an axiomatic
(Hilbert-style) deductive system. Then, if one does not want to downgrade from
higher-order logic (which would artificially limit the expressiveness of the
language) and prefers to remain in the realm of Russell's invention, namely
type theory [cf. Russell, 1908], basically three options would be left:
a) Church's Hilbert-style system of 1940 [cf. Church, 1940] (simple type
theory, i.e., without type variables)
b) Andrews' logic Q0 [cf. Andrews, 2002, pp. 210-215], an improved formulation
with identity (equality) as the main notion (also simple type theory, i.e.,
without type variables), first published in 1963 as a simplification of
Henkin's variant of Church's formulation [cf. Andrews, 1963, pp. 345 f., 350]
and described at
c) my own logic R0 [cf. Kubota, 2015a] (polymorphic and dependent type theory,
i.e., with type variables and types depending on arguments due to type
variables bound with lambda), a further development of Q0, described at

In his Ph.D. thesis, Andrews developed a transfinite type theory with type
variables Q [cf. Andrews, 1965, pp. 3-8], which is already some sort of
polymorphic type theory. But instead of consequently reducing the variable
binders to a single one as in Q0 (with the abstraction operator and single
variable binder lambda, obtaining definability of the universal, existential
and uniqueness quantifier) at the type level of Q also, which would have built
the foundation of a dependent type theory, the universal quantifier becomes a
true variable binder (an improper symbol) in the case of types (for details
[cf. Kubota, 2015a, p. 31]).

Concerning Isabelle, I do not believe that "30 years" and "millions of dollars"
are simply lost. Both Goedel's First Incompleteness Theorem and natural
deduction have been publicly available for about 80 years now, in relation to
which shorter periods and any economic quantities appear relatively small. I
highly value Paulson's presentation of Goedel's First Incompleteness Theorem,
which, unlike all other presentations I studied (Andrews and Rautenberg), does
not use a shortcut for (P), but a proven theorem, leaving only the (rather
methodological) implicit assumptions of
- natural deduction (or at least the lack of a clear distinction of the object
language and the meta-language) and
- the semantic approach (model theory invented by Tarski),
assuming otherwise correctness of the syntactical inference in Isabelle. Maybe
this fully formalized presentation of Goedel's First Incompleteness Theorem by
Professor Paulson as the climax in the development and application of the
Isabelle proof assistant software was even a necessary step for evaluating the
implications (and potential deficits) of natural deduction.

Following the arguments given above, the path to the natural and ideal
formulation of formal logic and mathematics is narrowed down to higher-order
logic in the form of a Hilbert-style type theory, unless natural deduction is
reformulated in a way that preserves the distinction of the object language and
the meta-language, and the possibility of offering clarification here seems to
me to be one of the most important tasks at present.

In order to do so, I suggest the careful examination of Paulson's presentation
of Goedel's First Incompleteness Theorem under consideration of the critique of
James R. Meyer [cf. Meyer, 2015] and myself both printed [cf. Kubota, 2013;
Kubota, 2015] and online at

This seems even more important, as with the critique of natural deduction or
certain modes of its implementation, all current major theorem provers, such as
- Lawrence C. Paulson's Isabelle (proof claimed by Lawrence C. Paulson),
- Coq by INRIA et al. (proof claimed by Russell O'Connor), and
- Mike Gordon's original HOL system and its variants, including
- John Harrison's HOL Light (proof claimed by John Harrison),
might be affected, as they all rely - either as the single form of inference or
as one of several components - on natural deduction (considering sequent
calculus as a subcase here, defining natural deduction as opposed to
Hilbert-style systems).

The only older theorem prover, in which Goedel's First Incompleteness Theorem
was claimed to be proven,
- Robert S. Boyer's and J. Strother Moore's Nqthm (proof claimed by Natarajan
obviously allows the instantiation of metatheorems, which might violate the
object language ("Proved meta-theorems can be installed as simplifiers",, December 13, 2015).

Kind regards,

Ken Kubota


Andrews, Peter B. (1963), "A reduction of the axioms for the theory of
propositional types". In: Fundamenta Mathematicae 52, pp. 345-350.

Andrews, Peter B. (1965), A Transfinite Type Theory with Type Variables.
Amsterdam: North-Holland Publishing Company.

Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type
Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London:
Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: 10.1007/978-94-015-9934-4.

Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In:
Journal of Symbolic Logic 5, pp. 56-68.

GÃdel, Kurt (1931), "On formally undecidable propositions of Principia
mathematica and related systems I". In: Heijenoort, Jean van, ed. (1967), From
Frege to GÃdel: A Source Book in Mathematical Logic, 1879-1931. Cambridge,
Massachusetts: Harvard University Press, pp. 596-616.

Kubota, Ken (2013), On Some Doubts Concerning the Formal Correctness of GÃdel's
Incompleteness Theorem. Berlin: Owl of Minerva Press. ISBN 978-3-943334-04-3.
DOI: 10.4444/100.101. See:

Kubota, Ken (2015), GÃdel Revisited. Some More Doubts Concerning the Formal
Correctness of GÃdel's Incompleteness Theorem. Berlin: Owl of Minerva Press.
ISBN 978-3-943334-06-7. DOI: 10.4444/100.102. See:

Kubota, Ken (2015a), On the Theory of Mathematical Forms (Draft of May 18,
2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5
45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50
011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See:

Meyer, James R. (2015), "A Fundamental Flaw in An Incompleteness Proof by
StanisÅaw Åwierczkowski" (v2 30 Apr 2015). SHA-512:
380de2a2e4dfa0441d7d3019025a1e49 87fd9282cb309fd7abd7be667879e554
696f5e265d911799ecf7416b9c0cf3c0 fbdb2a10bab58532f9a117ddee2b3866. Available
online at (November 28,

Russell, Bertrand (1902), "Letter to Frege". In: Heijenoort, Jean van, ed.
(1967), From Frege to GÃdel: A Source Book in Mathematical Logic, 1879-1931.
Cambridge, Massachusetts: Harvard University Press, pp. 124 f.

Russell, Bertrand (1908), "Mathematical Logic as based on the Theory of Types".
In: American Journal of Mathematics 30, pp. 222-262.

Am 09.12.2015 um 19:10 schrieb Gottfried Barrow<igbi at>:


Really, what would be of more value? A generalized logic that stands the test
of time, such as Isabelle/Pure and Isabelle/HOL, or a very narrow logic, such
as what you advise?

How are people supposed to test the generalized logic, over many years, if the
safer route is taken. And an inconsistent logic is not a crisis anyway. An
inconsistent logic that can't be fixed with "don't do that" is a crisis. A loss
of 30 years, that's a crisis.

ZFC is an inconsistent logic that was fixed with "don't do that". It's called
the Axiom Schema of Separation. It's ugly, because it demands a new axiom for
every subset of a set. Or is "ugly" just a matter of perception?


Ken Kubota
doi: 10.4444/100

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.