Help solving formal logic exercises with Lean

Stream: new members

[Trunks]

EXERCICE 1

example (h1: VSE joe → VSE tim)  (h2: ¬ VSE joe → VSE clara) : VSE tim ∨ VSE clara := by

---EXERCICE 2
-- a) do with Tiers Exclu -> em

example (h1: ¬ VSE joe → VSE clara) (h2: ¬ VSE clara): VSE joe :=by

-- b) dowith Double negation -> byContracdiction

example (h1: ¬ VSE joe → VSE clara) (h2: ¬ VSE clara): VSE joe :=by

---EXERCICE 3
-- a) do with Tiers Exclu -> em

example (h1: ¬ VSE joe → VSE clara) (h2: ¬ VSE joe → ¬ VSE clara): VSE joe :=by

-- b) do with Double negation -> byContracdiction

example (h1: ¬ VSE joe → VSE clara) (h2: ¬ VSE joe → ¬ VSE clara): VSE joe :=by

---EXERCICE 4

example : (p→ q) → (¬ p ∨ q) :=by

---EXERCICE 5

example : (∀ x: Person, (Etudiant x → VSE x)) → ∀ x: Person, (¬ Etudiant x ∨ VSE x) :=by

---EXERCICE 6

example : ¬ (p ∧ q) → (¬ p ∨ ¬ q) :=by

---EXERICZ 7 (Challenge: Difficile!)

The goal is to prove the "paradoxical" property of classical logic:
∃ x: Person, (Millionaire x → ∀ y: Person, Millionaire y)
"There exists a person such that if they are a Millionaire, then all people are Millionaires."
Help:
a) You need to use the Law of Excluded Middle with the formula "(∀ y: Person, Millionaire y)", so reasoning by cases:

• If everyone is a millionaire, then...
• If it is not true that everyone is a millionaire, then...

b) You need to use the lemma_utile above with the application "lemma_utile Person Millionaire".

example : ∃ x: Person, (Millionaire x → ∀ y: Person, Millionaire y) :=by

[Kevin Buzzard]

There are several issues with your post, unfortunately.

1) Code should be posted within triple back-ticks: ```
2) Code should work for other people not just for you. You have VSE everywhere in your code (and joe etc) and this is just an error for everyone because it has no definition, so nobody else can even understand the question.
3) This looks like a lazy attempt to get someone else to do your homework, and this Zulip is not a homework-solving site.

[Trunks]

oh okey thanks for your answer

Le mer. 4 déc. 2024 à 12:32, Zulip notifications <noreply@zulip.com> a
écrit :