definitions are not proved - risks? (inconsistency)

Stream: new members

[rzeta0]

Lemmas/theorems are proved.

Definitions are asserted, not proved.

What are the ways in which creating definitions can go wrong?

I'm no expert by my own beginner thinking suggests:

• definitions which contradict known axioms or theorems proven from those axioms
• definitions which don't contradict current axioms but contradict each other

[Ilmārs Cīrulis]

Definitions are not asserted, they are just names to things, imo.
It is impossible to name things in such way that the names 'contradict' theorems or axioms.

The biggest risk is to have names for worthless things.

(My 2 cents)

[Daniel Weber]

I believe the main problem is that the formalized definition may not match up with the actual mathematical content - as an extreme example, one can define

def GoldbachConjecture : Prop := 1 + 1 = 2

theorem goldbach : GoldbachConjecture := rfl

This is obviously an invalid formalization, but there can be examples which are much more subtly off.

This is a problem which can't really be resolved, but in general a good way to avoid this is to prove a bunch of things about your definitions — if it satisfies all of the properties it should, that lowers the chances it's the wrong thing

[Dan Velleman]

A definition can go wrong if what comes after := has the wrong type. For example,

def f (a b : Nat) : Nat := a = b

produces the error message

type mismatch
  a = b
has type
  Prop : Type
but is expected to have type
  ℕ : Type

[Dan Velleman]

This is similar to what can go wrong with an incorrect proof. For example, here is a correct proof:

example (a b : Nat) : a + b = b + a := Nat.add_comm a b

But if you change it to

example (a b : Nat) : a + b = b + a := Nat.add_comm b a

then you get the error message

type mismatch
  Nat.add_comm b a
has type
  b + a = a + b : Prop
but is expected to have type
  a + b = b + a : Prop