Stream: Beginner Questions

Topic: How is this schematic goal provable by assumption?

o7 (Dec 22 2024 at 04:54):

schematic_goal ‹∀x. ¬ R x ⟶ R (F x) ⟹ ¬ R (F (F ?x2)) ⟹ R (F (F (F ?x2))) ⟹ R (F (F ?x17))›
by assumption

My understanding is that ?x2 and ?x17 are functions that don't contain any free variables. With this in mind I can't see how the goal can just be proven by assumption. Is my understanding incorrect?
But it seems that Isabelle is just able to choose

goal instantiation:
    ?x17 ↝ F ?x2

but F is a free variable/predicate/etc. Why is it able to use F here?

Jan van Brügge (Dec 22 2024 at 11:20):

You can think of free variables as implicitly bound at the top-level. As such they are "in-scope" for the schematic variables. If you change your goal to explicitly bind them, they will no longer be able to unify:

schematic_goal ‹⋀F. ∀x. ¬ R x ⟶ R (F x) ⟹ ¬ R (F (F ?x2)) ⟹ R (F (F (F ?x2))) ⟹ R (F (F ?x17))›

Last updated: Feb 01 2025 at 20:19 UTC