Proving in Hilbert System

Stream: new members

[Moti Ben-Ari]

I want to start learning Lean by verifying proofs in my textbook Mathematical Logic for Computer Science. A Hilbert system starts with three axioms and MP as the inference rule. The first theorem (3.10 in the book) is p -> p [how do I get the arrow? p \to p doesn't work either!]. The theorem is proved from axioms p -> (q->p) and ((p->(q->r)->((p->q)->(p->r)). How do I specify an axiom?

I want to use this for educational purposes so I don't want to depend on the Lean libraries.

[Kyle Miller]

One problem with doing something so basic is that these axioms are all theorems in Lean using only its built-in axioms

-- \to gives →

example (p : Prop) : p → p := fun x => x
example (p q : Prop) : p → (q → p) := fun x y => x
example (p q r : Prop) : (p → (q → r)) → ((p → q) → (p → r)) := fun x y z => x z (y z)

Maybe it would make sense to make your own arrow so that you're sure you avoid Lean's axioms.

[Kyle Miller]

Here:

axiom imp : Prop → Prop → Prop
infix:40 " ⇒ " => imp -- \=>

axiom mp : (p q : Prop) → (p ⇒ q) → p → q
axiom ax1 : (p q : Prop) → p ⇒ (q ⇒ p)
axiom ax2 : (p q r : Prop) → (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r))

example (p : Prop) : p ⇒ p := sorry

[Martin Dvořák]

I was just doing the same thing:
https://github.com/madvorak/fecssk/blob/76f4e7dfa13ecc7fab5ef348d798480e216add4f/Fecssk/Class06.lean#L91

[Martin Dvořák]

Your @Kyle Miller observation about arrows is smart. I was less careful in my implementation.

[Martin Dvořák]

Also, how can I use the ¬ symbol after prelude (without importing its meaning)?

[Martin Dvořák]

What does axiom imp exactly do in your @Kyle Miller code?

[Martin Dvořák]

I think I could define ¬ similarly to => that you have on the second line.

[Kyle Miller]

Martin Dvořák said:

What does axiom imp exactly do in your Kyle Miller code?

It says that there exists some binary operator on Prop called imp (notice it has the same type as fun p q => (p -> q))

[Kyle Miller]

You can override the notation using high priority:

axiom myNot : Prop → Prop
notation:max (priority := high) "¬" p:40 => myNot p

[Martin Dvořák]

Kyle Miller said:

Martin Dvořák said:

What does axiom imp exactly do in your Kyle Miller code?

It says that there exists some binary operator on Prop called imp (notice it has the same type as fun p q => (p -> q))

How is it different from variable of the same type?

[Kyle Miller]

variable adds a new argument to new definitions/theorems. axiom adds a new definition without any sort of proof of existence.

[Kyle Miller]

axiom is sort of like a variable that the whole theory takes (but there's no mechanism to pass in values of that variable, short of replacing the axiom with a definition)

[Martin Dvořák]

Ah makes sense. I was confused by seeing axiom used for two different purposes.

[Martin Dvořák]

May I copy your @Kyle Miller code into my repository?

[Kyle Miller]

Sure

[Martin Dvořák]

Thanks!

[Moti Ben-Ari]

Martin Dvořák said:

I was just doing the same thing:
https://github.com/madvorak/fecssk/blob/76f4e7dfa13ecc7fab5ef348d798480e216add4f/Fecssk/Class06.lean#L91

Thanks, Martin, I'll look at this.

[Martin Dvořák]

FYI, I am refactoring it right now.

[Martin Dvořák]

Martin Dvořák said:

Ah makes sense. I was confused by seeing axiom used for two different purposes.

Actually three...

• axiom as a symbol
• axiom as a rule of inference
• axiom as an axiom

[Martin Dvořák]

Kyle Miller said:

Here

Well...

axiom _imp : Prop → Prop → Prop
infix:40 " ⇒ " => _imp

axiom MP {φ ψ : Prop} : φ → (φ ⇒ ψ) → ψ
axiom K (φ ψ : Prop) : φ ⇒ (ψ ⇒ φ)
axiom S (φ ψ χ : Prop) : (φ ⇒ (ψ ⇒ χ)) ⇒ ((φ ⇒ ψ) ⇒ (φ ⇒ χ))

example (a b : Prop) :=
  have h1 := K a (b → a)
  have h2 := S a (b → a) a
  have h3 := MP h1 h2
  have h4 := K a b
  show a ⇒ a
        from MP h4 h3

I got a weird error:

application type mismatch
  MP h4 h3
argument
  h3
has type
  (a ⇒ (b → a)) ⇒ (a ⇒ a) : Prop
but is expected to have type
  (a ⇒ (b ⇒ a)) ⇒ (a ⇒ a) : Prop

[Ruben Van de Velde]

Note that the second arrow is different

[Martin Dvořák]

You have very sharp eyes!

[Ruben Van de Velde]

(I'm not sure I'd use Prop at all)

[Ruben Van de Velde]

Martin Dvořák said:

You have very sharp eyes!

Big screen :)

[Martin Dvořák]

Ruben Van de Velde said:

(I'm not sure I'd use Prop at all)

Would you write axiom Propo then?

[Martin Dvořák]

Ruben Van de Velde said:

Note that the second arrow is different

Ah, I kept the "wrong" arrow in the first two instantiations of the axioms.

[Martin Dvořák]

Moti Ben-Ari said:

Thanks, Martin, I'll look at this.

Have a look now:
https://github.com/madvorak/fecssk/blob/3fce703425c30539fb06c791a3a976fbcf34fb84/Fecssk/Class06.lean#L93
Also, I included some example proofs.

[Martin Dvořák]

Or rather now:
https://github.com/madvorak/fecssk/blob/40467a80dc045a4bce0380143231e7d5f0d2ea09/Fecssk/Class06.lean#L95

[Kyle Miller]

Ruben Van de Velde said:

(I'm not sure I'd use Prop at all)

You can try this exercise and see why I left it as Prop, unless you mean you'd use Type. Or maybe you'd use a type with a CoeType instance?

[Ruben Van de Velde]

I haven't thought about it; just noting the risk of using the wrong arrows, for example