= 27d567bc2d48d9f40e9ccc20ea370b15)
Kytael comments on SotW: Be Specific - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (306)
It seems natural to evaluate existential quantifiers using model-checking and any universally quantified statement can be transformed into an existentially quantified statement by applying double-negation and moving the inner negation through the quantifier.
Example:
forall x. p(x)
not (not (forall x. p(x)))
not (exists x. (not p(x)))
But I can't think of how to apply this to Yudkowsky's example so it's probably useless for teaching :P
Here's one way that this could be transformed into an exercise: Have the instructor read a proof (or a fake proof) from, say, formal logic or set theory, and ask the students to follow along step-by-step using a simple example (a la Richard Feynman). Then, at the end of the proof, the students have to explain whether the proof is or is not valid using their example. E.g.:
Instructor: forall x. p(x)
"Ok, let's see, 'all ice cream cones are delicious'."
Instructor: not (not (forall x. p(x)))
"It's not true that 'not all ice cream cones are delicious'."
Instructor: not (exists x. (not p(x)))
"Therefore, 'there is never going to be an ice cream cone that is not delicious'. Valid!"