Add content

1 files changed, 23 insertions, 0 deletions

diff --git a/content/zettel/3c3f6a.md b/content/zettel/3c3f6a.md
new file mode 100644
index 0000000..e5029b4
--- /dev/null
+++ b/content/zettel/3c3f6a.md
@@ -0,0 +1,23 @@
++++
+title = "Evaluability inside of a current context"
+date = "2023-02-14"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3f6"]
+forwardlinks = []
+zettelid = "3c3f6a"
++++
+
+The main important property is also not that one can always find an
+execution of a predicate in any context, but that in the current context
+that we are proving things in, that one can evaluate it only there. This
+is a much easier property to maintain (and is maintained automatically
+by the proof), because the semantic interpretation of the forest ensures
+that one evaluates all the predicates to some boolean already. This
+means that given the current context which can interpret the forest, we
+can also interpret any predicate that is inside the forest already.
+
+This also means that if we want to add a new predicate to the forest,
+that we need to show we can evaluate it, where the lazy predicate
+evaluation is important again.