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

Question

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?

Answer 1

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).

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 case (the other one is similar):

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

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 φ.

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

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].

Answer 2

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!