Zulip Chat Archive

Stream: general

Topic: Logic & Proof


view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 09:42):

Hi, I am going through the online course Logic and Proof. I am stuck in the exercises. Is this the right place to ask such questions?

view this post on Zulip Chris Hughes (Jun 07 2018 at 09:44):

Yes

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 09:50):

Thanks. So I'm stuck progressing with the last prob. of Chapter 4's exercises i.e. prove ¬ (A ↔ ¬ A)

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 09:52):

I am thinking of following the rules mentioned in the book till now and start with the assumption that (A ↔ ¬ A)is true and then progress to show false so that I can prove the negation. But I can't figure out a way forward

view this post on Zulip Kenny Lau (Jun 07 2018 at 09:53):

hint: prove ¬ A from your assumption

view this post on Zulip Chris Hughes (Jun 07 2018 at 09:58):

This actually came up in M1F, and I was annoyed with myself for assuming excluded middle.

view this post on Zulip Kenny Lau (Jun 07 2018 at 09:58):

not constructive enough, eh :P

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 10:02):

am failing to get how can I get ¬ A with just assuming A ↔ ¬ A. I can get it if I also assume A and apply left elimination to the iff to get ¬ A. Is my understanding correct ?

view this post on Zulip Kenny Lau (Jun 07 2018 at 10:02):

no, you need to assume A and prove false

view this post on Zulip Kenny Lau (Jun 07 2018 at 10:03):

ok, which you get via deducing ¬ A

view this post on Zulip Chris Hughes (Jun 07 2018 at 10:05):

Try have h : ¬ A

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 10:05):

I am trying to do something like that but I am getting a type mismatch error coz of the additional assumption.
Could you please look at this LEAN code

view this post on Zulip Chris Hughes (Jun 07 2018 at 10:07):

You can only do assume a : A if your goal is A → something

view this post on Zulip Chris Hughes (Jun 07 2018 at 10:07):

Have you used have before?

view this post on Zulip Kenny Lau (Jun 07 2018 at 10:08):

variables A : Prop

example : ¬ (A  ¬ A) :=
assume h,
have h1 : ¬ A, from _,
show false, from _

view this post on Zulip Kenny Lau (Jun 07 2018 at 10:08):

so your code should look like this

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 10:12):

yeah that's what I am trying but could not think of any intro/elim rule to apply to get ¬ A from h

view this post on Zulip Moses Schönfinkel (Jun 07 2018 at 10:15):

The biggest hint here was the innocuous sentence "...and I was annoyed with myself for assuming excluded middle" :). You can't conjure not A from thin air, but you can conjure something almost as good.

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 10:19):

Ok I think I got it

variables A : Prop

example : ¬ (A ↔ ¬ A) :=
assume h,
have h1 : ¬ A, from
    assume a : A,
    show false, from (h.mp a) a,
show false, from h1 (h.mpr h1)

view this post on Zulip Kaushik Chakraborty (Jun 07 2018 at 10:20):

thanks a lot for the guidance

view this post on Zulip Kaushik Chakraborty (Jul 19 2018 at 07:25):

Hello again. I want to do the exercise 17.1 of the course on proving the equivalence of principle of complete induction to principle of least element in Lean. So in that regard does the following setup make sense? I still need to do the actual proof.

variable P :   Prop

example :  n, ( m, m < n  P(m)   P(n))   x, P(x) 
                 n, P(n)   m x, m < n  ¬ (x < m)  P(m) :=
sorry

view this post on Zulip Mario Carneiro (Jul 19 2018 at 07:38):

the parentheses seem to be off in a few places

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:00):

I think this is correct with minimal parentheses:

variable P :   Prop

example : (( n, ( m, m < n  P m)  P n)   x, P x) 
             n, P n   m, P m   x, x < m  ¬ P x :=
sorry

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:03):

the statement of the principle of least element you gave looks really weird and is probably incorrect - I've changed the statement a bit

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:04):

I expect it to say something like "if P(n) for some n, then there exists an m such that P(m), and ¬ P(x) for all smaller x"

view this post on Zulip Johan Commelin (Jul 19 2018 at 08:07):

The current statement reads to me as "I can prove P by induction iff the principle of least element holds for P"

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:12):

My point is that the right hand side doesn't look like the PLE to me

view this post on Zulip Johan Commelin (Jul 19 2018 at 08:14):

Oooh, you are completely right. The right hand side should start with \exists. As stated it is trivial: take m = 0.

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:14):

Also, I don't think this will actually work (unless you prove both sides individually), since the traditional reduction of induction to PLE and vice versa involves negating P

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:15):

this can be rectified by quantifying P individually on each side:

example : ( P :   Prop, ( n, ( m, m < n  P m)  P n)   x, P x) 
            (P :   Prop) n, P n   m, P m   x, x < m  ¬ P x :=
sorry

view this post on Zulip Kaushik Chakraborty (Jul 19 2018 at 08:17):

Ok. I got the formalization of PLE. Thanks

view this post on Zulip Kaushik Chakraborty (Jul 19 2018 at 08:20):

although in your formalization of PLE, there is no relation between n and m. Shouldn't we mention that m < n ?

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:28):

There is no need, in the same way that there is no relation between n and x in the statement of induction

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:29):

You can prove, given the conclusion, that m <= n, but it is possible that m = n if n is already the minimal witness

view this post on Zulip Mario Carneiro (Jul 19 2018 at 08:30):

another way to bracket it is ∀ (P : ℕ → Prop), (∃ n, P n) → ∃ m, P m ∧ ∀ x, x < m → ¬ P x

view this post on Zulip Kaushik Chakraborty (Jul 19 2018 at 08:32):

Ok got it.

view this post on Zulip Kaushik Chakraborty (Jul 23 2018 at 09:25):

I'm stuck at this simple proof. how do I go from n * n < m * m to n ^ 2 < m ^2

open nat
variables n m : ℕ

example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 :=
assume h,
have n * n < n * m, from mul_lt_mul_of_pos_left h.right h.left,
have n * m < m * m, from mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right),
have n * n < m * m, from lt_trans ‹ n * n < n * m › ‹ n * m < m * m ›,
sorry

view this post on Zulip Kenny Lau (Jul 23 2018 at 09:32):

open nat
variables n m : 

example : 0 < n  n < m  n ^ 2 < m ^ 2 :=
assume h,
calc  n ^ 2
    = nat.pow n 2 : by dsimp [(^)]; refl
... = 1 * (n * n) : nat.mul_assoc 1 n n
... = n * n : nat.one_mul _
... < n * m : mul_lt_mul_of_pos_left h.right h.left
... < m * m : mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right)
... = m ^ 2 : by simp [(^), nat.pow]

view this post on Zulip Kenny Lau (Jul 23 2018 at 09:33):

@Mario Carneiro why can't I replace by dsimp [(^)]; refl with rfl?

view this post on Zulip Chris Hughes (Jul 23 2018 at 09:34):

Definitional equality is not transitive.

view this post on Zulip Kenny Lau (Jul 23 2018 at 09:34):

but then why does this work?

view this post on Zulip Kenny Lau (Jul 23 2018 at 09:34):

example : n ^ 2 = nat.pow n 2 := rfl

view this post on Zulip Kenny Lau (Jul 23 2018 at 09:35):

Definitional equality is not consistent either?

view this post on Zulip Kaushik Chakraborty (Jul 23 2018 at 09:37):

thanks @Kenny Lau . I still don't understand tactics. Maybe the theorem proving in lean course will help. Logic and Proof course have few mentions of tactics.

view this post on Zulip Johan Commelin (Jul 23 2018 at 09:42):

Kaushik, to answer your original question, there is pow_two which you can use to rewrite between n * n and n^2.

view this post on Zulip Kenny Lau (Jul 23 2018 at 09:42):

it's not available without further import though

view this post on Zulip Johan Commelin (Jul 23 2018 at 09:51):

Right, you need to import algebra.group_power, I think.

view this post on Zulip Kaushik Chakraborty (Jul 23 2018 at 10:37):

thanks @Johan Commelin. but am still not sure how to use pow_two in my proof. I think I have to use rewrite tactic but not sure how. Here is how I've changed my earlier proof

import algebra.group_power
open nat
variables n m : ℕ

example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 :=
assume h,
have n * n < n * m, from mul_lt_mul_of_pos_left h.right h.left,
have n ^ 2 < n * m, by sorry,
have n * m < m * m, from mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right),
have n * m < m ^ 2, by sorry,
lt_trans ‹ n ^ 2 < n * m ›  ‹ n * m < m ^ 2 ›

view this post on Zulip Johan Commelin (Jul 23 2018 at 10:41):

example (n : ) : n ^ 2 = n * n :=
begin
  rewrite pow_two
end

view this post on Zulip Kenny Lau (Jul 23 2018 at 10:43):

example (n : ) : n ^ 2 = n * n := pow_two n

view this post on Zulip Kaushik Chakraborty (Jul 23 2018 at 10:53):

yeah I got the function usage part but how do I use pow_two when I've the lt relation i.e. replace sorry in have n ^ 2 < n * m, by sorry when I've established n * n < n * m. Or I'm approaching it wrong ?

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:31):

You should be able to do this with rw

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:39):

import algebra.group_power

example (m n : ) (h : n * n < n * m) : n ^ 2 < n * m :=
begin
  have H : n ^ 2 = n * n := pow_two n,
  rw H,
  exact h
end

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:39):

You should also be able to do it with eq.subst but I can never ever ever for the life of me get it to work.

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:39):

\t

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:40):

import algebra.group_power

example (m n : ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm  h

[doesn't work]

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:40):

Can you fix it Kenny?

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:41):

I think you would like by convert h

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:42):

import algebra.group_power

example (m n : ) (h : n * n < n * m) : n ^ 2 < n * m :=
have H : n * n = n ^ 2, from eq.symm $ pow_two n,
H  h

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:43):

I'm not sure why your original version doesn't work

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:43):

import algebra.group_power

example (m n : ) (h : n * n < n * m) : n ^ 2 < n * m :=
by convert h; from pow_two n

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:44):

example (m n : ) (h : n * n < n * m) : n ^ 2 < n * m :=
((((pow_two n).symm : n * n = n ^ 2)  (h : n * n < n * m)) : n ^ 2 < n * m)

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:44):

:o

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:44):

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  n ^ 2 < n * m

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:44):

I see no metavariables!

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:44):

yeah I'm puzzled too

view this post on Zulip Chris Hughes (Jul 23 2018 at 19:44):

example (m n : ℤ) (h : n * n < n * m) : n ^ (2 : ℕ) < n * m := (pow_two n).symm ▸ h

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:44):

...

view this post on Zulip Chris Hughes (Jul 23 2018 at 19:44):

works

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:44):

...

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:45):

The well-known metavariable 2

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:48):

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  @has_lt.lt.{0} int int.has_lt
    (@has_pow.pow.{0 ?l_1} int ?m_2 ?m_3 n (@bit0.{?l_1} ?m_2 ?m_4 (@has_one.one.{?l_1} ?m_2 ?m_5)))
    (@has_mul.mul.{0} int int.has_mul n m)

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:48):

Indeed there was a metavariable

view this post on Zulip Chris Hughes (Jul 23 2018 at 19:48):

This works lemma thing (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:49):

?????????????????

view this post on Zulip Chris Hughes (Jul 23 2018 at 19:49):

not this though def thing (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:50):

I think this is a bug in pow_two -- the inbuilt 2 is a nat

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:51):

Clearly pow_two should be a definition not a theorem

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:51):

Or am I barking up the wrong tree ;-)

view this post on Zulip Kenny Lau (Jul 23 2018 at 19:52):

I agree. Split the definition into more cases for easier definitional equality.

view this post on Zulip Chris Hughes (Jul 23 2018 at 19:52):

I don't think it has anything to do with pow_two

lemma two_add_three : 2 + 3 = 5 := add_comm 0 5  rfl -- works

example : 2 + 3 = 5 := add_comm 0 5  rfl -- doesn't work

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 20:10):

example : (2 : ℕ) + 3 = 5 := add_comm 0 5 ▸ rfl -- works

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 20:11):

So the bit where it says "Ok I can't figure out the type of this 2 thing, let's let it be nat just so we can get on" is not occurring in the examples

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 20:11):

Maybe pow_two should have been an example. Wait...

view this post on Zulip Mario Carneiro (Jul 23 2018 at 23:50):

The reason that example and def fail while theorem succeeds is due to the separation of statement and proof done with theorem

view this post on Zulip Mario Carneiro (Jul 23 2018 at 23:51):

Remember how I mentioned a long time ago that nat is the default type for numerals but it occurs very late in the elaboration? It's basically the last resort if there is a numeral of indeterminate type

view this post on Zulip Mario Carneiro (Jul 23 2018 at 23:54):

In regard to this example, what happens is that since def/example allows the statement and proof to be elaborated together, it checks the proof to see if that will give a hint what is alpha in (2:alpha) + 3 = 5. But that means that when it hits the eq.subst it will still have a lingering metavariable. In the theorem case, there is no information to be had, since the proof doesn't contribute to elaborating the statement, so it goes with the default nat type for numerals. Then when it elaborates the proof, there are no metavariables

view this post on Zulip Kaushik Chakraborty (Jul 24 2018 at 23:29):

For this code in the LEAN live in-browser IDE

import algebra.group_power
theorem thing (m n : ) (h : n * n < n * m) : (n ^ 2 < n * m) := (pow_two n).symm  h

am getting following error

"eliminator" elaborator type mismatch, term
  h
has type
  n * n < n * m
but is expected to have type
  n ^ 2 < n * m
Additional information:
/test.lean:2:82: context: the inferred motive for the eliminator-like application is
  λ (_x : ), n ^ 2 < n * m

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 23:33):

Join the -haters club!

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 23:34):

Sometimes the issue is that higher-order unification is undecidable, sometimes I've just made a silly mistake.

view this post on Zulip Chris Hughes (Jul 24 2018 at 23:36):

The mistake here is that pow_two is a theorem about monoid.pow and not nat.pow

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 23:36):

yes, I just realised that when trying to solve without the triangle

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 23:36):

invalid type ascription, term has type
  @has_lt.lt nat nat.has_lt (@has_pow.pow nat nat (@monoid.has_pow nat nat.monoid) n 2)
    (@has_mul.mul nat nat.has_mul n m)
but is expected to have type
  @has_lt.lt nat nat.has_lt (@has_pow.pow nat nat nat.has_pow n 2) (@has_mul.mul nat nat.has_mul n m)

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 23:41):

theorem nat.pow_two (a : ) : a ^ 2 = a * a := show (1 * a) * a = a * a, by rw one_mul

theorem thing (m n : ) (h : n * n < n * m) : (n ^ 2 < n * m) := (nat.pow_two n).symm  h

view this post on Zulip Kaushik Chakraborty (Jul 25 2018 at 00:33):

thanks @Kevin Buzzard this worked. however, I have some doubts about the nat.pow_two theorem. In your proof, you showed a different equality than what is in the sig. of the theorem. Is Lean somehow guessing the fact that (1 * a) * a = a ^ 2. Or how is the rewrite tactics working here?

view this post on Zulip Nicholas Scheel (Jul 25 2018 at 01:04):

that’s obtained by unfolding the definition of pow, which basically is that n^a = (((1*n)*n)*...)*n (with a ns of course)

view this post on Zulip Kaushik Chakraborty (Jul 25 2018 at 08:05):

got it. thanks, @Nicholas Scheel

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 09:04):

Yes, there are two kinds of equality in Lean. There's "equal by definition" and "equal because of a theorem". a^2=1*a*a is true by definition of ^ (you can discover this sort of thing by continually unfolding everything -- switch off notation and just get unfolding in tactic mode and see where you go) but 1*a=a is true because of a theorem. Things that are equal by definition you can just use interchangeably (I used show to change the goal to a goal which Lean thinks is the same goal by definition), but then I used a rewrite to apply the theorem.

view this post on Zulip Kaushik Chakraborty (Aug 09 2018 at 00:22):

I am trying to attempt a Lean proof of quotient-remainder theorem shown here and, as usual, clueless on the approach. I've tried to chalk out a rough skeleton of the proof based on my understandings from an earlier chapter on doing induction in Lean & some exploration of Lean's types and functions. Does it make sense?

open int
open nat

 -- quotient / remainder theorem
theorem qt (n m q r : ℤ) : m > 0 → n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
assume h,
show (n = m * q + r) ∧ (0 ≤ r ∧ r < m), from
  int.rec_on n
  (assume k,
  show (of_nat k = m * q + r) ∧ ( 0 ≤ r ∧ r < m ), from
    nat.rec_on k
      (show (of_nat 0 = m * q + r) ∧ (0 ≤ r ∧ r < m), from sorry)
      (assume k ih,
        show of_nat (succ k) = m * q + r ∧ (0 ≤ r ∧ r < m), from sorry)
  )
  (assume k,
    have h11 : -of_nat (k + 1) = m * q + r, from sorry,
    have h22 : 0 ≤ r ∧ r < m, from sorry,
    ⟨ h11 , h22 ⟩)

view this post on Zulip Chris Hughes (Aug 09 2018 at 00:34):

The theorem isn't true. This says for all n m q r, ... Whereas you want forall m n, exists q r,...

view this post on Zulip Chris Hughes (Aug 09 2018 at 00:35):

the proof of this theorem in the lean library is a combination of int.mod_add_div, int.mod_lt and int.mod_nonneg.

view this post on Zulip Kaushik Chakraborty (Aug 09 2018 at 05:07):

Oh, thanks for clarifying. Does this theorem statement make sense?

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, (n = m * q + r) ∧ (0 ≤ r ∧ r < m) :=
sorry

view this post on Zulip Kaushik Chakraborty (Aug 09 2018 at 07:07):

I tried to solve the above statement with the functions you mentioned but I could not figure out how to come up with the existential terms q & r from n and m and hence the proof does not type check. I must be formulating the theorem statement wrong or missing some approach in the proof.

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
assume n m h,

assume q r,
assume h2 : q = n / m,
assume h1 : r = n % m,

have HH:  n = m * q + r, from calc
  n = n % m + m * (n / m) : by rw [int.mod_add_div]
  ... = r + m * (n / m) : by rw h1
  ... = r + (m * q) : by rw h2
  ... = (m * q) + r : by rw add_comm,

have HH1: 0 ≤ r, from calc
  0 ≤ n % m : int.mod_nonneg n (ne_of_gt h)
  ... ≤ r : by rw h1,

have HH2: r < m, from calc
  r = n % m : by rw h1
  ... < abs m : int.mod_lt n (ne_of_gt h)
  ... = m : abs_of_pos h,

exists.intro q (exists.intro r (and.intro HH  (and.intro HH1 HH2) ))

view this post on Zulip Mario Carneiro (Aug 09 2018 at 07:12):

This is an incorrect use of the assume keyword. assume is used only for proving a forall or pi or implication, and it introduces a variable with the type specified in the domain. To prove an existential, you use exists.intro and provide the witness you want

view this post on Zulip Mario Carneiro (Aug 09 2018 at 07:14):

So after assume n m h, you should write exists.intro (n / m) $ exists.intro (n % m) $ instead of assume q r, assume h2 : q = n / m, assume h1 : r = n % m,

view this post on Zulip Mario Carneiro (Aug 09 2018 at 07:14):

(The dollar signs are to save on having to close parentheses at the end of the proof)

view this post on Zulip Mario Carneiro (Aug 09 2018 at 07:15):

After that, q and r will no longer be present in the statement, so you won't need to rewrite with h1 anymore

view this post on Zulip Kaushik Chakraborty (Aug 09 2018 at 08:03):

I knew what was wrong with that assume but your tip on the exists.intro was helpful. Here's my updated proof which type checks

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
assume n m h,

exists.intro (n / m) $ exists.intro (n % m) $

  have HH:  n = m * (n / m)  + (n % m), from calc
    n = n % m + m * (n / m) : by rw [int.mod_add_div]
    ... = m * (n / m) + (n % m) : by rw add_comm,

  have HH1: 0 ≤ (n % m), from int.mod_nonneg n (ne_of_gt h),

  have HH2: (n % m) < m, from calc
    (n % m) < abs m : int.mod_lt n (ne_of_gt h)
    ... = m : abs_of_pos h,

  ⟨ HH , ⟨ HH1 , HH2 ⟩ ⟩

view this post on Zulip Olivier de G. (Feb 29 2020 at 06:57):

I am working on exercice 2 of Chapter 2. The exercise states that the first clue can be represented as

((FASA)(MWDW))((MADA)(FWSW))((FA \lor SA) \rightarrow (MW \lor DW)) \land ((MA \lor DA) \rightarrow (FW \lor SW))

Should the implications be replaced with iff as follows ?

((FASA)(MWDW))((MADA)(FWSW))((FA \lor SA) \leftrightarrow (MW \lor DW)) \land ((MA \lor DA) \leftrightarrow (FW \lor SW))

view this post on Zulip Olivier de G. (Feb 29 2020 at 07:01):

Humm maybe it's actually equivalent because of

FWSWMWDWFW \lor SW \lor MW \lor DW

and

FASAMADAFA \lor SA \lor MA \lor DA

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 11:17):

I think you're right. Both interpretations are valid translations of the sentence and. as you say, both are equivalent in the context (but of course they are not equal).

This is a common theme I guess. I found it interesting watching computer scientists claiming that they had proved there were infinitely many primes by showing that given a finite set of primes, they could find a prime not in this set. I initially thought "that's not what infinite means" but then I realised that actually it's a perfectly reasonable way of formalising it ("no finite set of primes is all the primes") and actually I didn't really know what infinite meant -- there are several definitions of infinite, all equivalent, but not at all equal, and one has to make a choice at some point.


Last updated: May 15 2021 at 23:13 UTC