[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings
From: |
Martin Baker |
Subject: |
Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings |
Date: |
Tue, 25 Jun 2019 22:51:27 +0100 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.7.2 |
On 6/25/19, William Sit<address@hidden> wrote:
> The expression x = x + 0, whether treated as a type or an equation,
> can only make sense when x, =, + and 0 are clearly typed and defined.
> It makes little sense to me that this, as an equation, can be "proved"
> to be valid universally (that is, without the definition of, say +).
If x is a natural number defined like this in Coq:
Inductive nat : Set := O : nat | S : nat -> nat
then x = x + 0 is not an axiom but is derivable.
Of course this all depends on the structures and definitions, I didn't
mean to imply that it is valid universally.
On 25/06/2019 19:28, Tim Daly wrote:
The "elegant way" that Martin is questioning is the problem
of combining a certain kind of logic operation (refl aka
"reflection" where both sides are equal) with the notion of
a mathematical unit.
I think that refl (short for "reflexivity" of = relation), is the usual
abbreviation for the only constructor of an equality type in Martin-Lof
type theory.
I get the impression that this theory is very powerful in proof
assistants and I am questioning if you proposing to build this into
Axiom and how?
Martin
- [Axiom-developer] Axiom's Sane redesign musings, Tim Daly, 2019/06/19
- Re: [Axiom-developer] Axiom's Sane redesign musings, Martin Baker, 2019/06/19
- Re: [Axiom-developer] Axiom's Sane redesign musings, Tim Daly, 2019/06/19
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, William Sit, 2019/06/25
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Tim Daly, 2019/06/25
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings,
Martin Baker <=
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Tim Daly, 2019/06/25
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Martin Baker, 2019/06/26
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Tim Daly, 2019/06/26
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Tim Daly, 2019/06/27
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Tim Daly, 2019/06/29
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Martin Baker, 2019/06/30
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Tim Daly, 2019/06/30
- Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings, Clifford Yapp, 2019/06/30