Propositional logic exercises with the lean theorem prover

mathematically wrote: post #5

sidpatil wrote: post #2

Just the kind of thing I've been looking for!

Just a heads up, worksheet 5 has an error: (P ↔ Q) → (R ↔ S) → (P ∧ Q ↔ R ∧ S). That proposition is not actually true.

It’s probably supposed to be (P & R) (Q & S)

Re: Propositional logic exercises with the lean theorem prover

#7

Post by mathematically » Fri, Oct 22, 2021, 8:47 AM UTC

BreakfastB0b wrote: post #6

mathematically wrote: post #5

Earlier quoted context omitted.

Just a heads up, worksheet 5 has an error: (P ↔ Q) → (R ↔ S) → (P ∧ Q ↔ R ∧ S). That proposition is not actually true.

It’s probably supposed to be (P & R) (Q & S)

Yup, transposition error.

Re: Propositional logic exercises with the lean theorem prover

#8

Post by kevinbuzzard » Fri, Oct 22, 2021, 8:59 AM UTC

mathematically wrote: post #7

BreakfastB0b wrote: post #6

Earlier quoted context omitted.

It’s probably supposed to be (P & R) (Q & S)

Yup, transposition error.

Thanks so much! Fixed.

Re: Propositional logic exercises with the lean theorem prover

#9

Post by kevinbuzzard » Fri, Oct 22, 2021, 9:00 AM UTC

kevinbuzzard wrote: post #8

mathematically wrote: post #7

Earlier quoted context omitted.

Yup, transposition error.

Thanks so much! Fixed.

PS I cannot believe my undergraduate teaching material is on HN! I am a math lecturer and this is just my course notes for my UGs.

Re: Propositional logic exercises with the lean theorem prover

#10

Post by mathematically » Fri, Oct 22, 2021, 9:14 AM UTC

kevinbuzzard wrote: post #9

kevinbuzzard wrote: post #8

Earlier quoted context omitted.

Thanks so much! Fixed.

PS I cannot believe my undergraduate teaching material is on HN! I am a math lecturer and this is just my course notes for my UGs.

It's very fun. Thanks for putting it together.