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

Nicole,

`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.
Best,
Stephan
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
Nicole

`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)))
`variables:
P :: (nat \<Rightarrow> bool)
M :: nat

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