Lab: Modeling with Logic

Problem: Back and Forth

Translate each of the natural language propositions into formal logical propositions. Ensure in your answer that you (1) identify the atomic propositions and assign them to variables and (2) write your formal proposition in terms of these variables. Make sure you maximally translate the proposition using as many of the connectives introduced in the reading. In particular, make sure you use the negation logical operator when appropriate in your answers.

  1. It rained this morning and it will be sunny this afternoon.
  2. If I am forced to stay in-doors this week, I will play Genshin Impact, have fun, and become poor.
  3. If I either eat Taco Bell or McDonalds, I will either become swoll, or I will not survive the night.
  4. If Jan and Bob both work at the company, then Jan certainly works more than Bob.

Now, consider the following parameterized atomic propositions:

  • = "I love ."
  • = " barfs."
  • = "I own ."
  • = "I'm sending away ."

As well as their parameterized versions:

Translate each of the formal logical propositions to natural language propositions. Ensure that your natural language propositions clearly indicate the explicit grouping found in the formal logic propositions.

  1. .
  2. .
  3. .
  4. .
  5. .

Note that and have higher precedence than . So, for example,

is equivalent to

Problem: Warm-up

In our examples from the reading relied heavily on non-mathematical, intuitive propositions to convey the meaning of quantified propositions. Now we'll consider translating propositions of a more mathematical nature between formal, symbolic statements and English.

First, translate each of the following formal statements regarding integers into English and for each, explain in a sentence or two why they are true.

  • .
  • .
  • .

Now, consider the following theorems taken from Fortnow's paper on his Favorite Ten Complexity Theorems of the Past Decade. Computational complexity theory is a branch of computer science concerning the resource usage (both time and space) of algorithms. While we do not have the background to fully understand what each of Fortnow's theorems (i.e., main propositions) says, we can certainly translate their logical intent. For each of these theorems, identify relevant atomic propositions and predicates and give a formal statement of the theorem maximizing your use of our logical connectives.

  • Theorem 1: For any one-way function, there exists a pseudorandom generator constructed from that one-way function.
  • Theorem 2: There are no sparse sets hard for via polynominal-time bounded truth-table queries unless . (Hint: to deal with "unless," think about what it means and try to rewrite the theorem in terms of a "if...then" rather than "unless.")

Problem: Quantification and Negation

The negation of propositions can be tricky to reason about. De Morgan's laws:

Remind us that negation doesn't simply "distribute into" connectives like conjunction and disjunction. Instead, De Morgan's laws say we "distribute/factor the negations and flip the signs." Are there similar equivalences for quantifiers? We'll answer this question by using real-world examples and our intuition to gain understanding.

Consider the following variants of propositions involving universal and existential quantification and negation both inside and outside of the quantifier.

  • .
  • .
  • .
  • .
  • .
  • .
  1. Come up with a concrete example predicate to use for this exploration. For each of these propositions above, translate the proposition into English. Try to choose a predicate that is both memorable and simple to reason about.
  2. Using your English translations as a guide, decide which pairs of propositions are equivalent.
  3. For each pair of propositions you believe are equivalent, write a sentence or two justifying the equivalence, using your concrete example to explain why it holds.

Problem: Thinking About Proof

Thinking ahead, we've used first-order logic to explore the extends of what we can express as far as propositions go. However, we are studying logic in this course to derive a set of rules for proving a proposition. Because our propositions are defined inductively, i.e., as a finite set of cases, our rules for proving a proposition also follow by case analysis on the different cases.

For each possible form of a proposition given in the reading, describe at a high-level how you would go about proving that proposition in a few sentences per form. Use a concrete example of a proposition in English for each case to describe your process. For example, for conjunction , I would instantiate and to concrete propositions, e.g.,

  • = "The sky is rainy."
  • = "It is dark outside."

And then explain how I would prove . Use your example and your intuition about what each logical connective means to arrive at your process. In tomorrow's reading and lab, we'll firm up your intuition with concrete rules and then look at how we express these rules precisely using mathematical notation.