Theorem: FOL.NV.T_13_6_no_deduct (FOL/NV/Margaris/Prop.lean)

State before:
P Q : Formula
⊢ IsProof (P.not_.imp_ (P.imp_ Q))
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ (Q.not_.imp_ P.not_))
State after:
case a
P Q : Formula
⊢ IsDeduct ∅ ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q)))

case a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ (Q.not_.imp_ P.not_))

State before:
case a
P Q : Formula
⊢ IsDeduct ∅ ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q)))
Tactic:
apply IsDeduct.mp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)))
State after:
case a.a
P Q : Formula
⊢ IsDeduct ∅
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))

case a.a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)))

State before:
case a.a
P Q : Formula
⊢ IsDeduct ∅
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a.a
P Q : Formula
⊢ IsAxiom
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))

State before:
case a.a.a
P Q : Formula
⊢ IsAxiom
    ((P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))).imp_
      ((P.not_.imp_ (Q.not_.imp_ P.not_)).imp_ (P.not_.imp_ (P.imp_ Q))))
Tactic:
apply IsAxiom.prop_2_
State after:
no goals

State before:
case a.a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)))
Tactic:
apply IsDeduct.mp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
State after:
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))

case a.a.a
P Q : Formula
⊢ IsDeduct ∅ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))

State before:
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a.a.a
P Q : Formula
⊢ IsAxiom (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))

State before:
case a.a.a.a
P Q : Formula
⊢ IsAxiom (((Q.not_.imp_ P.not_).imp_ (P.imp_ Q)).imp_ (P.not_.imp_ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))))
Tactic:
apply IsAxiom.prop_1_
State after:
no goals

State before:
case a.a.a
P Q : Formula
⊢ IsDeduct ∅ ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a.a.a
P Q : Formula
⊢ IsAxiom ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))

State before:
case a.a.a.a
P Q : Formula
⊢ IsAxiom ((Q.not_.imp_ P.not_).imp_ (P.imp_ Q))
Tactic:
apply IsAxiom.prop_3_
State after:
no goals

State before:
case a
P Q : Formula
⊢ IsDeduct ∅ (P.not_.imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
P Q : Formula
⊢ IsAxiom (P.not_.imp_ (Q.not_.imp_ P.not_))

State before:
case a.a
P Q : Formula
⊢ IsAxiom (P.not_.imp_ (Q.not_.imp_ P.not_))
Tactic:
apply IsAxiom.prop_1_
State after:
no goals