proposition: Theorem Incompleteness : forall T : System, Included Formula NN T -> RepresentsInSelf T -> DecidableSet Formula T -> exists f : Formula, (Sentence f) /\ (SysPrf T f \/ SysPrf T (notH f) -> Inconsistent LNN T).
proof: Proof. intros T H H0 H1; repeat induction H0. apply Rosser'sIncompleteness with x x0; auto; tauto. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith Lia) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(NNtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815)