notation problems

Stream: new members

[Michael Beeson]

Here is a minimal non-working example. I can't get it to parse. What am I doing wrong?

set_option default_priority 100
reserve infix ` ∈ ` : 49
reserve infix ` <ℕ `: 49
reserve infix ` ⊕ ` : 60  --addition on Church numbers

class Model (M : Type) :=
(mem : M → M → Prop)
(ℕℕ:M)      -- Church numbers
(lessthanN: M → M → Prop)
(ChurchZero:M)  --Church zero
(ChurchAddition: M → M → M)
(notation: `𝟘`:= ChurchZero)
(infix  ∈ :=  mem)
(infix <ℕ := lessthanN)
(infix ⊕:= ChurchAddition)
(S:M → M)  --Church successor
(N_members: ∀ (x:M), (x ∈ ℕℕ ↔ ∀ w,(ChurchZero ∈ w ∧ ∀ u, (u ∈ w →S u ∈ w)) → x ∈ w))
(ChurchOrder: ∀ (x y:M), x <ℕ y ↔ ∃ (n:M), n ∈ ℕℕ ∧ x ⊕ S n = y)

variables {M : Type} [Model M] (a b x y z: M)
open Model

lemma isssuccessor: ∀ (x y:M), x ∈ ℕℕ → y ∈ ℕℕ → x <ℕ y → ∃(z:M), z ∈ ℕℕ ∧ y = S z:=
  assume x y,
  begin
    intros hx hy h3,
    have h4:= ChurchOrder x y,
    rw h4 at h3,

  end

[Yakov Pechersky]

set_option default_priority 100
reserve infix ` ∈ ` : 49
reserve infix ` <ℕ `: 49
reserve infix ` ⊕ ` : 60  --addition on Church numbers

class Model (M : Type) :=
(mem : M → M → Prop)
(ℕℕ:M)      -- Church numbers
(lessthanN: M → M → Prop)
(ChurchZero:M)  --Church zero
(ChurchAddition: M → M → M)
(notation: `𝟘`:= ChurchZero)
(infix  ∈ :=  mem)
(infix <ℕ := lessthanN)
(infix ⊕:= ChurchAddition)
(S:M → M)  --Church successor
(N_members: ∀ (x:M), (x ∈ ℕℕ ↔ ∀ w,(ChurchZero ∈ w ∧ ∀ u, (u ∈ w →S u ∈ w)) → x ∈ w))
(ChurchOrder: ∀ (x y:M), x <ℕ y ↔ ∃ (n:M), n ∈ ℕℕ ∧ x ⊕ S n = y)

variables {M : Type} [Model M] (a b x y z: M)
open Model

local infix  ∈ := mem
local infix <ℕ := lessthanN

lemma isssuccessor: ∀ (x y:M), x ∈ ℕℕ → y ∈ ℕℕ → x <ℕ y → ∃(z:M), z ∈ ℕℕ ∧ y = S z:=
  assume x y,
  begin
    intros hx hy h3,
    have h4:= ChurchOrder x y,
    rw h4 at h3,

  end

[Yakov Pechersky]

I think you have to redeclare the notation

[Eric Wieser]

I'm curious @Michael Beeson - do you ever declare instance : Model T := sorry? If so, for what T?

[Michael Beeson]

Well, that worked, both in the MWE and in my project, so thanks. I was mystified at first as in my project, as opposed to the example,
I did already have redeclarations. But AHA! there was a one-letter typo in those redeclarations and the typo was still a legal reference to
some other member...so in reality my problem was a typo in the redeclarations... Thanks for helping me.

[Michael Beeson]

To answer Eric, no, I never declare an instance. I just work inside the class. The idea is that class Model represents a model of the
first-order theory I am studying, so my proofs are proofs from the axioms of that theory, which are members of class Model.

[Eric Wieser]

I guess my question then would be whether it is better to use class or just axiom - I guess the advantage of your approach is that you never end up with contradictory axioms, only contradictory "axiom" hypotheses

[Eric Wieser]

But if you never instantiate Model, then you are never proving that its axioms are not contradictory

[Eric Wieser]

Here's a proof that Model isn't contradictory:

inductive model_example
| NN
| Zero

namespace model_example

instance : Model model_example :=
{ mem := λ x y, x = Zero ∧ y = NN,
  ℕℕ := NN,
  ChurchZero := Zero,
  ChurchAddition := λ _ _, Zero,
  S := id,
  N_members := λ x, begin cases x; simp end,
  -- this means "define lessthanN such that this is true by definition"
  lessthanN := _,
  ChurchOrder := λ x y, iff.rfl }

end model_example

This perhaps indicates that your axioms aren't complete enough to capture what you want - in particular, you don't require that succ n and n are distinct.

[Mario Carneiro]

I assume it's been minimized

[Michael Beeson]

Eric Wieser said, if you never instantiate Model, then you are never proving its axioms are not contradictory. Indeed--in my case, the axioms are those of Quine's NF set theory, and it is a 90-year-old open problem whether they are contradictory or not! I have no idea how to settle that problem, so it's a good thing I don't try to instantiate my class.

[Michael Beeson]

New question about notation. I have a partial order that depends on a parameter. So there will be THREE arguments, a parameter n
and the two items x and y to be compared. In normal math I suppress mention of the parameter. If I had to write it I would make it a subscript to the order symbol, like x \prec_n y. I suppose there's no hope of getting Lean to use notation like that. I will have to write it out longhand as prec n x y I guess. Right?

[Eric Wieser]

There's no hope of getting lean to hand a subscript, but notation x `\prec[` n `]` y := prec n x y should work

[Mario Carneiro]

those of Quine's NF set theory, and it is a 90-year-old open problem whether they are contradictory or not!

Actually, NF was proved to be consistent around 2015, IIRC

[Mario Carneiro]

Hm, I remember this from the news of the time, but looking it up now it seems like there was a proof in 2015 whose status is somewhat unclear

[Michael Beeson]

Randall Holmes submitted a proof of the consistency of NF to a well-known journal. The editor-in-chief of that journal said that because of the importance of the theorem, he would have to referee it himself. That was at least four years ago and no verdict has yet been issued.

[Mario Carneiro]

It appears that Randall Holmes is also not satisfied with the situation. https://randall-holmes.github.io/Nfproof/newattempt.pdf discusses the status of the proof in the introduction