1 files changed, 21 insertions, 0 deletions
diff --git a/content/zettel/4e4.md b/content/zettel/4e4.md
new file mode 100644
index 0000000..d443be1
--- /dev/null
+++ b/content/zettel/4e4.md
@@ -0,0 +1,21 @@
++++
+title = "Realizability"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["4e3"]
+forwardlinks = ["4e5"]
+zettelid = "4e4"
++++
+
+Mathematitians like to work with abstract notions when proving theorems.
+However, often we would like to compute with that same abstract notion,
+so we want to find an equivalent model, or realizer, that will allow us
+to do that. This realizer is special though, in that it is an element of
+the set of partial combinator algebras (pca) ($r \in \mathbf{A}$).
+
+One can then create an Assembly $S$, which is composed of a type $|S|$
+and realizers which are part of $\mathbf{A}$. Then, it's necessary that
+for each element in $|S|$ there is a realizer:
+
+$r \Vdash p$ for $p \in |S|$ and $r \in \mathbf{A}$.