1 files changed, 36 insertions, 0 deletions
diff --git a/content/zettel/4e3.md b/content/zettel/4e3.md
new file mode 100644
index 0000000..6f11e82
--- /dev/null
+++ b/content/zettel/4e3.md
@@ -0,0 +1,36 @@
++++
+title = "Models in propositional logic"
+date = "2022-04-11"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["4e2"]
+forwardlinks = ["4e4"]
+zettelid = "4e3"
++++
+
+When $\Gamma \vDash A$ ($\Gamma$ models $A$), it means that semantically
+$A$ will hold in the environment of $\Gamma$. This semantics approach is
+quite different to what $\Gamma \vdash A$ ($A$ can be derived from
+$\Gamma$) says, which is that there is a derivation (which is inherently
+finite), that proves $A$ given the environment $\Gamma$.
+
+This means that to reason about the semantics of the proof framework
+requires a stronger, external model, to be able to manipulate the
+$\sigma$ in $M, \sigma\vDash A$, where $M$ is the model and $\sigma$ is
+the state of all the variables.
+
+Finally, using the semantic meaning of $A$ and the syntactic meaning of
+$A$, one can express soundness and consistency by the following:
+
+soundness
+:   a formula for which one can derive a proof is also true:
+    $\Gamma \vdash A \implies \Gamma \vDash A$.
+
+consistency
+:   if a formula is true, then there exists a derivation of it's proof:
+    $\Gamma \vDash A \implies \Gamma \vdash A$.
+
+As these talk about the semantics of A, they also need to be reasoned
+about in an external logic, which is often just assumed to exist and is
+normally stronger than the current logic.