help in question

Stream: new members

[Michelle Ioshpe]

hi. i'm new to lean and i don't understand how to solve this question. i would appreciate if someone could solve me theorm d based on all the imformation given in the pictures i uploaded. (i tried writing something in d but as you can see its not correct)
image.png
image.png

[Ruben Van de Velde]

Please share the code using #backticks , not as a screenshot. We can help much more easily when we can run the code ourselves and see the error you're seeing

[Michelle Ioshpe]

namespace Exercise5

variable (φ ψ μ : Prop)

/-

In this excersice you will proof some propositions

using axioms of abstract propositional calculus,

in this exercise usage of any tactics and "fun" is

forbidden, you only can use axioms defined below

(actually as you learned in class MP hp hpq can be just written as hpq hp, but we wanted to empathise

usage of axioms, so write MP hp hpq)
-/

axiom A1 (ψ φ : Prop) : (ψ → (φ → ψ))

axiom A2 (ψ φ μ: Prop) : ((φ→(ψ→μ)))→((φ→ψ)→(φ→μ))

axiom A3 (ψ φ: Prop) : ((¬ψ)→(¬φ))→(((¬ψ)→ φ)→ψ)

def MP {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp

/-

Here to proving something we will use "theorem" instead of "example" that you've learned in class. The

essential difference is that theorem has name, and it can be used again, as you will see in example below.

It's syntaxis is the following:

theorem "name of theorem" : "statement that you are going to proof" := "proof"
-/

/-

Here are two proofs of φ→φ, first (that is labeled t5) is divided into series of intermediate theorems corresponding to steps

that you've done in class to show this fact. And the second is essentially the same but in one line.
-/

/-

first
-/

theorem t1 : ((φ→((φ→φ)→φ)))→((φ→(φ→φ))→(φ→φ)) :=

A2 (φ→φ) φ φ

theorem t2  : (φ → ((φ→φ)→ φ)) :=

A1 φ (φ→φ)

theorem t3 : ((φ→(φ→φ))→(φ→φ)) :=

MP (t2 φ) (t1 φ)

theorem t4 : (φ→(φ→φ)) :=

A1 φ φ

theorem t5 : (φ→φ) :=

MP (t4 φ) (t3 φ)

/-

second
-/

theorem t : (φ→φ) :=

MP ((A1 φ φ)) (MP (A1 φ (φ→φ)) (A2 (φ→φ) φ φ))

/-

Now, proving these expressions, you can define some intermidiate

theorem to make proof more readable. You have to replace sorry with

an actual proof
-/

theorem a : ((¬φ→φ)→φ):= MP (t ¬φ) (A3 φ φ)

/-

In exercises b,с  you have additional assumptions that you can use, here you unfortunately forced

to write everything in one line, because theorem does not allow to use assumption outside of a theorem.
-/

theorem b (h1 : φ→ψ) (h2:ψ→μ) :  (φ → μ):= MP h1 (MP (MP h2 (A1 (ψ → μ) φ)) (A2 ψ φ μ))

theorem c (h1 : φ → (ψ → μ)): (ψ → (φ → μ)):= b ψ (φ → ψ) (φ → μ) (A1 ψ φ) (MP h1 (A2 ψ φ μ))

theorem d :(¬ψ→¬φ)→(φ→ψ):= MP (A3 ψ φ) (A2 (¬ψ → ¬φ) (A1 φ (¬ψ)))

/-b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (c (A2 ψ φ))-/

/-b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (MP ((¬ψ) → φ) (A3 ψ φ))   -gives φ→ψ -/

/- b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (c (A2 ψ φ φ))- gp-/

/-A3 ψ φ-/

end Exercise5

[Michelle Ioshpe]

i hope i understood you right

[Notification Bot]

This topic was moved here from #general > help in question by Eric Wieser.

[Ruben Van de Velde]

Please do read #backticks - it's a link

[Michelle Ioshpe]

namespace Exercise5
variable (φ ψ μ : Prop)

axiom A1 (ψ φ : Prop) : (ψ → (φ → ψ))
axiom A2 (ψ φ μ: Prop) : ((φ→(ψ→μ)))→((φ→ψ)→(φ→μ))
axiom A3 (ψ φ: Prop) : ((¬ψ)→(¬φ))→(((¬ψ)→ φ)→ψ)
def MP {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp

/-
theorem "name of theorem" : "statement that you are going to proof" := "proof"
-/

theorem t : (φ→φ) :=
  MP ((A1 φ φ)) (MP (A1 φ (φ→φ)) (A2 (φ→φ) φ φ))

  /-
Now, proving these expressions, you can define some intermidiate
theorem to make proof more readable. You have to replace sorry with
an actual proof
-/

theorem a : ((¬φ→φ)→φ):= MP (t ¬φ) (A3 φ φ)

/-
In exercises b,с  you have additional assumptions that you can use, here you unfortunately forced
to write everything in one line, because theorem does not allow to use assumption outside of a theorem.
-/
theorem b (h1 : φ→ψ) (h2:ψ→μ) :  (φ → μ):= MP h1 (MP (MP h2 (A1 (ψ → μ) φ)) (A2 ψ φ μ))

theorem c (h1 : φ → (ψ → μ)): (ψ → (φ → μ)):= b ψ (φ → ψ) (φ → μ) (A1 ψ φ) (MP h1 (A2 ψ φ μ))

theorem d :(¬ψ→¬φ)→(φ→ψ):= MP (A3 ψ φ) (A2 (¬ψ → ¬φ) (A1 φ (¬ψ)))
/-b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (c (A2 ψ φ))-/
/-b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (MP ((¬ψ) → φ) (A3 ψ φ))   -gives φ→ψ -/
/- b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (c (A2 ψ φ φ))-/
/-A3 ψ φ-/


end Exercise5

[Michelle Ioshpe]

theorem d is not correct

[Aaron Liu]

What's your informal argument?

[Michelle Ioshpe]

i have no idea... it is all the information my teacher gave me
sorry i am new to this

[Michelle Ioshpe]

if it helps here is everithing including comments:

[Michelle Ioshpe]

namespace Exercise5

variable (φ ψ μ : Prop)

/-

In this excersice you will proof some propositions

using axioms of abstract propositional calculus,

in this exercise usage of any tactics and "fun" is

forbidden, you only can use axioms defined below

(actually as you learned in class MP hp hpq can be just written as hpq hp, but we wanted to empathise

usage of axioms, so write MP hp hpq)
-/

axiom A1 (ψ φ : Prop) : (ψ → (φ → ψ))

axiom A2 (ψ φ μ: Prop) : ((φ→(ψ→μ)))→((φ→ψ)→(φ→μ))

axiom A3 (ψ φ: Prop) : ((¬ψ)→(¬φ))→(((¬ψ)→ φ)→ψ)

def MP {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp

/-

Here to proving something we will use "theorem" instead of "example" that you've learned in class. The

essential difference is that theorem has name, and it can be used again, as you will see in example below.

It's syntaxis is the following:

theorem "name of theorem" : "statement that you are going to proof" := "proof"
-/

/-

Here are two proofs of φ→φ, first (that is labeled t5) is divided into series of intermediate theorems corresponding to steps

that you've done in class to show this fact. And the second is essentially the same but in one line.
-/

/-

first
-/

theorem t1 : ((φ→((φ→φ)→φ)))→((φ→(φ→φ))→(φ→φ)) :=

  A2 (φ→φ) φ φ

theorem t2  : (φ → ((φ→φ)→ φ)) :=

  A1 φ (φ→φ)

theorem t3 : ((φ→(φ→φ))→(φ→φ)) :=

  MP (t2 φ) (t1 φ)

theorem t4 : (φ→(φ→φ)) :=

  A1 φ φ

theorem t5 : (φ→φ) :=

  MP (t4 φ) (t3 φ)

/-

second
-/

theorem t : (φ→φ) :=

  MP ((A1 φ φ)) (MP (A1 φ (φ→φ)) (A2 (φ→φ) φ φ))

  /-

Now, proving these expressions, you can define some intermidiate

theorem to make proof more readable. You have to replace sorry with

an actual proof
-/

theorem a : ((¬φ→φ)→φ):= MP (t ¬φ) (A3 φ φ)

/-

In exercises b,с  you have additional assumptions that you can use, here you unfortunately forced

to write everything in one line, because theorem does not allow to use assumption outside of a theorem.
-/

theorem b (h1 : φ→ψ) (h2:ψ→μ) :  (φ → μ):= MP h1 (MP (MP h2 (A1 (ψ → μ) φ)) (A2 ψ φ μ))

theorem c (h1 : φ → (ψ → μ)): (ψ → (φ → μ)):= b ψ (φ → ψ) (φ → μ) (A1 ψ φ) (MP h1 (A2 ψ φ μ))

theorem d :(¬ψ→¬φ)→(φ→ψ):= MP (A3 ψ φ) (A2 (¬ψ → ¬φ) φ ψ (A1 φ ¬ψ))

/-b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (c (A2 ψ φ))-/

/-b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (MP ((¬ψ) → φ) (A3 ψ φ))   -gives φ→ψ -/

/- b φ ((¬ψ) → φ) ψ (A1 φ (¬ψ)) (c (A2 ψ φ φ))- gp-/

/-A3 ψ φ-/

end Exercise5

[Arthur Paulino]

I'm not sure the community will be able to help you if you don't come up with informal proofs ("with pen and paper"). But if you do and you're finding it difficult to translate your reasoning to Lean, I'm sure ppl will happily help you

[Isak Colboubrani]

@Michelle Ioshpe Are you specifically referring to proving theorem d (the others are already proven?)? Keep in mind it’s unlikely anyone will simply hand you the complete solution, but if you show genuine effort and a willingness to learn, we might be able to guide you in the right direction.

[Ilmārs Cīrulis]

Wlerg, I hate those matematical logic exercises. :sweat_smile: I will try to solve the d and then probably drop some hints or smth. Wish me luck.

[Ilmārs Cīrulis]

Can you prove d in an easier form (aux)?

And were you taught about deduction theorem which looks smth like this:
[A1, A2, A3, MP] |- p -> q iff [A1, A2, A3, MP, p] |- q

import Mathlib

namespace Exercise5

variable (φ ψ μ : Prop)

axiom A1 (ψ φ : Prop) : (ψ → (φ → ψ))

axiom A2 (ψ φ μ: Prop) : ((φ→(ψ→μ)))→((φ→ψ)→(φ→μ))

axiom A3 (ψ φ: Prop) : ((¬ψ)→(¬φ))→(((¬ψ)→ φ)→ψ)

def MP {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp

theorem b (h1 : φ→ψ) (h2:ψ→μ) :  (φ → μ):= MP h1 (MP (MP h2 (A1 (ψ → μ) φ)) (A2 ψ φ μ))

theorem c (h1 : φ → (ψ → μ)): (ψ → (φ → μ)):= b ψ (φ → ψ) (φ → μ) (A1 ψ φ) (MP h1 (A2 ψ φ μ))

theorem aux (p q: Prop) (H1: ¬ p → ¬ q) (H2: q): p := sorry

[Ilmārs Cīrulis]

I hope I make sense. I had mathematical logic course and similar exercises eons ago.

[Ilmārs Cīrulis]

namespace Exercise5

axiom A1 (ψ φ : Prop) : (ψ → (φ → ψ))

axiom A2 (ψ φ μ : Prop) : ((φ → (ψ → μ))) → ((φ → ψ) → (φ → μ))

axiom A3 (ψ φ : Prop) : ((¬ ψ) → (¬ φ)) → (((¬ ψ) → φ) → ψ)

def MP {p q : Prop} (hp : p) (hpq : p → q) : q := hpq hp

theorem t (ψ : Prop): (ψ → ψ) := MP ((A1 ψ ψ)) (MP (A1 ψ (ψ → ψ)) (A2 (ψ → ψ) ψ ψ))

theorem b {ψ φ μ : Prop} (h1 : φ → ψ) (h2 : ψ → μ) : (φ → μ) := MP h1 (MP (MP h2 (A1 (ψ → μ) φ)) (A2 ψ φ μ))

theorem c {ψ φ μ : Prop} (h1 : φ → (ψ → μ)): (ψ → (φ → μ)) := b (A1 ψ φ) (MP h1 (A2 ψ φ μ))


section Example

theorem b' (p q r: Prop) (H1: p → q) (H2: q → r) (H3: p): r := by
  have step1: p := H3
  have step2: q → r := H2
  have step3: p → q := H1
  have step4: q := MP step1 step3
  have step5: r := MP step4 step2
  exact step5

theorem b'' (p q r: Prop) (H1: p → q) (H2: q → r): p → r := by
  have step1: p → p := t p
  have step2: p → (q → r) := MP H2 (A1 (q → r) p)
  have step3: p → (p → q) := MP H1 (A1 (p → q) p)
  have step4: p → q := MP step1 (MP step3 (A2 _ _ _)) ---- of course, the H1 is more simple
  have step5: p → r := MP step4 (MP step2 (A2 _ _ _))
  exact step5

theorem b''' (p q r: Prop) (H1: p → q) (H2: q → r): p → r := by
  have step1: p → q → r := MP H2 (A1 (q → r) p)
  have step2: p → r := MP H1 (MP step1 (A2 q p r))
  exact step2

theorem b'''' (p q r: Prop) (H1: p → q) (H2: q → r): p → r := MP H1 (MP (MP H2 (A1 (q → r) p)) (A2 q p r))

end Example

end Exercise5

Are such solutions as in section Example --- using have to store intermediate results --- allowed?

[Michelle Ioshpe]

no, unfortunately i am supposed to do it in one line, like a,b,c
and i am not allowed to use "have".
But thank you very much i really appreciate the help, i will try more and maybe your solution will help me to understand

[Ilmārs Cīrulis]

You can transform proofs that are written using have into one line proofs, when they are finished.

[Ilmārs Cīrulis]

Anyway, I proved
theorem aux (p q: Prop) (H1: ¬ p → ¬ q) (H2: q): p := by sorry

Then cheated by looking at the proof of deduction theorem and proved:
theorem aux' (p q: Prop) (H1: ¬ p → ¬ q): q → p := by sorry

Simplified a bit as I saw a step that can be proved in more simple way.
theorem aux'' (p q: Prop) (H1: ¬ p → ¬ q): q → p := by sorry

Then again following deduction theorem:
theorem aux''' (p q: Prop): (¬ p → ¬ q) → (q → p) := by sorry

Got 11 steps with have, then transformed this proof to one line proof (manually). So... that can be done.

But probably I should take a better look and try to get some direct proof.

[Ilmārs Cīrulis]

Got the proof term that is 775 symbols long (if everything is written).
And 232 symbols long, if everything except MP, A1, A2, A3 is replaced by underscores (Lean can infer what must be used in the place of underscores).

There should be shorter solution. :(