On 6/25/19, William Sit<w...@ccny.cuny.edu> 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 mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
