jly02 Goto Github PK

I'm a computer science major at the University of Washington. My interests span several theoretical and applied disciplines, including computational complexity theory, cryptography, logic and programming languages, and formal methods. It might seem like a lot to some, but there's no reason to believe these topics are all disjoint: if I don't know what the intersection is yet, I simply have to learn more.

And while these may sound highly academic, I am equally enthusiastic about applying my knowledge to real-world situations!

Currently, I'm a research assistant at the HPDIC lab. My work is about designing and implementing cryptographic protocols which leverage caching and the power of homomorphic encryption to accelerate encryption operations for large batches of data (see: RacheAL).

You can find links to my LinkedIn and email on my website!

Theorem (Law of the Excluded Middle, Model Theoretic Version). For any predicate $A$ and structure $M$ on a language $\mathcal{L}$, $$M \vDash (A(x) \lor \neg A(x))$$

Proof. Let $s$ be a variable assignment. Note that $|M| = A^M \cup (|M| - A^M)$, $A$ is modelled by some subset of $|M|$. Suppose we have $\text{Val}_s^M(x) = x_s^M$ ($x$ is interpreted as $x_s^M$ in the meta-language). Then there are two cases:

1. $x_s^M \in A^M$. By definition, we have that $M,s \vDash A(x)$.
2. $x_s^M \in |M| - A^M$. Then, $x_s^M \notin A^M$, and so we have $M, s \nvDash A(x)$. By definition, $M,s \vDash \neg A(x)$.

So it is the case that $M, s \vDash (A(x) \lor \neg A(x))$. Since $s$ was arbitrary, we may disregard it, giving us the claim. $\qquad \square$