## Stream: maths

### Topic: proofs in cocalc

#### Jane (Feb 29 2020 at 00:38):

Hey guys, can someone please help me with two problem using some of the axioms?

def has_min_element {A : Type} (R : A → A → Prop) : Prop :=
∃ x, ∀ y, R x y
axiom ax1 {n m: ℕ} : (n ≤ m) ↔ (∃ l : ℕ, n + l = m)
axiom ax2 {m n x y: ℕ} (h1 : x + n = y) (h2 : y + m = x): x = y ∧ (m = 0) ∧ (n = 0)
axiom ax3 {m n x y z : ℕ} (h1 : x + n = y) (h2 : y + m = z) : x + (n + m) = z
axiom ax4 : 1 ≠ 2
axiom ax5 (m n : ℕ) : ∃ l : ℕ, m + l = n ∨ n + l = m
axiom ax6 (n : ℕ) : 0 + n = n

theorem le_not_symmetric : ¬ (symmetric nat.less_than_or_equal) :=
sorry

example : ¬ (equivalence nat.less_than_or_equal) :=
sorry


Thank you guys soooo much !!!

#### Anne Baanen (Mar 02 2020 at 10:24):

To get started, it's good to realize ¬ p is the same as p → false, and x ≠ y is the same as ¬ (x = y), which is the same as (x = y) → false.

#### Kevin Buzzard (Mar 02 2020 at 10:33):

A lot of these axioms are things which one can prove in Lean anyway. Here's an axiom-free proof of the first one:

theorem le_not_symmetric : ¬ (symmetric nat.less_than_or_equal) :=
begin
intro h, -- proof by "mathematician's contradiction", i.e. assume it's symmetric
-- and get a contradiction
unfold symmetric at h, -- says x ≤ y → y ≤ x
have h12 : 1 ≤ 2 := dec_trivial,
have h21 : ¬ 2 ≤ 1 := dec_trivial,
apply h21,
apply h,
exact h12,
end


but it's hard to work out if this is what you're looking for.

Last updated: May 19 2021 at 02:10 UTC