# LPL 10.26 - Fitch - How to use ∀ Intro and ∃ Elim?

I am using LPL (Language, Proof, and Logic, commonly known as LPL) and the bundled Fitch program. I am trying to solve problem 10.26:

``````10.26:     ∀x Tet(b) ↔ ∃w Tet(b)
``````

Looks simple enough, as the null quantification means this is just:

``````Tet(b) ↔ Tet(b)
``````

Which is, of course, a tautology. I do not need an premises for this. But my problem is that I do not know how to use ∀ Intro nor ∃ Elim as the book doesn't seem to cover these two, and I have no idea how else to prove the original statement without using those two.

So how can I solve this issue?

• I would like to add that I think "lpl" and "fitch" would be good new tags. – zagadka314 Jul 10 '15 at 20:21

I agree with your concern : the exercise is proposed before the explanation of the inference rules for the quantifiers : thus, we are not requested to use them.

The exercise asks to prove that the biconditional : ∀x Tet(b) ↔ ∃w Tet(b) is a logical truth, i.e. that

the two sides of the biconditional are logically equivalent (2nd ed : 2011, page 286).

The definition of logical equivalence is :

We say that two wffs with free variables are logically equivalent if, in any possible circumstance, they are satified by the same objects. (page 278).

Note : if we want, we may consider only the non-trivial case :

∃w Tet(b) → ∀x Tet(b),

because for the other conditional, we have to note that : ∀x φ(x) → ∃w φ(x) holds in general.

The discussion about null quantication (page 283) has showed that :

if the variable x is not free in wff P, then we have the following (logical) equivalences: ∀x P ⇔ P ⇔ ∃w P (see page 82 for the symbol : which stay for logically equivalent, and is not the biconditional).

This means that : ∃w Tet(b), ∀x Tet(b) and Tet(b) are either all true or all false.

Consider the two cases :

(i) Tet(b) is t : then both ∃w Tet(b) and ∀x Tet(b) are t, and thus the biconditional : ∃w Tet(b) ↔ ∀x Tet(b) is t (because : t ↔ t is t);

(ii) Tet(b) is f : then both ∃w Tet(b) and ∀x Tet(b) are f, and thus the biconditional : ∃w Tet(b) ↔ ∀x Tet(b) is again t (because : f ↔ f is t).

Conclusion : in any possible circumstance, the formula ∃w Tet(b) ↔ ∀x Tet(b) is satisfied, and thus it is a logical truth.

For a derivation with the inference rules of the book (i.e. with Natural Deduction) we consider only the non-trivial case :

∃w Tet(b) → ∀x Tet(b).

Here we need to note that the (meta-) expressions φ(x,y) neither means that the listed variables occur free nor that no other ones occur free.

We have to "read carefully" the Universal Introduction (∀ Intro) rule (page 352) :

if we have a derivation of φ[c/x] (i.e. the formula obtained from φ(x) replacing all occurrences of the variable x with the term c) and c does not occur in φ or in any undischarged assumption of the derivation, then we are licensed to derive ∀xφ. In symbols : φ[c/x] ⊢ ∀x φ.

1) ∃w Tet(b) --- assumption [a]

start a subproof :

2) Tet(b) --- assumed for ∃ Elim (page 357) : we introduce a new constant symbol, say c, replacing all the occurrences of w in Tet(b) with c, along with the assumption that the object denoted by c satisfies the formula Tet(b); but there is no occurrences of w in Tet(b), thus the result of Tet(b)[c/w] is Tet(b) itself.

3) ∀x Tet(b) --- from 2) by ∀ Intro

end of subproof;

4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ Elim

5) ∃w Tet(b) → ∀x Tet(b) --- from 1) and 4) by → Intro, discharging the assumption [a].

• Wow, thank you very much for that detailed solution! – zagadka314 Jul 12 '15 at 17:34

The solution to 10.26. You will hit yourself for this, if you are as lost as I was!!

``````|_
|∀x Tet(b) ↔ ∃w  Tet(b)                                                             FO Con
``````

Just type the same exact thing you see in question 10.26, then select "FO Con" without any premises.

This still doesn't answer the question about how to use ∀ Intro and ∃ Elim, but it answers how to solve 10.26. I assume that ∀ Intro and ∃ Elim are covered later in the text, and I will update this answer when I come to that section. See the very impressive answer above instead!

• Of course, any other answers are welcome too! – zagadka314 Jul 10 '15 at 21:50