proposition: Lemma FirstIncompletenessB : wConsistent T -> ~ SysPrf T (notH G).
proof: Proof. intros H; assert (con : (forall f:Formula, SysPrf T f) -> False). { intros H0. destruct (wCon2Con T H) as [x H1]. - apply H1; apply H0. } unfold G; destruct (FixPointLNN (notH codeSysPf) 0) as [x [H1 H2]]. unfold not in |- *; intros H0. set (codeX := code.codeFormula x) in *. unfold wConsistent in H. set (y := notH (substF codeSysPrf 0 (codeNatToTerm.natToTermLNN codeX))) in *. assert (forall x : nat, In x (freeVarF y) -> 1 = x). { intros x0 H3; unfold y in H3. assert (H4: (In x0 (freeVarF (substF codeSysPrf 0 (codeNatToTerm.natToTermLNN codeX))))) by apply H3. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5]. - destruct x0 as [| n]. elim (in_remove_neq _ _ _ _ _ H5). + reflexivity. + destruct n as [|n ]. * reflexivity. * elim (Compat815.le_not_lt (S (S n)) 1). assert (H6: In (S (S n)) (freeVarF codeSysPrf)). { eapply in_remove; apply H5. } apply ( freeVarCodeSysPrf _ _ _ _ _ _ _ _ freeVarRepT _ H6). apply Compat815.lt_n_S; apply Nat.lt_0_succ. - elim (closedNatToTerm _ _ H5). } induction (H _ _ H3) as [x0 H4]. - unfold y in H4. destruct (eq_nat_dec (checkPrf LNN LcodeLNN codeArityLNTF codeArityLNNR (codeFNN x) x0) 0) as [e |n ]. + apply H4. rewrite (subFormulaNot LNN). unfold codeSysPrf, codeX in |- *. apply codeSysPrfCorrect3. unfold not in |- *; intros A p H5. assert (H6: (checkPrf LNN LcodeLNN codeArityLNTF codeArityLNNR (codeFNN x) (codePrf A x p) = S (cPair.codeList (map codeFNN A)))). { apply (checkPrfCorrect1 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNNRIsCorrect1 A x p). } rewrite <- H5 in H6; rewrite H6 in e; discriminate e. + assert (H5: (checkPrf LNN LcodeLNN codeArityLNTF codeArityLNNR (codeFNN x) x0 <> 0)) by assumption. clear n; decompose record (checkPrfCorrect2 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNTFIsCorrect2 codeArityLNNRIsCorrect1 codeArityLNNRIsCorrect2 _ _ H5) /r; intros x1 H7 x2 x3 H8. assert (H6: x1 = x). { eapply codeFormulaInj. - apply H7. } cut (codePrf x2 x1 x3 = x0). * generalize x3. rewrite H6; intros x4 H9. clear H6 H8 x3 H7 x1. assert (H6: ~ (forall g : fol.Formula LNN, In g x2 -> mem (fol.Formula LNN) T g)). { unfold not in |- *; intros H6. assert (H7: SysPrf T x). { exists x2; exists x4. intros g H7; apply H6; assumption. } apply con; unfold Inconsistent in |- *. intros f; apply contradiction with x; assumption. } assert (H7: ~ (exists g : Formula, In g x2 /\ ~ mem _ T g)). { unfold not in |- *; intros H7; apply H4. rewrite (subFormulaNot LNN). unfold codeSysPrf, codeX in |- *; rewrite <- H9. apply codeSysPrfCorrect2; assumption. } clear x4 H9; induction x2 as [| a x2 Hrecx2]. -- apply H6; intros g H8; elim H8. -- assert (H8: ~ (exists g : Formula, In g x2 /\ ~ mem (fol.Formula LNN) T g)). { unfold not in |- *; intros H8; apply H7. destruct H8 as (x1, H8). exists x1; simpl in |- *; tauto. } assert (H9: ~ ~ (mem (fol.Formula LNN) T a \/ ~ mem (fol.Formula LNN) T a)) by tauto. apply H9; intros [H10| H10]. ++ apply Hrecx2. ** intros H11; apply H6. intros g [H12| H12]. { rewrite <- H12; assumption. } { apply H11; assumption. } ** assumption. ++ apply H7; exists a; simpl in |- *. split; auto. * assumption. - apply impE with (notH (substF (notH codeSysPf) 0 (codeNatToTerm.natToTermLNN codeX))). + unfold codeSysPf, codeSysPrf.codeSysPf, y in |- *. fold codeSysPrf in |- *. rewrite (subFormulaNot LNN). apply impTrans with (substF (existH 1 codeSysPrf) 0 (codeNatToTerm.natToTermLNN codeX)). * apply impI; apply nnE; apply Axm; right; constructor. * apply sysExtend with NN. -- assumption. -- apply impI; rewrite (subFormulaExist LNN). destruct (eq_nat_dec 1 0) as [e|n]. ++ discriminate e. ++ induction (In_dec eq_nat_dec 1 (freeVarT (codeNatToTerm.natToTermLNN codeX))) as [a | _]. ** elim (closedNatToTerm _ _ a). ** clear n; apply existSys. { apply closedNN. } { unfold not in |- *; intros H4. elim (in_remove_neq _ _ _ _ _ H4). reflexivity. } { apply existSimp; apply nnI. apply Axm; right; constructor. } + apply impE with (notH x). * apply cp2; apply iffE2; apply sysExtend with NN; assumption. * apply H0; assumption. 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)