Need proof for meta-logic conjunction elimination rule

1
votes

Here, I ask for a proof of a Isabelle meta-logic conjunction elimination rule.

The source below contains comments of mine which explain a little of what I'm doing. In the theory, there are two pairs of a meta-false definition and conjunction elimination rule. The two pairs are the following:

  • falseH, andH_E1, and
  • falseM, andM_E1.

The form of my andM conjunction is (P ==> Q ==> falseM) ==> falseM), and it's this form for which I cannot get an easy proof.

In the future, I plan on duplicating the HOL.thy natural deduction rules using meta-logic operators which will be similar to the andM above. As part of that, the operator ==> will be treated as a primitive operator. Because the Pure operator !! is also primitive in the same sense as ==>, I'm guessing that I may not be able to develop rules which will help me with the meta-false definition, !!P. PROP P, as I use it below. I could be wrong, though.

It's not like I have to have the falseM I try to use below, because falseH is conducive to the simp magic that already works in conjunction with HOL, pun not intended. Though I don't have to have it, having it would be good.

theory i131210a__SO_question_andM_elim
imports Complex_Main 
begin

(*This is conjunct1 from HOL.thy, line 426. Someday, I'll get rules to  
  use by duplicating the HOL rules as meta-logic rules, but my question 
  here is about proving andM_E1 below with what's already available.*)
lemma conjunct1_from_HOL: 
  "[| P & Q |] ==> P"
by(unfold and_def, iprover intro: impI dest: spec mp)

(*Using bool for falseH allows the auto magic to work for andH_E1.*)
definition falseH :: "prop" ("falseH") where
  "falseH == (!!P. P::bool)"

theorem andH_E1: 
  "((P ==> Q ==> falseH) ==> falseH) ==> P"
by(unfold falseH_def, auto)

(*Using Pure &&&, auto-tools work too, but I want a different meta-and.*)
theorem mand_E1: 
  "(P &&& Q) ==> P"
by(linarith)

(*Here I define a pure meta-false. That's what I want, if I can get it.*)
definition falseM :: "prop" ("falseM") where
  "falseM == (!!P. PROP P)"

(*But here, I need an IsaMagician to do what may be easy, or may be hard.
  A proof for this might give me a good template to follow.*)  
theorem andM_E1: 
  "((P ==> Q ==> falseM) ==> falseM) ==> P"
  apply(unfold falseM_def)
oops

end

Update (131211)

I update this with three things, where two of them are related to Andreas' answer that an axiom of excluded middle is needed. What I say below is not really an answer to anything, and it's open to more comments, since I can be wrong on simple things.

I put my lengthy comments in here to consolidate some ideas related to the core idea of my question, which is how to use a meta-logic false to define meta-logic operators.

  1. I show how I think I would add a meta-logic axiom of excluded middle in a locale.
  2. I show what led to me understanding what form of an axiom of excluded middle I need. Most all the literature will say that an excluded middle is P or not P, which is deceptive, since I rarely think about an excluded middle, because it is ingrained my thinking.
  3. I note that "(P &&& Q) ==> P is proved by conjunctionD1 in conjunction.ML, and an unfolded version is proved using meta_allE. I wonder why andM, with !! on the inside rather than outside, can't be manipulated so that it can be proved.

Putting a Meta-Logic Excluded Middle in a Locale

So Adreas saved me many months, probably at least a year, and possibly many years of fruitless scheming by pointing out that Isabelle/Pure doesn't have an excluded middle, and that I need it. This has helped answer related questions I had, and helps make more sense to me what Isabelle/Pure is.

If using the HOL excluded middle is forced on me, I would just use False, instead of (!!P. P::bool).

If I want a meta-false, I think I would add a meta-logic excluded middle in a locale like this:

abbreviation (input) trueM :: "prop" ("trueM") where
  "trueM == (falseM ==> falseM)"

locale pure_with_em =
  assumes t_or_f: "((P == trueM) ==> falseM) ==> (P == falseM)"
begin
theorem andM_E1:
  "((P ==> Q ==> falseM) ==> falseM) ==> P"
unfolding falseM_def
oops
end

Like I said, this is not an answer because I would have to work it out.

From the proof that Andreas provided, there is classical from HOL:

lemma classical: 
  assumes prem: "~P ==> P" shows "P"
apply (rule True_or_False [THEN disjE, THEN eqTrueE])
...

The proof steps of HOL theorems like this tell me what I need for meta-logic versions. I did the easy part by providing the locale axiom t_or_f. The rest is just plain ole work.

Isabelle/Pure Not Having an Excluded Middle

Here, I don't talk just to talk, which I do at times, but I put in what I worked through to see that == is needed as part of an excluded middle. I could need to look at all this again, so maybe it won't be held against me.

First, jumping ahead of what I say next about the HOL lemma excluded_middle, a person, me in particular, would also want to be thinking about this HOL.thy axiom, line 171: 

True_or_False: "(P = True) | (P = False)".

Andreas points out that the law of excluded middle is needed, and that Pure does not provide it. This is the HOL.thy theorem named excluded_middle, line 604:

lemma excluded_middle: "~P | P" by (iprover intro: disjCI)

Analogously, I state this as a meta-logic theorem using falseM, where my meta-or is (P ==> falseM) ==> Q, and meta-not is P ==> falseM.

theorem 
  "(P ==> falseM) ==> (P ==> falseM)"
by(simp)

If meta-or notation is defined to obscure what it actually is, a logical novice (not me of course) might not recognize this as "if P is false then P is false", rather than what's needed, "if P is not false, then it must be true".

Update (131213): I put this in because I can forget why I did something, then when I try to work back through the logic, I think I messed up big time, when I didn't, though my logical awareness may not have been complete.

I didn't actually implement a meta-logic version of ~P | P, but of P | ~P. If it's not obvious, which it probably is, I'm using a truth table based definition of implication along with DeMorgan's laws, and using the basic theorems of logic, which ultimately must be true for me.

However, I'm now working with hindsight in regards to the axiom of excluded middle, which makes the fact that I used P | ~P less acceptable, since it becomes "((P ==> falseM) ==> falseM) ==> P", which involves double negation, which I vaguely remember is related to all this. Until now, I've never in my life ever had to concern myself with the excluded middle. That's supposed to be what constructivists think about.

It's actually fortuitous that I made the switch, because that took me to seeing the significance of = in True_or_False.

A meaningful theorem would be "not (P and not P)" (or would it?). So I substitute (P ==> falseM) for Q in the meta-and expression (P ==> Q ==> falseM) ==> falseM.

theorem 
  "((P ==> (P ==> falseM) ==> falseM) ==> falseM) ==> falseM"
by(auto,assumption)

This has gone into full play-the-logical-fool red alert, because falseM didn't have to be expanded. Now, I state the same theorem, but without bool variables and without falseM, to make explicit that it has nothing to do with falseM or bool.

theorem 
  "((PROP P ==> (PROP P ==> PROP Q) ==> PROP Q) ==> PROP Q) ==> PROP Q"
by(erule Pure.cut_rl Pure.meta_impE Pure.meta_mp, assumption)

Back to what I jumped ahead to at the beginning, I see now that a key difference is that operator = is being used in True_or_False.

Now, I state a meta-logic form of True_or_False which uses operator ==, with meta-or as (P ==> falseM) ==> Q, the true part as (P == (falseM ==> falseM)), and the false part as (P == falseM).

theorem 
  "((P == (falseM ==> falseM)) ==> falseM) ==> (P == falseM)"
apply(unfold falseM_def)
oops

This finally got me a meaningful meta-logic statement of the excluded middle, in which falseM needs to be expanded. I can't prove this, which means nothing in itself, or disprove it, which means I could be totally confused.

This demonstrates why I have to study a lot of low-level logic to work with theorem assistants, when my end goal is high-level mathematics, which traditionally doesn't require this kind of knowledge.

Not having a good understanding of the significance of no excluded middle ended up killing me, among other things.

Why Can "(P &&& Q) ==> P" Be Proved Above?

There is still the significance that (P &&& Q) ==> P can be proved by the methods linarith and presburger above, where &&& in pure_thy.ML is this:

"(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)"

My meta-and, using falseM, actually just moves the use of !! from the outside to the inside, once falseM has been expanded.

Here, I prove expanded terms of meta-and elimination, and prove an unexpanded version of it using Pure.conjunctiond1.

theorem 
  "(PROP P &&& PROP Q) ==> PROP P" 
apply(unfold Pure.conjunction_def)
by(erule Pure.meta_allE, assumption)

theorem expanded_and_1: 
  "(!!R. (PROP P ==> PROP Q ==> PROP R) ==> PROP R) ==> PROP P"
by(erule Pure.meta_allE, assumption)

theorem 
  "(PROP P &&& PROP Q) ==> PROP P"
by(erule Pure.conjunctionD1)

The rule conjunctionD1 is in conjunction.ML, and it appears that forall_elim_vars is taking care of the operator !!, which I suppose is just doing the same thing as meta_allE.

I Could Use the Standard Meta-And, but Meta-And Is Not the Goal

I compare two expanded versions of the conjunction elimination rule. The first term uses the standard &&&, and the second term uses my andM.

term "(!!R. (P ==> Q ==> PROP R) ==> PROP R) ==> P"
term "((P ==> Q ==> (!!P. PROP P)) ==> (!!P. PROP P)) ==> P"

Using &&& allows the first term to be proved easily with meta_allE, as shown above.

It seems to me, I should be able to manipulate the second term into the form of the first term, but I wouldn't know. If that's true, then I don't need to add an axiom of excluded middle for this theorem. I'll know after studying a lot of natural deduction, like I need to.

If my goal was just meta-logic operators, I'd use &&&, but that's not my goal. My goal is to define a meta-false to use to abbreviate meta-logic operators. I'm trying to slightly expand the natural deduction framework of Isabelle/Pure, not duplicate all of HOL.

The main value I've gotten from this question is that I now know I need to be on the lookout for the need for an axiom of excluded middle. If I want a meta-false, then it seems I will need an axiom of excluded middle.

This is where I leave off. Thanks for the help, and please pardon the lengthy additions.

1
isabelle

1 Answers

1
votes

As a first step, you can prove the HOL version andH_E1 without using any proof tools, just plain rule, subst, and assumption. Then, you should be able to see whether you can translate your proof to andM_E1 and how to do so. I found the following proof for andH_E1:

theorem andH_E1: "((P ==> Q ==> falseH) ==> falseH) ==> P"
unfolding falseH_def
apply(rule classical)
apply(erule meta_allE)
apply(erule meta_impE)
apply(erule notE)
apply assumption
apply assumption
done

As you can see, the first step applies the rule classical, i.e., my proof works only in classical logic. However, Pure is weaker than classical logic, because there is no axiom of excluded middle. Hence, you will not be able to transfer this proof to andM_E1. You can try to find a proof of andH_E1 that does not rely on the classical axioms, but I doubt that you will find one; at least iprover does not. Otherwise, you cannot prove this theorem with Pure means only unless you introduce the axiom of excluded middle to Pure.

As excluded middle is equivalent to the classical axiom (you can derive the one from the other), the easiest way to go is probably to add the classical axiom directly, e.g., in a locale as you suggested. Then, the proof goes as follows, where I write Pure negation as _ ==> falseM.

locale classical =
  assumes pure_classical: "((PROP P ==> falseM) ==> PROP P) ==> PROP P"
begin

theorem andM_E1: 
  "((PROP P ==> PROP Q ==> falseM) ==> falseM) ==> PROP P"
unfolding falseM_def
apply(rule pure_classical)
apply(erule meta_allE)
apply(erule meta_impE) back
apply(erule (1) meta_impE)
apply(unfold falseM_def)
apply(assumption)
apply(assumption)
done

end