I was wondering if someone can provide a basic procedural approach when undertaking quantifier rules in an inference system (specifically for natural deduction), and a basic explanation on the restriction when using the quantifier inference rules.
=====================================================================
Side question, before main question:
Quiet confused about when books talk about "constant" and "variables" in respect to quantifiers, and quantifier inference rules.
Constant –
Formal definition:
- A constant is a number on its own, or sometimes a letter such as a, b or c to stand for a fixed number.
My understanding of a "constant" in respect to quantifiers:
- In the case quantifier this mean a single individual.
Variable –
Formal definition:
- A symbol for a number we don't know yet. It is usually a letter like x or y.
My understanding of a "variable" in respect to quantifiers:
- In the case of quantifiers this means we get to choose any individual
=====================================================================
My understanding in repeat to quantifiers rules, using my understanding of "constant" and "variable" in terms of quantifier. As shown above.
EI = Existential instantiation ( removal of existential quantifier)
- Going from a variable to a constant ?
EG = Existential generalisation ( introduction of existential quantifier)
- Going from a constant to a variable ?
UI = Universal instantiation ( removal of universal quantifier)
– Going from a variable to a constant ?
UG = Universal generalisation ( introduction of existential quantifier).
- Going from a constant to a variable ?
=====================================================================
=====================================================================
MAIN QUESTION
My understanding,below for how to go about using the quantifiers rules in natural deduction inference system :
Key for the proceeding information:
Numerator – the formula above the line.
Denominator – the formula below the line
I know it's not fraction, but wanted to make it more clear
=====================================================================
EI = Existential instantiation ( removal of existential quantifier)
Inference rule:
∃xF / F(x/e)
For the Inference rule:
Numerator part of the inference rule:
- The ∃(x) the "x" variable can be any type of variable e.g. x,y,z.Depending on what variable is inside the parenthesis of the quantifier, e.g.∃(y) the matrix beside it will have all "y" variables.
Denominator part of the inference rule:
- A new variable "e" for the F(e) is required every time you use this inference rule, i.e. cannot be the same as the a previous existential instantiation .
=====================================================================
EG = Existential generalisation ( introduction of existential quantifier)
Inference rule:
F(x/d) / ∃xF
For the Inference rule:
Numerator part of the inference rule:
- The "d" in F(d) MUST NOT come from universal instantiation , from a previous line in the inference system.
Denominator part of the inference rule:
- The F part all variable should be "x" variable as the quantifier is ∃(x).Depending on what variable is inside the parenthesis of the quantifier, e.g.∃(y) the matrix beside it will have all "y" variables.
=====================================================================
UI = Universal instantiation ( removal of universal quantifier)
Inference rule:
∀x F / F(x/d)
For the Inference rule:
Numerator part of the inference rule:
- The "F" part of ∀(x)F all variable should be "x" variable as the quantifier is ∀(x).Depending on what variable is inside the parenthesis of the quantifier, e.g.∀(y) the matrix beside it will have all "y" variables.
Denominator part of the inference rule:
- where "d" in F(d) can come from anywhere, even from previous lines.
=====================================================================
UG = Universal generalisation ( introduction of existential quantifier)
Inference rule:
F(x/d) / ∀xF
For the Inference rule:
Numerator part of the inference rule:
- The "d" part of F(d) can come from anywhere, even from previous lines.
Denominator part of the inference rule:
- The F part all variable should be "x" variable as the quantifier is ∀(x).Depending on what variable is inside the parenthesis of the quantifier, e.g.∀(y) the matrix beside it will have all "y" variables.
Thanks in advance. Any form of clarification, is highly welcomed. If you could base any answers upon "my understanding", that would be great.
Best Answer
First, I know that you know that the inference rules aren't fractions, but still ... please replace 'Numerator' and 'Denominator' with something more appropriate ... such as 'premise' and 'conclusion' respectively.
OK, the rules, and some more intuitive explanation:
Universal Instantiation
'Typical' Form:
$\forall x P(x)$
$\therefore P(a)$ for any constant $a$
Explanation:
I all things have property $P$, then of course each individual thing has property $P$, whether this is $a$, $b$, ... This is why there are no restrictions here.
Universal Generalization
'Typical' Form:
$P(a)$ ... where $a$ has been introduced as some arbitrary object!
$\therefore \forall x P(x)$
Explanation:
Suppose we have a constant that we are using to denote a specific object, e.g. suppose we use the constant $c$ for 'Charlie', and suppose we have as a given that $Dog(c)$, since we know that Charlie is a dog. Now, clearly we should not be able to infer that everything is a dog just because Charlie is a dog. And that is why we mandate the constant $a$ in the rule to be a temporary name that we use to denote "some arbitrary object from our domain ... let's call it $a$" In fact, many systems require you to explicitly introduce this constant ... it would be the formal logical equivalent to the mathematician's "consider any object $a$".
I must say that in your description off the rule this requirement is not clear. ... so if you don't understand the rule as you yourself stated, I can understand that!
Here is a formal proof example:
$\forall x P(x)$ Premise
$\forall x Q(x)$ Premise
$\qquad a$ (here is where we introduce $a$ ... so we have to make sure that $a$ is not used earlier in the proof, i.e. it is a 'new' constant. Again, this is the equivalent of saying "let's consider any arbitrary object $a$. I use the indentation to create a temporary context for the use of this $a$ ... some systems use subproofs to do this)
$\qquad P(a)$ Universal Instantiation 1 (as we saw, this works for any constant, so also for $a$)
$\qquad Q(a)$ Universal Instantiation 2
$\qquad P(a) \land Q(a)$ Conjunction 4,5
$\forall x (P(x) \land Q(x))$ Universal Generalization 6 (or: 3 through 6) (so why can we do this? Because $a$ was used as an arbitrary constant!)
Existential Generalization
'Typical' Form:
$P(a)$
$\therefore \exists x P(x)$
Explanation:
Like Universal Instantiation, Existential Generalization should really be without any restrictions: If $a$ has property $P$, then there is something that has property $P$, whether $a$ is used to denote a specific or arbitrary object.
So here I am not sure why there is this restriction stated in your description of the rule...
Existential Instantiation
'Typical' Form:
$\exists x P(x)$
$\therefore P(a)$ ... for a new constant $a$
Explanation:
OK, so in this rule we do have to treat $a$ very carefully! Think about it: you know that something has property $P$ .. but do you know what it is? No. So, what the $a$ is representing here, is "some object that has property P ... which we know exists ... but we don't know what specific object it is ... so let's call it $a$". And again, like Universal Generalization, it is best to contrast the correct use of this rule with an incorrect one: Again, suppose we use constant $c$ to denote a specific individual: Charlie. Now, suppose we know that $\exists Dog(x)$ ... can we now infer $Dog(c)$? No! Because even though we know something is a dog, we don't know whether Charlie is a dog. So, like Universal Generalization, the $a$ represents an unknown object, but this time, we do know that $a$ has property $P$. And that also means that $a$ is not a completely arbitrary object .. meaning that we can't use it for a Universal Generalization.
Example:
$\exists x P(x)$ Premise
$\forall x (P(x) \rightarrow Q(x))$
$P(a)$ Existential Elimination (OK use of rule, since $a$ is a new constant)
$P(a) \rightarrow Q(a)$ Universal Instantiation 2
$Q(a)$ Modus Ponens 3,4
$\exists x Q(x)$ Existential Generalization 5
Note that we had to do line 3 before line 4, because if we would have first instantiated the universal with $a$, then we could not have instantiated the existential with that same $a$, since the $a$ is on longer a new constant!