[Top][All Lists]

[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?


reply via email to

[Prev in Thread] Current Thread [Next in Thread]