Theorem: FOL.NV.isProofAltImpIsDeduct (FOL/NV/Margaris/Fol.lean)

State before:
F : Formula
h1 : IsProofAlt F
⊢ IsDeduct ∅ F
Tactic:
induction h1
State after:
case prop_true_
F : Formula
⊢ IsDeduct ∅ true_

case prop_1_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ (phi✝.imp_ (psi✝.imp_ phi✝))

case prop_2_
F phi✝ psi✝ chi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.imp_ (psi✝.imp_ chi✝)).imp_ ((phi✝.imp_ psi✝).imp_ (phi✝.imp_ chi✝)))

case prop_3_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.not_.imp_ psi✝.not_).imp_ (psi✝.imp_ phi✝))

case pred_1_
F : Formula
v✝ : VarName
phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((forall_ v✝ (phi✝.imp_ psi✝)).imp_ ((forall_ v✝ phi✝).imp_ (forall_ v✝ psi✝)))

case pred_2_
F : Formula
v✝ t✝ : VarName
phi✝ phi'✝ : Formula
a✝¹ : fastAdmits v✝ t✝ phi✝
a✝ : fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ IsDeduct ∅ ((forall_ v✝ phi✝).imp_ phi'✝)

case pred_3_
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : ¬isFreeIn v✝ phi✝
⊢ IsDeduct ∅ (phi✝.imp_ (forall_ v✝ phi✝))

case eq_1_
F : Formula
v✝ : VarName
⊢ IsDeduct ∅ (forall_ v✝ (eq_ v✝ v✝))

case eq_2_pred_const_
F : Formula
name✝ : PredName
n✝ : ℕ
xs✝ ys✝ : Fin n✝ → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn xs✝)
      (Forall_ (List.ofFn ys✝)
        ((And_ (List.ofFn fun i => eq_ (xs✝ i) (ys✝ i))).imp_
          ((pred_const_ name✝ (List.ofFn xs✝)).iff_ (pred_const_ name✝ (List.ofFn ys✝))))))

case eq_2_eq_
F : Formula
x_0✝ x_1✝ y_0✝ y_1✝ : VarName
⊢ IsDeduct ∅
    (forall_ x_0✝
      (forall_ x_1✝
        (forall_ y_0✝
          (forall_ y_1✝ (((eq_ x_0✝ y_0✝).and_ (eq_ x_1✝ y_1✝)).imp_ ((eq_ x_0✝ x_1✝).iff_ (eq_ y_0✝ y_1✝)))))))

case gen_
F : Formula
v✝ : VarName
phi✝ : Formula
a✝ : IsProofAlt phi✝
a_ih✝ : IsDeduct ∅ phi✝
⊢ IsDeduct ∅ (forall_ v✝ phi✝)

case mp_
F phi✝ psi✝ : Formula
a✝¹ : IsProofAlt (phi✝.imp_ psi✝)
a✝ : IsProofAlt phi✝
a_ih✝¹ : IsDeduct ∅ (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct ∅ phi✝
⊢ IsDeduct ∅ psi✝

case def_false_
F : Formula
⊢ IsDeduct ∅ (false_.iff_ true_.not_)

case def_and_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)

State before:
F : Formula
⊢ IsDeduct ∅ true_
Tactic:
case prop_true_ =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_true_
State after:
no goals

State before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_1_ h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_1_
State after:
no goals

State before:
F h1_phi h1_psi h1_chi : Formula
⊢ IsDeduct ∅ ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
case prop_2_ h1_phi h1_psi h1_chi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_2_
State after:
no goals

State before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
case prop_3_ h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.prop_3_
State after:
no goals

State before:
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Tactic:
case pred_1_ h1_v h1_phi h1_psi =>
  apply IsDeduct.axiom_
  apply IsAxiom.pred_1_
State after:
no goals

State before:
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsDeduct ∅ ((forall_ h1_v h1_phi).imp_ h1_phi')
Tactic:
case pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1 =>
  apply IsDeduct.axiom_
  exact IsAxiom.pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1
State after:
no goals

State before:
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsDeduct ∅ (h1_phi.imp_ (forall_ h1_v h1_phi))
Tactic:
case pred_3_ h1_v h1_phi h1_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.pred_3_
  exact h1_1
State after:
no goals

State before:
F : Formula
h1 : VarName
⊢ IsDeduct ∅ (forall_ h1 (eq_ h1 h1))
Tactic:
case eq_1_ h1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.eq_1_
State after:
no goals

State before:
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Tactic:
case eq_2_pred_const_ h1_name h1_n h1_xs h1_ys =>
  apply IsDeduct.axiom_
  apply IsAxiom.eq_2_pred_const_
State after:
no goals

State before:
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsDeduct ∅
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Tactic:
case eq_2_eq_ h1_x_0 h1_y_0 h1_x_1 h1_y_1 =>
  apply IsDeduct.axiom_
  apply IsAxiom.eq_2_eq_
State after:
no goals

State before:
F h1_phi h1_psi : Formula
h1_1 : IsProofAlt (h1_phi.imp_ h1_psi)
h1_2 : IsProofAlt h1_phi
h1_ih_1 : IsDeduct ∅ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_psi
Tactic:
case mp_ h1_phi h1_psi h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
State after:
no goals

State before:
case def_false_
F : Formula
⊢ IsDeduct ∅ (false_.iff_ true_.not_)

case def_and_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.and_ psi✝).iff_ (phi✝.imp_ psi✝.not_).not_)

case def_or_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅ ((phi✝.or_ psi✝).iff_ (phi✝.not_.imp_ psi✝))

case def_iff_
F phi✝ psi✝ : Formula
⊢ IsDeduct ∅
    (((phi✝.iff_ psi✝).imp_ ((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_).imp_
        (((phi✝.imp_ psi✝).imp_ (psi✝.imp_ phi✝).not_).not_.imp_ (phi✝.iff_ psi✝)).not_).not_

case def_exists_
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Tactic:
all_goals
  sorry
State after:
no goals

State before:
F : Formula
⊢ IsDeduct ∅ true_
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
⊢ IsAxiom true_

State before:
case a
F : Formula
⊢ IsAxiom true_
Tactic:
apply IsAxiom.prop_true_
State after:
no goals

State before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom (h1_phi.imp_ (h1_psi.imp_ h1_phi))

State before:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom (h1_phi.imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsAxiom.prop_1_
State after:
no goals

State before:
F h1_phi h1_psi h1_chi : Formula
⊢ IsDeduct ∅ ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F h1_phi h1_psi h1_chi : Formula
⊢ IsAxiom ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))

State before:
case a
F h1_phi h1_psi h1_chi : Formula
⊢ IsAxiom ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
Tactic:
apply IsAxiom.prop_2_
State after:
no goals

State before:
F h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))

State before:
case a
F h1_phi h1_psi : Formula
⊢ IsAxiom ((h1_phi.not_.imp_ h1_psi.not_).imp_ (h1_psi.imp_ h1_phi))
Tactic:
apply IsAxiom.prop_3_
State after:
no goals

State before:
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsDeduct ∅ ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsAxiom ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))

State before:
case a
F : Formula
h1_v : VarName
h1_phi h1_psi : Formula
⊢ IsAxiom ((forall_ h1_v (h1_phi.imp_ h1_psi)).imp_ ((forall_ h1_v h1_phi).imp_ (forall_ h1_v h1_psi)))
Tactic:
apply IsAxiom.pred_1_
State after:
no goals

State before:
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsDeduct ∅ ((forall_ h1_v h1_phi).imp_ h1_phi')
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsAxiom ((forall_ h1_v h1_phi).imp_ h1_phi')

State before:
case a
F : Formula
h1_v h1_t : VarName
h1_phi h1_phi' : Formula
h1_1 : fastAdmits h1_v h1_t h1_phi
h1_ih_1 : fastReplaceFree h1_v h1_t h1_phi = h1_phi'
⊢ IsAxiom ((forall_ h1_v h1_phi).imp_ h1_phi')
Tactic:
exact IsAxiom.pred_2_ h1_v h1_t h1_phi h1_phi' h1_1 h1_ih_1
State after:
no goals

State before:
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsDeduct ∅ (h1_phi.imp_ (forall_ h1_v h1_phi))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsAxiom (h1_phi.imp_ (forall_ h1_v h1_phi))

State before:
case a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ IsAxiom (h1_phi.imp_ (forall_ h1_v h1_phi))
Tactic:
apply IsAxiom.pred_3_
State after:
case a.a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ ¬isFreeIn h1_v h1_phi

State before:
case a.a
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : ¬isFreeIn h1_v h1_phi
⊢ ¬isFreeIn h1_v h1_phi
Tactic:
exact h1_1
State after:
no goals

State before:
F : Formula
h1 : VarName
⊢ IsDeduct ∅ (forall_ h1 (eq_ h1 h1))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
h1 : VarName
⊢ IsAxiom (forall_ h1 (eq_ h1 h1))

State before:
case a
F : Formula
h1 : VarName
⊢ IsAxiom (forall_ h1 (eq_ h1 h1))
Tactic:
apply IsAxiom.eq_1_
State after:
no goals

State before:
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsDeduct ∅
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsAxiom
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))

State before:
case a
F : Formula
h1_name : PredName
h1_n : ℕ
h1_xs h1_ys : Fin h1_n → VarName
⊢ IsAxiom
    (Forall_ (List.ofFn h1_xs)
      (Forall_ (List.ofFn h1_ys)
        ((And_ (List.ofFn fun i => eq_ (h1_xs i) (h1_ys i))).imp_
          ((pred_const_ h1_name (List.ofFn h1_xs)).iff_ (pred_const_ h1_name (List.ofFn h1_ys))))))
Tactic:
apply IsAxiom.eq_2_pred_const_
State after:
no goals

State before:
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsDeduct ∅
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsAxiom
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))

State before:
case a
F : Formula
h1_x_0 h1_y_0 h1_x_1 h1_y_1 : VarName
⊢ IsAxiom
    (forall_ h1_x_0
      (forall_ h1_y_0
        (forall_ h1_x_1
          (forall_ h1_y_1
            (((eq_ h1_x_0 h1_x_1).and_ (eq_ h1_y_0 h1_y_1)).imp_ ((eq_ h1_x_0 h1_y_0).iff_ (eq_ h1_x_1 h1_y_1)))))))
Tactic:
apply IsAxiom.eq_2_eq_
State after:
no goals

State before:
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ (forall_ h1_v h1_phi)
Tactic:
apply generalization
State after:
case h1
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_phi

case h2
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ ∀ H ∈ ∅, ¬isFreeIn h1_v H

State before:
case h1
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_phi
Tactic:
exact h1_ih
State after:
no goals

State before:
case h2
F : Formula
h1_v : VarName
h1_phi : Formula
h1_1 : IsProofAlt h1_phi
h1_ih : IsDeduct ∅ h1_phi
⊢ ∀ H ∈ ∅, ¬isFreeIn h1_v H
Tactic:
simp
State after:
no goals

State before:
F h1_phi h1_psi : Formula
h1_1 : IsProofAlt (h1_phi.imp_ h1_psi)
h1_2 : IsProofAlt h1_phi
h1_ih_1 : IsDeduct ∅ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct ∅ h1_phi
⊢ IsDeduct ∅ h1_psi
Tactic:
exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
State after:
no goals

State before:
case def_exists_
F : Formula
v✝ : VarName
phi✝ : Formula
⊢ IsDeduct ∅ ((exists_ v✝ phi✝).iff_ (forall_ v✝ phi✝.not_).not_)
Tactic:
sorry
State after:
no goals