Stream: General

Topic: Surprising definitions of True and False.

Alex Weisberger (Sep 23 2023 at 01:01):

I looked up the definitions of True and False, and they're very surprising to me. For reference:

definition True :: bool
  where "True ≡ ((λx::bool. x) = (λx. x))"

definition False :: bool
  where "False ≡ (∀P. P)"

One the one hand, they make sense, because their values are literally true and false respectively - the lambda terms in the True definition are equivalent, and all propositions are not true, so ∀P. P is false.

However, I always assumed True and False would just be defined as a datatype with two constructors. Why are they defined this way?

Yong Kiam (Sep 23 2023 at 05:03):

I suspect one (part of) the answer is that logical connectives are defined in HOL before any kind of datatypes (which are not primitive in the logic)

Mathias Fleury (Sep 23 2023 at 05:51):

And let me destroy your world a second time: nat is also axiomatized and not a datatype

Mathias Fleury (Sep 23 2023 at 05:51):

You need nats and termination to even express that datatypes are well formed

Wolfgang Jeltsch (Sep 23 2023 at 12:28):

Mathias Fleury said:

You need nats and termination to even express that datatypes are well formed

Ah, that’s the reason. I already saw in the past that nat isn’t defined via datatype but somehow thought that this was a leftover from a time when the new datatype package didn’t yet exist.

Well, let’s go on: prod also isn’t defined via datatype, right? Why is this?

Alex Weisberger (Sep 24 2023 at 13:53):

I also didn't realize that about nat. I guess things get complicated down at the level of the foundations of the logic :D

Jan van Brügge (Sep 25 2023 at 08:36):

prod also isn’t defined via datatype, right? Why is this?

prod and sum are used to define datatypes, if you specify for example datatype 'a foo = Bar | Foo 'a | Both 'a "'a foo" the datatype package internally works with the type unit + 'a + 'a * 'b, proves that it is a functor in 'a and 'b, constructs a suitable algebra and creates the datatype as a fixpoint of the functor (removing 'b and replacing it with recursion)

Jan van Brügge (Sep 25 2023 at 08:37):

There a bunch of base functors that the functor proof uses, namely sum, prod, 'a => 'b, identity and constant (both are not their own types, just different theorems)

Jan van Brügge (Sep 25 2023 at 08:38):

You can see them in src/HOL/Basic_BNFs.thy

Jonathan Julian Huerta y Munive (Sep 25 2023 at 08:46):

@Alex Weisberger that definition looks more intuitive to me as a mathematics degree holder. Every field of mathematics can be represented as a set of assumptions and their logical consequences. To construct all of mathematics, I was taught ZFC but Isabelle's HOL axiom system is nicely presented in Kuncar and Popescu's A Consistent Foundation for Isabelle/HOL. From those axioms you can model datatypes, sums, products, and all those things programmers know. Isabelle has automated machinery to make each new declaration of these entities consistent/within its HOL foundation.

Last updated: Dec 21 2024 at 12:33 UTC