+++
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.