Answer as many questions as you can.

1. Write (in the logic notation used in this class) an encoding of “Everyone in Tanya’s class is more likely to pass the midterm if they know Type Theory”. Context: Tanya is a student and is only taking one class right now. “Everyone” means Tanya and her classmates.

   Many answers possible. Let $t$ be Tanya, $Asc$ means student $s$ attends class $c$, $y$ be Type Theory, $m$ be the midterm, $Pst$ be student $s$ passes test $t$, $Kst$ be student $s$ knows topic $t$.
   
   $\forall s. As(\iota c. Atc) \supset (pr(Psm \mid Ksy) \gt pr(Psm \mid \neg Ksy))$

2. A logical system has three parts. Choose the best description for the three parts:
   $\bigcirc$ syntax, axioms, inference rules

   $\bigcirc$ axioms, inference rules, theorems

   $\bigcirc$ alphabet, grammar, inference rules

   $\bigcirc$ symbols, models, inference rules

   ⬤ syntax, semantics, inference rules

   $\bigcirc$ symbols, axioms, models
3. Which of the following are accurate descriptions of 5 pentated to 2?
   $\Box$ 25

   $\Box$ A power tower of five 2s

   ⬛ A number that would take weeks to write out by hand

   $\Box$ $5\uparrow\uparrow 5\uparrow\uparrow 5\uparrow\uparrow 5\uparrow\uparrow 5$

   ⬛ $5^{5^{5^{5^5}}}$

   I did not mark the “weeks” option wrong. It does takes weeks, to write out, but the number of weeks is longer than the lifetime of the universe. But as someone pointed out, that is still some number of weeks.

4. Let $R = \{ (1,2), (2,1), (3,3) \}$. What is $R^2$ assuming (a) $R$ is just a regular set, and (b) $R$ is a relation?
   1. $\begin{array}{l}\{ \\ \;\;((1,2),(1,2)), ((1,2),(2,1)), ((1,2),(3,3)), \\ \;\;((2,1),(1,2)), ((2,1),(2,1)), ((2,1),(3,3)), \\ \;\;((3,3),(1,2)), ((3,3),(2,1)), ((3,3),(3,3)) \\ \} \end{array}$
   2. $\{ (1,1), (2,2), (3,3) \}$
5. Write the cond function in lambda notation.

   $\lambda(\mathsf{true} \to \lambda x_t. \lambda y_t. x \mid \mathsf{false} \to \lambda x_t. \lambda y_t. y)$

6. Match the people on the left with something they are known for on the right.

     Bertrand Russell ——— A letter to Frege
     Abraham Fränkel  ——— Replacement
     Ernst Zermelo    ——— Axiomatizing Set Theory
     David Hilbert    ——— Entscheidungsproblem
     Ada Lovelace     ——— Bernoulli Numbers Program
     Alonzo Church    ——— Lambda Calculus
     Georg Cantor     ——— Infinities
   

7. Match the Set Theory axioms with their intent.

     Foundation     ——— No self-containing sets
     Extensionality ——— What equality means
     Pairing        ——— You can combine two sets
     Union          ——— All the elements of the elements are a set
     Power Set      ——— Set of all subsets is a set
     Replacement    ——— Set of all members' images under a function
     Infinity       ——— The natural numbers comprise a set
     Choice         ——— Set with one element from each member
     Separation     ——— You can make a set by filtering
   

8. How is the list $[1,2,3]$ encoded in ZFC?

   $(1, (2, (3, \varnothing)))$

9. Give an inductive definition for a type which we will call Propositional Logic Formulas, or $\textsf{PLF}$. PLF’s are either constants, variables, not-expressions, and-expressions, or-expressions, or material implication expressions. You should be able to take it from here.
   $\dfrac{c: \textsf{Constant}}{\textsf{con}\;c: \textsf{PLF}}$

   $\dfrac{v: \textsf{Variable}}{\textsf{var}\;v: \textsf{PLF}}$

   $\dfrac{f: \textsf{PLF}}{\textsf{not}\;f: \textsf{PLF}}$

   $\dfrac{f_1: \textsf{PLF} \quad f_2: \textsf{PLF}}{\textsf{and}\;f_1\;f_2: \textsf{PLF}}$

   $\dfrac{f_1: \textsf{PLF} \quad f_2: \textsf{PLF}}{\textsf{or}\;f_1\;f_2: \textsf{PLF}}$

   $\dfrac{f_1: \textsf{PLF} \quad f_2: \textsf{PLF}}{\textsf{impl}\;f_1\;f_2: \textsf{PLF}}$
10. What are the inhabitants of the type $\textsf{Bool}\to\textsf{Bool}$? Write them out precisely.

    $\begin{array}{l} \lambda(\mathsf{true} \to \mathsf{true} \mid \mathsf{false} \to \mathsf{true}) \\ \lambda(\mathsf{true} \to \mathsf{true} \mid \mathsf{false} \to \mathsf{false}) \\ \lambda(\mathsf{true} \to \mathsf{false} \mid \mathsf{false} \to \mathsf{true}) \\ \lambda(\mathsf{true} \to \mathsf{false} \mid \mathsf{false} \to \mathsf{false}) \end{array}$