1. Do Not Iron While Wearing Shirt

For each of the following English statements, (i) translate it into predicate logic, (ii) write the negation of that statement in predicate logic with the negation symbols pushed as far in as possible, and then (iii) translate the result of (ii) back to (natural) English.

Let the domain of discourse be people and activities. You should use only the predicates Loves(_x,y) and Likes(_x,y) which say that person x loves or likes (respectively) activity y; the predicates Person(_x) and Activity(_x), which say whether x is a person or activity, respectively; and the predicates x _{= y} and x _{6= y}, which say whether or not x and y are the same object. You can use constants to refer to specific people or activities such as the Bob in the next example.

Example: There is some activity, other than ironing, that Bob likes.

1. x((Activity(x) (x 6= ironing)) Likes(Bob,x)) ii. x((Activity(x) (x 6= ironing)) Likes(Bob,x))

(Make sure you see why! Its important to notice domain restrictions when translating to English.) iii. Bob does not like any activity other than ironing.

(Or less natural: Every activity other than ironing is not liked by Bob.) (a) [9 Points] Every activity that Bob loves is also loved by someone else.

(b) Someone who likes every activity does not love any activity.

2. May Cause Drowsiness

Write formal proofs of each of the following.

• Given p _q, p _r, and r _{(s w)}, it follows that q _w.
• Given p q, r p, and (r q) s, it follows that p s.
• Given ((p q) (p r)) ((p r) (p q)), it follows that p ((q r) (r q)).

You can write your proofs by hand or in LATEX. Alternatively, feel free to use either of the following tools:

• This tool will allow you to check the correctness of most proofs in Propositional Logic. You can use it for these problems by typing in the premise and conclusion and clicking Start Proof. (You can take a screenshot of your completed proof and include it in your submission.)
• Cozy IDE now has a project template called CSE 311 HW3 that is preloaded with these three problems.

(As in HW2, you can download your completed project as a zip file and submit it in canvas.)

(Both tools only allow one premise, but they can take the of those facts as the premise instead.)

3. Contents Under Pressure

In this problem, we will consider the following, new inference rule:

This rule says that, if we know that either A or B is true and that both A implies C and B implies C, then it follows that C is true. If it is A that is true, then we get that C is true by Modus Ponens and likewise if B is true instead. This is a valid rule of inference and you are free to use it outside of this problem as well.

• Use the Proof By Cases rule to prove the following. Given p _{(q r)}, q _{(r s)}, and r (r s), it follows that p (s t)
• Prove that the Elim rule follows from Proof By Cases. Specifically, use the Proof by Cases rule to prove that, given p _q and _p, it follows that q is true. (You may not use Elim .)
• ] What does (b) tell us about the relative power of Elim versus Proof By Cases to infer new facts from given ones?

4. Not Intended For Human Consumption

Let Q_(x) be a predicate defined in some, fixed domain of discourse.

• Prove that, given (y Q(y)), it follows that x(Q(x) y Q(y)).
• Prove that, given y Q(y), it follows that x(Q(x) y Q(y)).

Hint: It is okay to simply repeat a fact proved above, again, on another line below. Just cite the original line where it appeared as the explanation.

• Why can we conclude from parts (a) and (b) that _{x(Q(x) y Q(y))} is a tautology? Explain. (A formal proof is not necessary but is also allowed.)

5. Keep Away From Small Children

Recall that an integer n is a square iff there exists a k Z such that n _{= k}². Formally, with our domain of discourse as the integers, we can define Square(_{n) := k (n = k}²₎.

• Write the following claim in Predicate Logic: if integers n and m are squares, then nm is a square. (Be careful!)
• Give a formal proof of the claim from part (a). In addition to the inference rules discussed in class, you can also rewrite an algebraic expression to equivalent ones using the rule Algebra. (E.g., you could write a_{(b + 1) a = ab} with Algebra as the rule / explanation.)
• Translate your formal proof from part (b) into an English proof.

6. Extra Credit: Some Assembly Required

In this problem, we will extend the machinery we used in HW1s extra credit problem in two ways. First, we will add some new instructions. Second, and more importantly, we will add type information to each instruction.

Rather than having a machine with single bit registers, we will imagine that each register can store more complex values such as

Primitives These include values of types int, float, boolean, char, and String.

Pairs of values The type of a pair is denoted by writing between the types of the two parts. For example, the pair (1_,true) has type int boolean since the first part is an int and the second part is a boolean.

Functions The type of a function is denoted by writing a between the input and output types. For example, a function that takes an int as argument and returns a String is written int String. We add type information, describing what is stored in each each register, in an additional column next to the instructions. For example, if R₁ contains a value of type int and R₂ contains a value of type int ₍Stringint), i.e., a function that takes an int as input and returns a pair containing a String and an int, then we could write the instruction

R₃ := CALL(R₁,R₂) String int

which calls the function stored in R₂, passing in the value from R₁ as input, and stores the result in R₃, and write a type of String int in the right column since that is the type that is now stored in R₃.

In addition to _CALL, we add new instructions for working with pairs. If R₁ stores a pair of type Stringint, then _LEFT(R1) returns the String part and _RIGHT(R1) returns the int part. If R₂ contains a char and R₃ contains a boolean, then _PAIR(R2,R3) returns a pair of containing a char and a boolean, i.e., a value of type char boolean.

• Complete the following set of instructions so that they compute, in the final register assigned, a value of type float boolean:

R₁ int float

R₂ int String

R₃ String ₍char boolean)

R₄ :=

The first three lines show the types already stored in registers R₁, R₂, and R₃ at the start, before your instructions are executed. You are free to use the values in those registers in later instructions.

Since we have unlimited space, store into a new register on each line. Do not reassign any registers.

• Compare the types listed next to these instructions to the propositions listed on the lines of your proof in problem 2 (a). Give a collection of text substitutions, such as replacing all instances of p by int (these can include both atomic propositions and operators), that will make the sequence of propositions in problem 2 (a) exactly match the sequence of types in problem 6 (a). You may need to change your solution to problem 6 (a) slightly to make this work.
• Now, lets add another way to form new types. If A and B are types, then A _{+ B} will be the type representing values that can be of either type A or type B. For example, String + int would be a type of values that can be strings or integers.

To work with this new type, we need some new instructions. First, if R₁ has type A, then the instruction _CASE(R1) returns the same value but now having type A _{+ B}. (Note that we can pick any type B that we want here.) Second, if R₂ stores a value of type A _{+ B}, R₃ stores a function of type A _C (a function taking an A as input and returning a value of type C), and R₄ stores a function of type B _C, then the instruction _{SWITCH(R2,R3,R4)} returns a value of type C: it looks at the value in R₂, and, if it is of type A, it calls the function in R₃ and returns the result, whereas, if it is of type B, it calls the function in R₄ and returns the result. In either case, the result is something of type C.

Complete the following set of instructions so that they compute, in the final register assigned, a value of type int ₍char + boolean):

R₁ int (float + String)

R₂ float (String char) R₃ String (String char)

R₄ :=

The first three lines again show the types of values already stored in registers R₁, R₂, and R₃. As before, do not reassign any registers. Use a new register for each instructions result.

• Compare the types listed next to these instructions to the propositions listed on the lines of your proof in problem 3 (a). Give a collection of text substitutions, such as replacing all instances of p by int (these can include both atomic propositions and operators), that will make the sequence of propositions in problem 3 (a) exactly match the sequence of types in problem 6 (c). You may need to change your solution to problem 6 (c) slightly to make this work.
• Now that we see how to match up the propositions in our earlier proofs with types in the code above, lets look at the other two columns. Describe how to translate each of the rules of inference used in the proofs from both problem 2 (a) and 3(a) so that they turn into the instructions in problem 6 (a) and (c).
• One of the important rules not used in problems 2 (a) or 3 (a) was Direct Proof. What new concept would we need to introduce to our assembly language so that the similarities noted above apply could also to proofs that use Direct Proof?