Universal Quantifier Intro: Natural Deduction in Predicate Logic

[Mathelogician]

In Natural deduction in Predicate logic we have a rule which says [assume the set of hypotheses to be H)

if H implies phi(x) then H implies [for all x phi(x)] such that x doesn't belong to FV(psi) for all psi in H [indeed such that x occurs free in no one of formulas in H]

In other words, if we want to proof a universal quantified formula, we need only to prove the formula without any quantifier (x occurs free in all hypotheses ; or arbitrarily chosen in other words) and then assert it in (universally) quantified form.

Now i need an example of real case in math. For example let the structure contain the set R\{0} of real numbers without 0 and the natural ordering < ; we want to prove : for all x x^2>0.

Now i don't get what 'the occurrence of x as free' means here when we aim to prove the theorem for an arbitrary x [ I myself tried to solve it for two cases x>0 and x<0 ; but i know that here we have x as free in both hypotheses! ]
Anyway I'm a bit confused about the real application of the rule; And any help is welcome!
Regards

 

[Evgeny.Makarov]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

Now i need an example of real case in math. For example let the structure contain the set R\{0} of real numbers without 0 and the natural ordering < ; we want to prove : for all x x^2>0.

First, you are asking for an example of an application of an inference rule, i.e., an example of a derivation, but derivations have nothing to do with structures. Derivations are purely symtactic objects (trees of formulas), while structures are about semantics: they determine truth values of formulas. The relationship between syntax and semantics is established by the soundness and completeness theorems, but these are very different things.

Almost all universal statements that are not proved by induction are proved using universal introduction $({\forall}I)$. (And inductive steps, as universal statements, are usually proved by $({\forall}I)$.) We can indeed derive $\forall x\,(x\ne0\to x^2>0)$ from the axioms of ordered rings. We fix an arbitrary $x$, assume $x\ne 0$ and use it to derive $x^2>0$. Now, at this point we cannot apply universal introduction because $x$ occurs free in the assumption $x\ne0$. If we did apply $({\forall}I)$ followed by implication introduction at this point, we would get $x\ne0\to\forall x\,x^2>0$. Now we can change the name of the bound variable to $y$ and apply $({\forall}I)$ again to get $\forall x\,(x\ne0\to\forall y\,y^2>0)$. This formula is equivalent (using pure logic) to $(\exists x\,x\ne0)\to\forall y\,y^2>0$, which is obviously false.

The correct way is to first apply inplication introduction to close the assumption $x\ne0$ and to get $x\ne0\to x^2>0$. Now there are no more open assumptions (except universally quantified ordered ring axioms), so we can apply $({\forall}I)$ to get $\forall x\,(x\ne0\to x^2>0)$, as required.

 

[Mathelogician]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

Perfect!
Just a 2questions:
1- Is the tactic (which here for example comes from the axioms of the structure) to reach phi, included in the inference tree? Or we just use the tactic outside of the tree and then just use the resulting phi and continue to make the inference?

2- FORMALLY,the condition to use the universal introduction rule is that x occurs free in no one of the hypotheses. But how we believe this is happened when we are canceled the hypotheses that x occurs free in?!

Thanks anyway!

 

[Evgeny.Makarov]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

1- Is the tactic (which here for example comes from the axioms of the structure) to reach phi, included in the inference tree? Or we just use the tactic outside of the tree and then just use the resulting phi and continue to make the inference?

If you want a complete derivation, then it must include every relevant application of inference rules, inluding those that use axioms.

2- FORMALLY,the condition to use the universal introduction rule is that x occurs free in no one of the hypotheses. But how we believe this is happened when we are canceled the hypotheses that x occurs free in?!

The condition is that the variable being generalized does not occur in open assumptions at the moment when the universal introduction rule is applied. Before that, the variable can, of course, occur in open assumptions. Those assumptions have to be closed before the application of universal introduction.

 

[Mathelogician]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

The condition is that the variable being generalized does not occur in open assumptions at the moment when the universal introduction rule is applied. Before that, the variable can, of course, occur in open assumptions. Those assumptions have to be closed before the application of universal introduction.

I mean how these two assertions are the same?
1-The variable x does not occur free in elements of H. 2- those hypotheses which contain x as a free variable, get canceled before using the universal introduction rule.
Thanks.

 

[Evgeny.Makarov]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

I mean how these two assertions are the same?
1-The variable x does not occur free in elements of H. 2- those hypotheses which contain x as a free variable, get canceled before using the universal introduction rule.

I assume 1 also talks about the moment of application of the universal introduction rule. Statement 1 is the official condition of applying the universal introduction rule. One way to ensure it is to cancel hypotheses that contain $x$ free as described in 2. The other is to have $x$ never occur free in the hypotheses in the first place.

 

[Mathelogician]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

One way to ensure it is to cancel hypotheses that contain $x$ free as described in 2.

I mean: how do we ensure this?!

 

[Evgeny.Makarov]

Re: A question on 'universal quantifier Intriduction' rule in Natural deduction of Predicate logic

My guess is that you are missing some parts of the definition of natural deduction derivations (possibly you are not clear on what open hypotheses are). In addition, there are probably some translation issues. I am not sure I understand your last several questions.

2- FORMALLY,the condition to use the universal introduction rule is that x occurs free in no one of the open (E.M.) hypotheses. But how we believe this is happened when we are canceled the hypotheses that x occurs free in?!

It's precisely because we canceled open hypotheses containing x that x now does not occur free in open hypotheses. The key word here is "open". When you are proving A -> B, you assume A and prove B. In the process of proving B, A is an open hypothesis. Then, when B is finally proved, you apply the implication introduction rule, cancel (or close) A and derive A -> B. At this point, A is strictly speaking still a hypothesis (because it is a leaf in the derivation tree), but it is now a canceled (or closed) hypothesis. Usually when we are talking about hypotheses, we mean open hypotheses only.

One way to ensure it is to cancel hypotheses that contain $x$ free as described in 2

I mean: how do we ensure this?!

Again, I am not sure I understand the question. By canceling open hypotheses that contain x, we make them (hypotheses) canceled, or closed, rather than open. If we cancel all such hypotheses, there are no more open (not canceled) ones that contain x, and so the requirement associated with the universal introduction rule is fulfilled.

Does this answer your question? If not, then you may need to come up with an example or ask questions more formally (not using words like "we believe" or "we ensure", which may be subjective).

 

[Mathelogician]

I think my problem with the concepts of closed and open hypotheses is more philosophical than mathematical. You may remember that we have had a discussion on that before! but now i think i am still unconvinced about that!
So i prefer to first talk about those concepts (Closed and Open hypothesis).
As in Van Dalen (p. 31) we see the two Quires attached bellow!
Here Van Dalen himself says that it is more a matter of psychology than formal logic to cancel hypothesis in the Implication introduction rule!
I think it is also mostly a matter of pure Syntax than any meaningful notion in real! (How do you define Real? ;)). Maybe the two quires lead you to such a conception of the notion too! Or maybe i still need more discussions on the concept!
[Note: In the first line of the query 1, it is talking about the proof of the theorem that two angles of a isosceles triangle are equal]

Regards.

 

[Evgeny.Makarov]

Here Van Dalen himself says that it is more a matter of psychology than formal logic to cancel hypothesis in the Implication introduction rule!

Not exactly. He says it is a matter of psychology to experience superfluous hypotheses as confusing and/or misleading. For soundness (i.e., for every derived formula to be valid) we can cancel any number of (occurrences of) hypotheses A when using (->I) to derive A -> B. For completeness (to be able to derive every valid formula) it is important to be able to cancel all relevant hypotheses. Otherwise, we can't derive A -> A from the empty set of open hypotheses.

I think it is also mostly a matter of pure Syntax than any meaningful notion in real!

Yes, as any mathematical definition, the definition of a natural deduction derivation is somewhat arbitrary. But it is "correct" in the sense that it reflects actual mathematical reasoning. Also, the fact that the resulting concept has nice properties (such as soundness, completeness and strong normalization) adds confidence that it is designed correctly. At least it is mathematically interesting.