proposition: Lemma prv_ind_full {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} : forall P : peirce -> list (form falsity_on) -> (form falsity_on) -> Prop, (forall (p : peirce) (A : list form) (phi psi : form), (phi :: A) ⊢ psi -> P p (phi :: A) psi -> P p A (phi → psi)) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ phi → psi -> P p A (phi → psi) -> A ⊢ phi -> P p A phi -> P p A psi) -> (forall (p : peirce) (A : list form) (phi : form), (map (subst_form ↑) A) ⊢ phi -> P p (map (subst_form ↑) A) phi -> P p A (∀ phi)) -> (forall (p : peirce) (A : list form) (t : term) (phi : form), A ⊢ ∀ phi -> P p A (∀ phi) -> P p A phi[t..]) -> (forall (p : peirce) (A : list form) (t : term) (phi : form), A ⊢ phi[t..] -> P p A phi[t..] -> P p A (∃ phi)) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ ∃ phi -> P p A (∃ phi) -> (phi :: [p[↑] | p ∈ A]) ⊢ psi[↑] -> P p (phi :: [p[↑] | p ∈ A]) psi[↑] -> P p A psi) -> (forall (p : peirce) (A : list form) (phi : form), A ⊢ ⊥ -> P p A ⊥ -> P p A phi) -> (forall (p : peirce) (A : list form) (phi : form), phi el A -> P p A phi) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ phi -> P p A phi -> A ⊢ psi -> P p A psi -> P p A (phi ∧ psi)) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ phi ∧ psi -> P p A (phi ∧ psi) -> P p A phi) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ phi ∧ psi -> P p A (phi ∧ psi) -> P p A psi) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ phi -> P p A phi -> P p A (phi ∨ psi)) -> (forall (p : peirce) (A : list form) (phi psi : form), A ⊢ psi -> P p A psi -> P p A (phi ∨ psi)) -> (forall (p : peirce) (A : list form) (phi psi theta : form), A ⊢ phi ∨ psi -> P p A (phi ∨ psi) -> (phi :: A) ⊢ theta -> P p (phi :: A) theta -> (psi :: A) ⊢ theta -> P p (psi :: A) theta -> P p A theta) -> (forall (A : list form) (phi psi : form), P class A (((phi → psi) → phi) → phi)) -> forall (p : peirce) (l : list form) (f14 : form), l ⊢ f14 -> P p l f14.
proof: Proof. intros. specialize (@prv_ind _ _ (fun ff => match ff with falsity_on => P | _ => fun _ _ _ => True end)). intros H'. apply H' with (ff := falsity_on); clear H'. all: intros; try destruct ff; trivial. all: intuition eauto 2. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia