Commit 7b92a6d7 authored by Ralf Jung's avatar Ralf Jung

docs: update semantic entailment

parent 8bfac1ad
Pipeline #2772 passed with stage
in 9 minutes and 21 seconds
......@@ -98,20 +98,22 @@ We can now define \emph{semantic} logical entailment.
\typedsection{Interpretation of entailment}{\Sem{\vctx \mid \pfctx \proves \prop} : \mProp}
\[
\Sem{\vctx \mid \pfctx \proves \prop} \eqdef
\Sem{\vctx \mid \prop \proves \propB} \eqdef
\begin{aligned}[t]
\MoveEqLeft
\forall n \in \mathbb{N}.\;
\forall \rs \in \textdom{Res}.\;
\forall \gamma \in \Sem{\vctx},\;
\\&
\bigl(\All \propB \in \pfctx. n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)\bigr)
\Ra n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs)
n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs)
\Ra n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\rs)
\end{aligned}
\]
The soundness statement of the logic reads
\[ \vctx \mid \pfctx \proves \prop \Ra \Sem{\vctx \mid \pfctx \proves \prop} \]
The following theorem connects syntactic and semantic entailment:
\[ \vctx \mid \prop \proves \propB \Ra \Sem{\vctx \mid \prop \proves \propB} \]
It now becomes trivial to show soundness of the logic.
%%% Local Variables:
%%% mode: latex
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment