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

State before:
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ Q
Tactic:
apply IsDeduct.mp_ (exists_ v P)
State after:
case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((exists_ v P).imp_ Q)

case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (exists_ v P)

State before:
case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((exists_ v P).imp_ Q)
Tactic:
apply IsDeduct.mp_ (forall_ v (P.imp_ Q))
State after:
case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))

case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (forall_ v (P.imp_ Q))

State before:
case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))
Tactic:
apply proof_imp_deduct
State after:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))

State before:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsProof ((forall_ v (P.imp_ Q)).imp_ ((exists_ v P).imp_ Q))
Tactic:
exact T_17_11 P Q v h4
State after:
no goals

State before:
case a.a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (forall_ v (P.imp_ Q))
Tactic:
apply generalization
State after:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (P.imp_ Q)

case a.a.h2
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ ∀ H ∈ Δ, ¬isFreeIn v H

State before:
case a.a.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (P.imp_ Q)
Tactic:
apply deduction_theorem
State after:
case a.a.h1.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct (Δ ∪ {P}) Q

State before:
case a.a.h1.h1
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct (Δ ∪ {P}) Q
Tactic:
exact h2
State after:
no goals

State before:
case a.a.h2
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ ∀ H ∈ Δ, ¬isFreeIn v H
Tactic:
exact h3
State after:
no goals

State before:
case a
P Q : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ (exists_ v P)
h2 : IsDeduct (Δ ∪ {P}) Q
h3 : ∀ H ∈ Δ, ¬isFreeIn v H
h4 : ¬isFreeIn v Q
⊢ IsDeduct Δ (exists_ v P)
Tactic:
exact h1
State after:
no goals