Commits

Paweł Wieczorek  committed 84db9ec

* usunięcie kolejnego śmiecia Util.Theory
* dodanie skryptu uruchamiającego CoqIde tak jak bym chciał

  • Participants
  • Parent commits 176a78f

Comments (0)

Files changed (2)

File metalogic/Util/Theory.v

-Require Import Lang.
-Require Import Proof.
-Require Import Proof_facts.
-Require Import Sets.Ensembles.
-Require Import Sets.Finite_sets.
-Section TheoryDefs.
-
-
-Definition PcConsistentTheory T:= exists p, ~ (T |- p).
-Definition PcInconsistentTheory T:= exists p, (T |- p) /\ (T |- !p).
-Definition PcCompleteTheory T:= forall p, (T |- p) \/ (T |- !p).
-
-
-Theorem T0:
- forall T S, PcConsistentTheory T -> Included _ S T -> PcConsistentTheory S.
-Proof.
- intros T S consT subset.
- destruct consT.
- exists x.
- intro Sx.
- absurd (T |- x).
- assumption.
- apply PcProof_superset.
-Qed.
-
-Theorem PcCompactness: 
- forall T S, PcConsistentTheory T <-> (Included _ S T -> Finite _ S -> PcConsistentTheory S).
-Proof.
-intros.
-split.
- intros.
-
-(*
-Nie wiem czy powinienem byc zainteresowany tym dowodem, bez NNP on nie przejdzie.
-
-Theorem PcInconsistentTheory_corr T:
-  PcInconsistentTheory T <-> ~PcConsistentTheory T.
-Proof.
- intros T. split.
- intros inc. unfold PcConsistentTheory.
-*)
-
-End TheoryDefs.

File startCoqIde.sh

+COQIDE= coqide # <- liczę na to że to zawsze będę miał w $PATH
+
+$COQIDE -R metalogic metalogic