Metatheorem. (Auxiliary Constant Metatheorem) Let c be a constant that does not appear in the formulae A or B. Assume that I |- (∃x)A. Moreover, let I' +A[x :=c] |- B, with a proof where the formulae invoked from I' do not contain the constant c. Then I'|- B as well.
ADDMONAL EXERCISES-
1. Show that |- (∀x)(A → B) → (∃x)A→ (∃x)B.
2. Show that |- (∀x) ((A ν B) →C) → (∀x) (A → C).
3. Show that |- (∀x)((A ν B) → C) → (∀x)(A → C).
4. Show that |- (∀x)(A → (B Λ C)) → (∀x)(A → B).
5. Prove the following version of the relativized ∀-monotonicity,
|-(∀x)A(B →C) →(∀x)A B→ (∀x)AC
while in standard notation it reads
|- (∀x)(A→ B→ C) → (∀x)(A →B) → (∀x)(A → C)
6. Prove |- (∃x)AΛB C ≡ (∃x)A(B Λ C)
Hint Translate first to standard notation.
7. Prove
|- AV (∀x)BC = (∀x)B(A ν C), as long as x not free in A, Hint. Translate first to standard notation
8. Prove
|- A Λ (∃x)BC ≡ (∀x)B(A Λ C),as keg attract free is A, Hint Translate first to standard notation.
9. Prove
|- (∃x)A B v (∃x)AC ≡ (∃x)A(B v C)
Hint Translate first to standard notation.
10. Prove that if x is not free in A, then |- A ≡ (∃x)A.
11. Prove the one point rule- ∃-version: |- (∃x)(x = t Λ A) ≡ A[x:= t] if x is sot free in t.
12. Prove |- (∃x)(A Λ (∃y)(B Λ C)) ≡ (∃y)(B Λ (∃x)(A Λ C)), on the condition that y is not free in A and x is not free in B.
13. Prove |- (∃x)AvB C ≡ (∃x)AC v (∃x)BC. Hint. Translate to standard notation first.
14. Prove |- (∃x)( ∃y)(A Λ B Λ C) ≡ (∃x)(A Λ (∃y)(B Λ C)), on the condition that y is not free in A.
15. Prove dummy renaming for ∃: If z does not occur in A, then |- (∃x) A ≡ (∃z) A[x := z].
16. Here is a suggested proof of
|- (∀x)(∃y)A→ (∃y)(∀x)A (*)
We split the → and go via the deduction theorem:
(1) (∀x)(∃y)A (hypothesis)
(2) (∃y)A ((1) + spec)
(3) A[y :=z] (auxiliary hypothesis associated with (2); z is fresh)
(4) (∀x)A[y :=z] ((3) + gen; Okay: x is not free in hypothesis line (1))
(5) (∃y)(∀x)A
17. Prove using the auxiliary variable metatheorem |- (∃x)(A→B) → (∀x)A→ (∃x)B.
18. Prove using the auxiliary variable metatheorem: |- (∃x)B → (∃x)(A v B).
19. Prove |- (∃x)AC →(∃x)AvBC.
20. Let Φ be a predicate of arity 2.