Skip to content
View jly02's full-sized avatar

Block or report jly02

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
jly02/README.md

Hi, I'm Jonathan! 🐼

I'm a fourth-year computer science major at the University of Washington. My interests span several theoretical and applied disciplines, including computational complexity theory, logic and programming languages, and formal methods.

What I'm Up To

I am currently a teaching assistant for CSE 421: Introduction to Algorithms at the University of Washington.

How to Reach Me

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

A Cool Theorem

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$

Pinned Loading

  1. RacheAL RacheAL Public

    Simple and efficient homomorphic encryption.

    C++

  2. hmxxu/BeatBuddy hmxxu/BeatBuddy Public

    BeatBuddy is a web application that crafts personalized playlists that perfectly match your unique music taste.

    TypeScript 1