Re: [isabelle] Metalogical "spec" not resolved automatically


the problem in both cases has to do with the scopes of meta-quantification. These binders extend over the entire sequent. For example, the first sequent

  1. !! N. [| 0 < N; P N |] ==> P (Suc 0)

requires to prove P(1) just from knowing that P(n) holds for some positive n; it is analogous to the formula

  ALL n. (0 < n & P(n) --> P(1))          (*)

This formula is not satisfied by a model where you have, say, P(2), but not P(1). In fact, (*) is equivalent to the formula

  (EX n. 0<n & P(n)) --> P(1)

by standard quantifier equivalences of first-order logic.

I suppose that what you really want is the sequent

  1. (!! N. 0 < N ==> P N) ==> P (Suc 0)

which would indeed be trivial?

The explanation for the second subgoal is similar.



Nicole Rauch wrote:
Hello Isabelle-users,

I'm stuck with a logical problem and I don't see why it is not trivial to Isabelle. These are my two subgoals:

1. !! N. [| 0 < N; P N |] ==> P (Suc 0)
2. !! N. [| 0 < N; P N; 0 < M |] ==> P M

If P holds for all arguments greater than zero, then it should hold for a fixed argument which is greater than zero. This is basically HOL's spec lemma, just with metalogical quantification instead of HOL quantification. But Isabelle refuses to accept this. What am I overlooking here?

Thanks for any insights


PS: This is the full Isabelle output with types, sorts and brackets activated:

goal (show, 2 subgoals):
1. (\<And>(N\<Colon>nat). (\<lbrakk>((0\<Colon>nat) < N); (P N) \<rbrakk> \<Longrightarrow> (P (Suc (0\<Colon>nat))))) 2. (\<And>(N\<Colon>nat). (\<lbrakk>((0\<Colon>nat) < N); (P N); ((0 \<Colon>nat) < M)\<rbrakk> \<Longrightarrow> (P M)))
  P :: (nat \<Rightarrow> bool)
  M :: nat

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.