Commit 78a8fbfc authored by Miriam's avatar Miriam

merge presentation parts

parent aeae78e0
......@@ -7,6 +7,7 @@
......@@ -43,7 +44,7 @@
Now we need a proof system satisfying:
Now we need a proof system satisfying exactly:
\item All intuitionistic tautologies
\item Closure under substitution and MP
......@@ -60,8 +61,58 @@
\begin{frame}{Natural Deduction for $\KIbox \oplus Z$}
Some of the rules \dots
\AxiomC{$\KIbox \oplus Z \vdash A, G \Rightarrow A$}
\RightLabel{\scriptsize $G'$ is permutation of $G$}
\UnaryInfC{$\KIbox \oplus Z \vdash A, G' \Rightarrow A$}
\UnaryInfC{$\KIbox \oplus Z \vdash A, G \Rightarrow A$}
\RightLabel{\scriptsize s substitution}
\UnaryInfC{$\KIbox \oplus Z \vdash A, G \Rightarrow s(Z)$}
%or elimination
% KIbox Z G (f1 ||| f2) -> KIbox Z (f1 :: G) f3 -> KIbox Z (f2 :: G) f3 -> KIbox Z G f3
\AxiomC{$\KIbox \oplus Z \vdash G \Rightarrow A \lor B$}
\AxiomC{$\KIbox \oplus Z \vdash A, G \Rightarrow C$}
\AxiomC{$\KIbox \oplus Z \vdash B, G \Rightarrow C$}
\TrinaryInfC{$\KIbox \oplus Z \vdash G \Rightarrow C$}
\begin{frame}{Natural Deduction for $\KIbox \oplus Z$}
The only rule for box:
%(forall f, In f F -> KIbox Z G (|[]| f)) -> KIbox Z F h -> KIbox Z G (|[]| h)
\AxiomC{$\forall A_i. \KIbox \oplus Z \vdash G \Rightarrow \Box A_i$}
\AxiomC{$\KIbox \oplus Z \vdash A_1 \dots A_n \Rightarrow B $}
\BinaryInfC{$\KIbox \oplus Z \vdash G \Rightarrow \Box B$}
TODO explanaition?
IM Tautologien (impl, and, or)
......@@ -69,7 +69,7 @@ Fixpoint sat (m : kripke_model) (w : worlds _) (f : form) : Prop :=
| var n => valuation _ w n
| A ->> B => forall w', (int_relation (_ m) w w') -> sat m w' A -> sat m w' B
| A & B => sat m w A /\ sat m w B
| A \v/ B => sat m w A \/ sat m w B
| A ||| B => sat m w A \/ sat m w B
| |[]| A => forall w', (modal_relation (_ m) w w') -> sat m w' A
......@@ -92,13 +92,32 @@ Qed.
(** ** Examples *)
Lemma and_imp_neg_sem:
Lemma imp_dneg_sem:
forall A, val (A ->> -+! A).
red. intros. simpl. intuition. eapply H2.
eapply preord_refl. apply int_relation_preorder.
eapply upclosed_int. apply H0. apply H1.
Inductive one_point_set : Set := Elem.
Definition empty_relation A : relation A := (fun a => fun b => False).
Program Definition one_point_frame : kripke_frame.
apply (Build_kripke_frame one_point_set (empty_relation one_point_set)
(empty_relation one_point_set)).
- constructor. apply Elem.
Lemma dneg_imp_sem:
forall A, ~ val (-+! A ->> A).
unfold val.
intros A H.
assert (exists m w, ~sat m w (-+! A ->> A)).
(** ** Soundness of KIbox *)
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