proposition: Theorem Goedel'sIncompleteness1st : wConsistent T -> exists f : Formula, independent T f /\ closed f.
proof: Proof. intros H; exists G; pose freeVarG. pose FirstIncompletenessA. pose FirstIncompletenessB. assert (H0: ~Inconsistent LNN T). { intro H0; destruct (wCon2Con T H) as [x H1]. apply H1; apply H0. } repeat split; tauto. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) Goedel(fixPoint codeSysPrf) hydras.Ackermann(wConsistent) hydras.Ackermann(NN) hydras.Ackermann(code) hydras.Ackermann(checkPrf) hydras(Compat815)