1

The universal quantifier in first-order logic (the symbol is ∀) and meta-universal quantifier in meta-logic (the symbol is ⋀) what is the main difference? For the following two lemmas, the first example proves successful using universal quantifiers, while the meta-universal quantifiers do not.

lemma "∀ x. P x ⟹ P 0"
  apply simp
  done

lemma "⋀ x. P x ⟹ P 0"
  oops

Image of my Isabelle code

dbc
  • 104,963
  • 20
  • 228
  • 340
hahahahaha-sh
  • 11
  • 1

1 Answers1

4

Isabelle is a generic framework for interactive theorem proving. Its meta-logic Isabelle/Pure allows to define a broad range of object-logics, one of them being Isabelle/HOL. As you already hinted, the symbol ∀ is Isabelle/HOL's universal quantifier and the symbol ⋀ is Isabelle/Pure's universal quantifier. Also, the symbol ⟹ is Isabelle/Pure's implication. The operator precedence rules state that ⋀ has lower precedence than ⟹, and ∀ has higher precedence than ⋀ and ⟹. Therefore ⋀ x. P x ⟹ P 0 is actually parsed as ⋀ x. (P x ⟹ P 0) (which clearly doesn't hold) instead of (⋀ x. P x) ⟹ P 0, so you need to explicitly parenthesize the proposition ⋀ x. P x. Then, your lemma can be trivially proved using the usual elimination rule for ⋀ in natural deduction as follows:

lemma "(⋀ x. P x) ⟹ P 0"
  by (rule meta_spec)

In order to try to avoid this kind of nuances, I'd suggest you to adopt the Isabelle/Isar style for stating your lemmas, namely the following:

lemma
  assumes "⋀ x. P x"
  shows "P 0"
  using assms by (rule meta_spec)

Please refer to Programming and Proving in Isabelle/HOL and The Isabelle/Isar Reference Manual for more information.

Javier Díaz
  • 1,071
  • 4
  • 7