Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Preprint on grounded arithmetic (GA) metatheor...

view this post on Zulip Email Gateway (Jan 27 2026 at 17:06):

From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>

Dear Isabelle users,

I wanted to announce an arXiv preprint that might interest some of you:

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
https://bford.info/pub/lang/ga/

This is about a development of the metatheory of grounded arithmetic (GA), a development of a paracomplete logic/arithmetic partly inspired by Kripke’s theory of truth, using Isabelle/HOL as the working metalogic. It is currently about ~35K lines of Isabelle/HOL and counting, and includes quite a bit of recursion theory including a metacircular evaluator as foundations. The code repository isn’t public yet but the plan is to make it public with the paper’s formal publication, and in the meantime is shareable privately with colleagues with particular interest and relevant expertise. I also hope to submit at least the recursion theory part to the AFP, at some point, once it’s cleaned up and better documented.

Isabelle has served this project extremely well so far — a big thanks to all you who built and continue to maintain it! But I have built up a small “Isabelle wishlist” and wanted to ask if there might be support for a few potential improvements, which we would be happy to help with under Isabelle developer guidance:

None of these are urgent by any means, and again we’re happy to help by submitting concrete patches for example if there’s support for them.

Thanks
Bryan

view this post on Zulip Email Gateway (Jan 29 2026 at 12:19):

From: Lawrence Paulson <lp15@cam.ac.uk>

Dear Bryan, many thanks for your suggestions. I second the request for Quine quotes, which are often used in some branches of logic, and I hope that is a straightforward thing to do. Similarly for the other symbols you name.

As for “undefined", I'm not sure how difficult it would be to organise and it's not clear how useful it could be. There is nothing special about "undefined" and in particular you cannot conclude anything from “f x = undefined”. instead, we define x/0 = 0, from which we get a lot of algebraic identities to be unconditional. Lean regards even log as a total function, with ln(-x) = ln(x), which we have now adopted.

Larry

On 27 Jan 2026, at 17:06, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk> wrote:

view this post on Zulip Email Gateway (Jan 29 2026 at 17:57):

From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>

Thanks Larry for your feedback and support in the suggestions!

On 29 Jan 2026, at 13:19, Lawrence Paulson <lp15@cam.ac.uk> wrote:

Dear Bryan, many thanks for your suggestions. I second the request for Quine quotes, which are often used in some branches of logic, and I hope that is a straightforward thing to do. Similarly for the other symbols you name.

As for “undefined", I'm not sure how difficult it would be to organise and it's not clear how useful it could be. There is nothing special about "undefined" and in particular you cannot conclude anything from “f x = undefined”. instead, we define x/0 = 0, from which we get a lot of algebraic identities to be unconditional. Lean regards even log as a total function, with ln(-x) = ln(x), which we have now adopted.

For our purposes, the one useful thing about undefined is that it’s a constant — meaning anything equal to the “undefined” constant is also at least equal to anything else equal to the "undefined” constant, even if we can’t prove anything else about which member of a given type that constant might be.

Why this matters for us is that if, for example, the nth function in List.thy returned the “undefined” constant when nth is invoked on an empty list, then we could prove nth to be primitive-recursive. With Isabelle’s current semantics, however, we can’t even prove nth to be primitive-recursive, because “nth n []” is an arbitrary potentially-non-computable function of n, and not a constant. We instead have to define a different function that behaves the same way as nth for all “valid” inputs and prove that primitive recursive. We can also prove nth itself to be conditionally primitive recursive, conditioned on the inputs being valid (i.e., n < length of the list), but that just creates other unnecessary pain in using that conditional primitive-recursiveness proof.

With nth (or its equivalent) returning the undefined constant on invalid inputs, in contrast, we can Gödel-encode that undefined constant in any Gödel-encodable type, even if we don’t know precisely which value of that type “undefined” actually is, and we can prove that there exists a primitive-recursive function taking a natural number n and the Gödel code of a list and yielding the Gödel code of a list element; we simply arrange for that primitive recursive function to return the Gödel code of “undefined” of the appropriate type, whatever that is (we don’t care) in the case of invalid input arguments. So our inability to prove anything about what the undefined constant is doesn’t get in the way of primitive-recursiveness proofs at all for our purposes; what gets in the way is the fact that “nth n []” for example is not any constant but an undefined function. This is in fact inconsistent with how HOL already treats case statements, and it seems it would at least be better for the semantics to be consistent and “more-defined” in terms of at least producing the undefined constant and not an undefined function for undefined patterns.

I don’t have any objection to making such functions even more defined when appropriate, e.g., the x/0 = 0 example you mentioned. But in the case of the nth function, for example, it’s not clear to me what useful more-distinguished output value we might choose for invalid inputs like “nth n []”, since the list element type is polymorphic and doesn’t necessarily have an obvious distinguished “default” or “zero-like” element. I would personally rather have nth always return some, any, constant in the case of undefined inputs rather than add unnecessary constraints to the list element type (or to the classes of element types for which we could prove it primitive recursive).

Hope this clarifies our motivation for the “undefined constant” wishlist item.

In any case, thanks again for your consideration and feedback.
Bryan

Larry

On 27 Jan 2026, at 17:06, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk> wrote:

view this post on Zulip Email Gateway (Jan 29 2026 at 19:27):

From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>

Hi John,

On 29 Jan 2026, at 19:49, Hughes, John <john_hughes@brown.edu> wrote:

datatype t = Base
[…]
In view of this, Bryan might also want to consider what he would want

nth ([]::t list) 7

to evaluate to. If it evaluates to "undefined", then it also evaluates to "Base", which doesn't seem to match the semantics of "nth".

Thanks for your thoughts. I have no objection to single-element types in principle, but what exactly the semantics of single-element types “should” be seems orthogonal to the semantic issue I raised. In HOL, the only possible semantic value of any function returning a single-element type must be that it always yields the one and only value of that type, regardless of how you define the function, since HOL functions are always total. They always return something, and if there’s only one thing they can return, then that’s the something they return no matter what. Changing that characteristic of HOL would be a much, much, much more fundamental and universe-breaking change to HOL than the small change I’m proposing to the handling of uncovered patterns in ‘fun’ and ‘primrec’ definitions.

B

--John

On Thu, Jan 29, 2026 at 12:57 PM Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:
Thanks Larry for your feedback and support in the suggestions!

On 29 Jan 2026, at 13:19, Lawrence Paulson <lp15@cam.ac.uk<mailto:lp15@cam.ac.uk>> wrote:

Dear Bryan, many thanks for your suggestions. I second the request for Quine quotes, which are often used in some branches of logic, and I hope that is a straightforward thing to do. Similarly for the other symbols you name.

As for “undefined", I'm not sure how difficult it would be to organise and it's not clear how useful it could be. There is nothing special about "undefined" and in particular you cannot conclude anything from “f x = undefined”. instead, we define x/0 = 0, from which we get a lot of algebraic identities to be unconditional. Lean regards even log as a total function, with ln(-x) = ln(x), which we have now adopted.

For our purposes, the one useful thing about undefined is that it’s a constant — meaning anything equal to the “undefined” constant is also at least equal to anything else equal to the "undefined” constant, even if we can’t prove anything else about which member of a given type that constant might be.

Why this matters for us is that if, for example, the nth function in List.thy returned the “undefined” constant when nth is invoked on an empty list, then we could prove nth to be primitive-recursive. With Isabelle’s current semantics, however, we can’t even prove nth to be primitive-recursive, because “nth n []” is an arbitrary potentially-non-computable function of n, and not a constant. We instead have to define a different function that behaves the same way as nth for all “valid” inputs and prove that primitive recursive. We can also prove nth itself to be conditionally primitive recursive, conditioned on the inputs being valid (i.e., n < length of the list), but that just creates other unnecessary pain in using that conditional primitive-recursiveness proof.

With nth (or its equivalent) returning the undefined constant on invalid inputs, in contrast, we can Gödel-encode that undefined constant in any Gödel-encodable type, even if we don’t know precisely which value of that type “undefined” actually is, and we can prove that there exists a primitive-recursive function taking a natural number n and the Gödel code of a list and yielding the Gödel code of a list element; we simply arrange for that primitive recursive function to return the Gödel code of “undefined” of the appropriate type, whatever that is (we don’t care) in the case of invalid input arguments. So our inability to prove anything about what the undefined constant is doesn’t get in the way of primitive-recursiveness proofs at all for our purposes; what gets in the way is the fact that “nth n []” for example is not any constant but an undefined function. This is in fact inconsistent with how HOL already treats case statements, and it seems it would at least be better for the semantics to be consistent and “more-defined” in terms of at least producing the undefined constant and not an undefined function for undefined patterns.

I don’t have any objection to making such functions even more defined when appropriate, e.g., the x/0 = 0 example you mentioned. But in the case of the nth function, for example, it’s not clear to me what useful more-distinguished output value we might choose for invalid inputs like “nth n []”, since the list element type is polymorphic and doesn’t necessarily have an obvious distinguished “default” or “zero-like” element. I would personally rather have nth always return some, any, constant in the case of undefined inputs rather than add unnecessary constraints to the list element type (or to the classes of element types for which we could prove it primitive recursive).

Hope this clarifies our motivation for the “undefined constant” wishlist item.

In any case, thanks again for your consideration and feedback.
Bryan

Larry

On 27 Jan 2026, at 17:06, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:

view this post on Zulip Email Gateway (Jan 29 2026 at 23:23):

From: Tjark Weber <tjark.weber@it.uu.se>

Bryan,

On Thu, 2026-01-29 at 17:57 +0000, Bryan Alexander Ford wrote:

Hope this clarifies our motivation for the “undefined constant”
wishlist item.

Your motivation is clear. However, there are multiple approaches to
handling partial functions in HOL, where all functions are inherently
total, and the trade-offs between these approaches have been the
subject of extensive discussion.

Personally, I favor leaving functions as under-specified as possible--
for example, avoiding even proving statements like "nth [] n =
undefined n", let alone "nth [] n = undefined".

By contrast, many users prefer definitions that support stronger,
unconditional theorems. Isabelle's treatment of "x / 0 = 0" is a clear
example.

Compared to that, your request seems relatively harmless, though it is
worth noting that it would still produce "accidental" theorems, such as
"nth [] n = last []".

In any case, defining your own total function that extends nth is a
perfectly reasonable workaround for the time being.

Best,
Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

view this post on Zulip Email Gateway (Jan 30 2026 at 00:11):

From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>

On 30 Jan 2026, at 10:22, Tjark Weber [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

Compared to that, your request seems relatively harmless, though it is
worth noting that it would still produce "accidental" theorems, such as
"nth [] n = last []”.

I would be very much in favour of not being able to prove that. I’m perfectly fine with function completion for totality, but it should be designed not accidental.

Given that you can’t remove the ability to prove this once the primrec package makes it true, but you can explicitly add the ability to prove it if you define your own function, I think it is clear that the current design is the right one, because it gives you the choice.

Cheers,
Gerwin

This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error.

view this post on Zulip Email Gateway (Jan 30 2026 at 07:29):

From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>

Thanks Tjark and Gerwin for your follow-up thoughts.

On 30 Jan 2026, at 01:06, Gerwin Klein <kleing@unsw.edu.au> wrote:

On 30 Jan 2026, at 10:22, Tjark Weber [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

Compared to that, your request seems relatively harmless, though it is
worth noting that it would still produce "accidental" theorems, such as
"nth [] n = last []”.

I would be very much in favour of not being able to prove that. I’m perfectly fine with function completion for totality, but it should be designed not accidental.

I completely understand the desire not to have too many “unwanted” theorems in a formal system. If we were working in ZFC, it would be full of so-called “junk theorems” like ‘2 ∈ 3’; Isabelle’s strong type system already takes us a tremendous distance in minimizing such unwanted theorems. But the long-ago decisions in HOL to (a) make functions total and (b) make reflexivity unconditional means that we can always prove theorems like “undefined = undefined”, which from a “provability minimization” perspective seems like an undesirable junk theorem as well. That horse bolted from the HOL barn decades ago. Is "nth [] n = last []” so much more offensive than “undefined = undefined”?

(Incidentally, if you don’t like "junk theorems" like these, you might be interested in the grounded reasoning system mentioned in the paper I pointed to in my original post, or its early-prototype embodiment in the “Isabelle/GD” (grounded deduction) built by Sascha Kehri (https://bford.info/thesis/2025-kehrli/). In this approach, reflexivity in fact isn’t a blanket assumption, and you actually can’t prove “x = x” for any term x until you first prove that x represents a terminating computation that yields something concrete (e.g., a natural number, and in particular not “bottom”). But I digress…)

The design of any formal system involves a lot of pragmatic tradeoffs, and HOL is far from an exception. The consequence of taking a “provability minimization purist” stance on "nth [] n = last []” is that we cannot prove the “nth” function to be even computable, let alone primitive-recursive, even though it is completely inspired by corresponding computable functions in functional programming tradition (ML, Haskell, etc), and exactly the same definition expressed in exactly the same structural way as ’nth’ is in ML, Haskell, etc., will produce a computable (and even primitive-recursive) function! Isabelle’s ‘primrec’ and ‘fun’ constructs were originally inspired by functional programming tradition; a big part of their appeal is that they make it easy to express functional computations in HOL and then reason about what those computations do; and a ton of effort has even gone into making functions like nth extractable into executable functional-program code again in languages like ML and Haskell! Why go to all this effort to make it easy to express normally-computable functions in normal functional programming fashion in HOL, and to be able to reason about it and even extract executable functional code, but not make those “obviously computable” functions actually provably computable?

All the other ‘fun’ and ‘primrec’ definitions I can think of at the moment in List.thy are provably computable and primitive-recursive. This even includes ‘hd’ and ’tl’, despite their being “undefined” in the empty-list case, simply because “hd []” and “tl []” are constants by virtue of taking no arguments other than the list argument, and there is only one input argument yielding an undefined output. Our recursion theory framework has no trouble with these cases. Yes, “hd []” and “tl []” semantically yield unknown list elements whose values we can prove nothing about, but we can still take their Gödel code in the appropriate type and produce a genuinely (arithmetically, as in definable in Skolem’s PRA) primitive-recursive function that yields that Gödel code, whatever it is, when they get invoked with the empty list. No problem; this undefined behavior is still computably undefined.

But because it takes the additional argument n, the “nth” function is a quite rare exception (although I expect there are a few others hiding elsewhere in HOL’s functional-programming-inspired theories). Despite being “obviously” computable and even primitive recursive by its structural definition, defined using the functional-programming-inspired construct “primrec”, and even fully exportable to genuinely-computable ML/Haskell code, it is not provably even computable due to this particular quirk of Isabelle’s incomplete-pattern-matching semantics. Does a distaste for "nth [] n = last []” truly justify the obviously-computable nth function not being provably computable?

And as I mentioned before, this semantic quirk is already inconsistent with Isabelle/HOL’s semantics for the “case” statement, which already yields the “undefined” constant in incomplete-pattern cases. What is the principled justification of that semantic inconsistency?

Thanks
Bryan

view this post on Zulip Email Gateway (Jan 30 2026 at 08:00):

From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>

P.S. If we really wanted to avoid unwanted theorems like "nth [] n = last []” while also making “obviously-computable” functions like nth provably computable, an alternative would be to make each function defined by ‘fun’ or ‘primrec’ produce a distinct undefined constant, specific to that function, for that function’s undefined cases. Then, “nth [] n” would effectively be equal to some constant symbol like “nth_undefined” but would not be provably equal to the corresponding undefined constant for any other function with incomplete pattern coverage. We would not get "nth [] n = last []” but we would still get “last [] = last []” and “nth [] n = nth [] n”, of course. And from a provability-minimization-purist stance we would still get the arguably-unwanted theorem “nth [] n = nth [] m” even when n != m, but that’s the property we really need in order for the nth function to be provably computable. Tradeoffs.

I still feel however that "nth [] n = last []” is a small price to pay for “nth” being provably computable, and having every incompletely-defined function like nth produce its own undefined constant like “nth_undefined” sounds to me like more trouble than it's worth. Especially when there’s already a standard “undefined” constant that’s already widely-used for other “undefinedy” purposes in HOL (such as what case statements produce when they don’t match a pattern). And especially in comparison to the seemingly much more offensive but pragmatic decision “x/0 = 0” (not even “x/0 = undefined!”) that Larry brought up, a practical-utility compromise that HOL has been living with for a long time now.

Cheers
Bryan

On 30 Jan 2026, at 08:29, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk> wrote:

Thanks Tjark and Gerwin for your follow-up thoughts.

On 30 Jan 2026, at 01:06, Gerwin Klein <kleing@unsw.edu.au> wrote:

On 30 Jan 2026, at 10:22, Tjark Weber [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

Compared to that, your request seems relatively harmless, though it is
worth noting that it would still produce "accidental" theorems, such as
"nth [] n = last []”.

I would be very much in favour of not being able to prove that. I’m perfectly fine with function completion for totality, but it should be designed not accidental.

I completely understand the desire not to have too many “unwanted” theorems in a formal system. If we were working in ZFC, it would be full of so-called “junk theorems” like ‘2 ∈ 3’; Isabelle’s strong type system already takes us a tremendous distance in minimizing such unwanted theorems. But the long-ago decisions in HOL to (a) make functions total and (b) make reflexivity unconditional means that we can always prove theorems like “undefined = undefined”, which from a “provability minimization” perspective seems like an undesirable junk theorem as well. That horse bolted from the HOL barn decades ago. Is "nth [] n = last []” so much more offensive than “undefined = undefined”?

(Incidentally, if you don’t like "junk theorems" like these, you might be interested in the grounded reasoning system mentioned in the paper I pointed to in my original post, or its early-prototype embodiment in the “Isabelle/GD” (grounded deduction) built by Sascha Kehri (https://bford.info/thesis/2025-kehrli/). In this approach, reflexivity in fact isn’t a blanket assumption, and you actually can’t prove “x = x” for any term x until you first prove that x represents a terminating computation that yields something concrete (e.g., a natural number, and in particular not “bottom”). But I digress…)

The design of any formal system involves a lot of pragmatic tradeoffs, and HOL is far from an exception. The consequence of taking a “provability minimization purist” stance on "nth [] n = last []” is that we cannot prove the “nth” function to be even computable, let alone primitive-recursive, even though it is completely inspired by corresponding computable functions in functional programming tradition (ML, Haskell, etc), and exactly the same definition expressed in exactly the same structural way as ’nth’ is in ML, Haskell, etc., will produce a computable (and even primitive-recursive) function! Isabelle’s ‘primrec’ and ‘fun’ constructs were originally inspired by functional programming tradition; a big part of their appeal is that they make it easy to express functional computations in HOL and then reason about what those computations do; and a ton of effort has even gone into making functions like nth extractable into executable functional-program code again in languages like ML and Haskell! Why go to all this effort to make it easy to express normally-computable functions in normal functional programming fashion in HOL, and to be able to reason about it and even extract executable functional code, but not make those “obviously computable” functions actually provably computable?

All the other ‘fun’ and ‘primrec’ definitions I can think of at the moment in List.thy are provably computable and primitive-recursive. This even includes ‘hd’ and ’tl’, despite their being “undefined” in the empty-list case, simply because “hd []” and “tl []” are constants by virtue of taking no arguments other than the list argument, and there is only one input argument yielding an undefined output. Our recursion theory framework has no trouble with these cases. Yes, “hd []” and “tl []” semantically yield unknown list elements whose values we can prove nothing about, but we can still take their Gödel code in the appropriate type and produce a genuinely (arithmetically, as in definable in Skolem’s PRA) primitive-recursive function that yields that Gödel code, whatever it is, when they get invoked with the empty list. No problem; this undefined behavior is still computably undefined.

But because it takes the additional argument n, the “nth” function is a quite rare exception (although I expect there are a few others hiding elsewhere in HOL’s functional-programming-inspired theories). Despite being “obviously” computable and even primitive recursive by its structural definition, defined using the functional-programming-inspired construct “primrec”, and even fully exportable to genuinely-computable ML/Haskell code, it is not provably even computable due to this particular quirk of Isabelle’s incomplete-pattern-matching semantics. Does a distaste for "nth [] n = last []” truly justify the obviously-computable nth function not being provably computable?

And as I mentioned before, this semantic quirk is already inconsistent with Isabelle/HOL’s semantics for the “case” statement, which already yields the “undefined” constant in incomplete-pattern cases. What is the principled justification of that semantic inconsistency?

Thanks
Bryan

view this post on Zulip Email Gateway (Jan 30 2026 at 11:30):

From: Lawrence Paulson <lp15@cam.ac.uk>

This is, in fact, quite a niche request. It's unusual for people to want to prove that functions are computable, especially when applied outside of their actual domain.

Note that if you write your own version of nth, you can easily prove that it coincides with the built-in one on its domain. So if it is automation that concerns you, this would give you easy access to everything already proved about nth.

Larry

On 30 Jan 2026, at 07:59, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk> wrote:

I still feel however that "nth [] n = last []” is a small price to pay for “nth” being provably computable

view this post on Zulip Email Gateway (Jan 30 2026 at 14:20):

From: Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk>

Hi Larry,

On 30 Jan 2026, at 12:29, Lawrence Paulson <lp15@cam.ac.uk> wrote:

This is, in fact, quite a niche request. It's unusual for people to want to prove that functions are computable, especially when applied outside of their actual domain.

Fair enough, but I have to say I’m surprised to hear this position from you in particular, given the support you expressed just earlier in this thread for adding symbols to Isabelle to support the formalization of mathematical logic in HOL. Recursion theory is pretty fundamental to mathematical logic, as I know you’re perhaps more well-aware than almost anyone I can think of, given your own fantastic work formalizing Gödel’s incompleteness theorems in Isabelle/HOL — work I’m a huge fan of and learned so much from, by the way.

Note that if you write your own version of nth, you can easily prove that it coincides with the built-in one on its domain. So if it is automation that concerns you, this would give you easy access to everything already proved about nth.

That’s exactly what we already do — define our own version of “nth” that is actually primitive-recursive and prove the it behaves identically for all the in-domain inputs we care about — and yes of course it works fine. If there’s really no support for making what seem like “obviously" primitive-recursive (or computable) HOL definitions actually provably primitive-recursive (computable), then that’s fine, we’ll just keep the ugly hack.

Thanks for your support for adding the symbols anyway. I already have a partial Isabelle patch for that, which I just need to update and will propose when it’s ready.

Bryan

Larry

On 30 Jan 2026, at 07:59, Bryan Alexander Ford <cl-isabelle-users@lists.cam.ac.uk> wrote:

I still feel however that "nth [] n = last []” is a small price to pay for “nth” being provably computable

view this post on Zulip Email Gateway (Jan 30 2026 at 16:42):

From: "Hughes, John" <john_hughes@brown.edu>

Larry writes: in particular you cannot conclude anything from “f x =
undefined”

This is widely claimed, but it's not exactly true, as the following
example, meant to capture a bit of Bryan's intent w.r.t lists, demonstrates:

theory Scratch
imports Complex_Main
begin

datatype t = Base

fun example:: "('a list) ⇒ t" where
"example [] = undefined"
| "example (x # xs) = Base"

lemma "example [] = example [1::nat]"
using t.exhaust by auto
end

=====
(I.e., you've just proved that "undefined" and "Base" are equal).

One might reasonably say, "OK, sure, if you have a type so impoverished
that it has only one instance, then you CAN prove things about 'undefined',
but that's just stupid."

Then again, if you come from a background in topology, as I do, a
topological space with a single element is right at the heart of the
Eilenberg-Steenrod axioms for homology, so maybe it's stupid, but it's also
pretty important. It's arguably the very first type that you'd want to
define.

In view of this, Bryan might also want to consider what he would want

nth ([]::t list) 7

to evaluate to. If it evaluates to "undefined", then it also evaluates to
"Base", which doesn't seem to match the semantics of "nth".

--John

On Thu, Jan 29, 2026 at 12:57 PM Bryan Alexander Ford <
cl-isabelle-users@lists.cam.ac.uk> wrote:

Thanks Larry for your feedback and support in the suggestions!

On 29 Jan 2026, at 13:19, Lawrence Paulson <lp15@cam.ac.uk> wrote:

Dear Bryan, many thanks for your suggestions. I second the request for
Quine quotes, which are often used in some branches of logic, and I hope
that is a straightforward thing to do. Similarly for the other symbols you
name.

As for “undefined", I'm not sure how difficult it would be to organise
and it's not clear how useful it could be. There is nothing special about
"undefined" and in particular you cannot conclude anything from “f x =
undefined”. instead, we define x/0 = 0, from which we get a lot of
algebraic identities to be unconditional. Lean regards even log as a total
function, with ln(-x) = ln(x), which we have now adopted.

For our purposes, the one useful thing about undefined is that it’s a
constant — meaning anything equal to the “undefined” constant is also at
least equal to anything else equal to the "undefined” constant, even if we
can’t prove anything else about which member of a given type that constant
might be.

Why this matters for us is that if, for example, the nth function in
List.thy returned the “undefined” constant when nth is invoked on an empty
list, then we could prove nth to be primitive-recursive. With Isabelle’s
current semantics, however, we can’t even prove nth to be
primitive-recursive, because “nth n []” is an arbitrary
potentially-non-computable function of n, and not a constant. We instead
have to define a different function that behaves the same way as nth for
all “valid” inputs and prove that primitive recursive. We can also prove
nth itself to be conditionally primitive recursive, conditioned on the
inputs being valid (i.e., n < length of the list), but that just creates
other unnecessary pain in using that conditional primitive-recursiveness
proof.

With nth (or its equivalent) returning the undefined constant on invalid
inputs, in contrast, we can Gödel-encode that undefined constant in any
Gödel-encodable type, even if we don’t know precisely which value of that
type “undefined” actually is, and we can prove that there exists a
primitive-recursive function taking a natural number n and the Gödel code
of a list and yielding the Gödel code of a list element; we simply arrange
for that primitive recursive function to return the Gödel code of
“undefined” of the appropriate type, whatever that is (we don’t care) in
the case of invalid input arguments. So our inability to prove anything
about what the undefined constant is doesn’t get in the way of
primitive-recursiveness proofs at all for our purposes; what gets in the
way is the fact that “nth n []” for example is not any constant but an
undefined function. This is in fact inconsistent with how HOL already
treats case statements, and it seems it would at least be better for the
semantics to be consistent and “more-defined” in terms of at least
producing the undefined constant and not an undefined function for
undefined patterns.

I don’t have any objection to making such functions even more defined when
appropriate, e.g., the x/0 = 0 example you mentioned. But in the case of
the nth function, for example, it’s not clear to me what useful
more-distinguished output value we might choose for invalid inputs like
“nth n []”, since the list element type is polymorphic and doesn’t
necessarily have an obvious distinguished “default” or “zero-like”
element. I would personally rather have nth always return some, any,
constant in the case of undefined inputs rather than add unnecessary
constraints to the list element type (or to the classes of element types
for which we could prove it primitive recursive).

Hope this clarifies our motivation for the “undefined constant” wishlist
item.

In any case, thanks again for your consideration and feedback.
Bryan

Larry

On 27 Jan 2026, at 17:06, Bryan Alexander Ford <
cl-isabelle-users@lists.cam.ac.uk> wrote:

  • A few Unicode symbols not yet supported in Isabelle2025 that would be
    nice to have for mathematical logic purposes:
  • The corners or “Quine quotes” — ⌜ and ⌝ — U+231C and U+231D. Maybe
    nice to add the bottom corners U+231E and U+231F just for
    completeness/symmetry.
  • The negated turnstile symbols ⊬ (U+22AC) “Does Not Prove” and ⊭
    (U+22AD) “Not True”

  • The “Left Tack” symbol ⊣ (U+22A3), which would be nice to have for a
    nontraditional, GA-specific use related to the traditional “proves”
    turnstile but distinct from either that or its negated version.

  • For purposes of proving interesting HOL functions primitive recursive
    (or even computable), it would be nice if the standard “default” semantics
    of undefined cases was uniformly to produce the well-known constant
    “undefined”.

view this post on Zulip Email Gateway (Jan 30 2026 at 17:57):

From: Tjark Weber <tjark.weber@it.uu.se>

John,

On Thu, 2026-01-29 at 13:49 -0500, Hughes, John wrote:
[...] as the following example, meant to capture a bit of Bryan's intent w.r.t lists, demonstrates:

In your example, the culprit is not the definition of the function, but rather the one-element type t. Both "Base" and "undefined" are constants of type t; but this type only has one element, so they must be equal. Consider the following results:

theory Scratch imports Main
begin

datatype t = Base

lemma "Base = undefined"
by (metis (full_types) t.exhaust)

consts example:: "('a list) ⇒ t"

lemma "example [] = example [1]"
by (metis (mono_tags) t.exhaust)

end

I suspect that the name "undefined" is misleading for a constant that is merely unspecified, though that is probably a discussion for another day.

Best,
Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

view this post on Zulip Email Gateway (Jan 30 2026 at 23:26):

From: Gerwin Klein <gerwin.klein@proofcraft.systems>

On 30 Jan 2026, at 18:29, Bryan Alexander Ford <bryan.ford@epfl.ch> wrote:

Thanks Tjark and Gerwin for your follow-up thoughts.

On 30 Jan 2026, at 01:06, Gerwin Klein <kleing@unsw.edu.au> wrote:

On 30 Jan 2026, at 10:22, Tjark Weber [cl-isabelle-users-bounces@lists.cam.ac.uk] <forwarded_for@cse.unsw.edu.au> wrote:

Compared to that, your request seems relatively harmless, though it is
worth noting that it would still produce "accidental" theorems, such as
"nth [] n = last []”.

I would be very much in favour of not being able to prove that. I’m perfectly fine with function completion for totality, but it should be designed not accidental.

I completely understand the desire not to have too many “unwanted” theorems in a formal system. If we were working in ZFC, it would be full of so-called “junk theorems” like ‘2 ∈ 3’; Isabelle’s strong type system already takes us a tremendous distance in minimizing such unwanted theorems. But the long-ago decisions in HOL to (a) make functions total and (b) make reflexivity unconditional means that we can always prove theorems like “undefined = undefined”, which from a “provability minimization” perspective seems like an undesirable junk theorem as well. That horse bolted from the HOL barn decades ago. Is "nth [] n = last []” so much more offensive than “undefined = undefined”?

Yes, of course. I have a proof base with 2 million lines of proof. I want the tool to help me weed out junk, not add unnecessary junk. It’s an engineering question, not a foundational logic question.

The design of any formal system involves a lot of pragmatic tradeoffs, and HOL is far from an exception. The consequence of taking a “provability minimization purist” stance on "nth [] n = last []” is that we cannot prove the “nth” function to be even computable,

In your formal definition and framework of computability. You can always just add assumptions and axioms if you need them instead of asking all of us to accept your additional assumptions that are not needed for what we want to prove. If those additional axioms are unpleasant, why are you asking me to accept them? Asking the function package to add a definition is after all precisely adding a new axiom to a logical system.

All the other ‘fun’ and ‘primrec’ definitions I can think of at the moment in List.thy are provably computable and primitive-recursive.

Looking at List.thy is quite a narrow view of what people do with a prover like Isabelle and for evaluating consequences of proposals like this.

But because it takes the additional argument n, the “nth” function is a quite rare exception (although I expect there are a few others hiding elsewhere in HOL’s functional-programming-inspired theories). Despite being “obviously” computable and even primitive recursive by its structural definition, defined using the functional-programming-inspired construct “primrec”, and even fully exportable to genuinely-computable ML/Haskell code, it is not provably even computable due to this particular quirk of Isabelle’s incomplete-pattern-matching semantics. Does a distaste for "nth [] n = last []” truly justify the obviously-computable nth function not being provably computable?

You misunderstand: I don’t care about nth and last. I care about the thousands of functions that people write in specifications where they might forget a clause and some automatic tool derives an equivalence that will take time to debug and track down when it was never necessary in the first place and would have been immediately obvious in the first proof about that function. It’s not about high-level properties that might become true, this is not a concern in practice. It’s about proofs running into dead ends for no recognisable reason. I have had that latter problem plenty of times, but I have never yet wished for knowing whether a primrec function is computable.

I’m not saying that a framework for computability is not a desirable thing to have (for those who partake), I’m saying applications of provers like Isabelle are wide and diverse and people care about different things. Adding what you ask would prevent one without recourse, while not adding what you ask does still leave you with a number of workarounds.

And as I mentioned before, this semantic quirk is already inconsistent with Isabelle/HOL’s semantics for the “case” statement, which already yields the “undefined” constant in incomplete-pattern cases. What is the principled justification of that semantic inconsistency?

It’s an implementation question. The primrec/fun packages derive new definitions from user specifications, so they can leave out equations when they do that. case statements are themselves functions that are applied, not something for which a new definition is generated each time. Maybe with a bit more work the default case of case x could be undefined x instead of undefined. I would welcome that change (as I would getting a warning for forgetting case clauses, which is probably harder to do).

Cheers,
Gerwin

Last updated: Jan 31 2026 at 12:53 UTC