# Return to Answer

 4 deleted 3 characters in body edited Jul 11 '15 at 13:21 Mauro ALLEGRANZA 28.9k22 gold badges2020 silver badges6868 bronze badges Here we need to note that the (meta-) expressions φ(x,y,z) neither means that the listed variables occur free nor that no other ones occur free. 4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ IntroElim Here we need to note that the (meta-) expressions φ(x,y,z) neither means that the listed variables occur free nor that no other ones occur free. 4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ Intro 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. 4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ Elim 3 added 106 characters in body edited Jul 11 '15 at 12:36 Mauro ALLEGRANZA 28.9k22 gold badges2020 silver badges6868 bronze badges I agree with your concern : the exercise is proposed before the explanation of the inference ruelsrules for the quantifiers : thus, we are not requested to use them. the that the two sides of the biconditional are logically equivalent (2nd ed : 2011, page 286). Here we need to note that the (meta-) expressions φ(x,y,z) neither means that the listed variables occur free nor that no other ones occur free. in order to simplify the substitution notation we will write down (meta-) expressions like φ(x,y,z),etc. This neither means that the listed variables occur free nor that no other ones occur free. This "tricky point" must be taken into account when usingWe 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)⊢∀x φ(x), where replacing all occurrences of the variablevariable x maywith the term c) and c does not occur free in any hypothesis on which φ(x) dependsor in any undischarged assumption of the derivation, then we are licensed to derive ∀xφ. In symbols : φ[c/x] ⊢ ∀x φ. 2) 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) end of subproof : ∀x Tet(b) --- from 2) by ∀ Intro end of subproof; I agree with your concern : the exercise is proposed before the explanation of the inference ruels for the quantifiers : thus, we are not requested to use them. the that the two sides of the biconditional are logically equivalent (2nd ed : 2011, page 286). Here we need to note that in order to simplify the substitution notation we will write down (meta-) expressions like φ(x,y,z),etc. This neither means that the listed variables occur free nor that no other ones occur free. This "tricky point" must be taken into account when using the Universal Introduction (∀ Intro) rule (page 352) : φ(x)⊢∀x φ(x), where the variable x may not occur free in any hypothesis on which φ(x) depends. 2) start a subproof : 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 is Tet(b) itself. 3) end of subproof : ∀x Tet(b) --- from 2) by ∀ Intro 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 two sides of the biconditional are logically equivalent (2nd ed : 2011, page 286). Here we need to note that the (meta-) expressions φ(x,y,z) 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 φ. 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; 2 added 1282 characters in body edited Jul 11 '15 at 11:37 Mauro ALLEGRANZA 28.9k22 gold badges2020 silver badges6868 bronze badges We say that two wff swffs with free variables are logically equivalent if, in any possible circumstance, they are satifi edsatified by the same objects. (page 278). The discussion about null quanti cationquantication (page 283) has showed that : 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 in order to simplify the substitution notation we will write down (meta-) expressions like φ(x,y,z),etc. This neither means that the listed variables occur free nor that no other ones occur free. This "tricky point" must be taken into account when using the Universal Introduction (∀ Intro) rule (page 352) : φ(x)⊢∀x φ(x), where the variable x may not occur free in any hypothesis on which φ(x) depends. 1) ∃w Tet(b) --- assumption [a] 2) start a subproof : 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 is Tet(b) itself. 3) end of subproof : ∀x Tet(b) --- from 2) by ∀ Intro 4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ Intro 5) ∃w Tet(b) → ∀x Tet(b) --- from 1) and 4) by → Intro, discharging the assumption [a]. We say that two wff s with free variables are logically equivalent if, in any possible circumstance, they are satifi ed by the same objects. (page 278). The discussion about null quanti cation (page 283) has showed that : Conclusion : in any possible circumstance, the formula ∃w Tet(b) ↔ ∀x Tet(b) is satisfied, and thus it is a logical truth. 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 : 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 in order to simplify the substitution notation we will write down (meta-) expressions like φ(x,y,z),etc. This neither means that the listed variables occur free nor that no other ones occur free. This "tricky point" must be taken into account when using the Universal Introduction (∀ Intro) rule (page 352) : φ(x)⊢∀x φ(x), where the variable x may not occur free in any hypothesis on which φ(x) depends. 1) ∃w Tet(b) --- assumption [a] 2) start a subproof : 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 is Tet(b) itself. 3) end of subproof : ∀x Tet(b) --- from 2) by ∀ Intro 4) ∀x Tet(b) --- from 1) and the subproof above, by ∃ Intro 5) ∃w Tet(b) → ∀x Tet(b) --- from 1) and 4) by → Intro, discharging the assumption [a]. 1 answered Jul 11 '15 at 9:13 Mauro ALLEGRANZA 28.9k22 gold badges2020 silver badges6868 bronze badges