Page 20 - Textos de Matemática Vol. 38

12 FERNANDO FERREIRA
Theorem 2.5 (Characterization). For any formula A, HAω0 + ACω + IPω∃free ⊢ A ↔ (A)mr.
With an eye to forthcoming results, it should be noted that the above equivalence is provable in a true theory, since both ACω and IPω∃free are true principles.
Corollary 2.6. The following two properties hold:
(a) (Disjunction Property) Suppose that HAω0 + ACω + IPω∃free ⊢ A ∨ B, for closed formulas A and B. Then, either HAω0 +ACω +IPω∃free ⊢ A or HAω0 + ACω + IPω∃free ⊢ B.
(b) (Existence Property) Suppose that HAω0 + ACω + IPω∃free ⊢ ∃xA(x), for a closed formula ∃xA(x). Then there is a closed term t such that HAω0 + ACω + IPω∃free ⊢ A(t).
The above corollary is consequence of the soundness and characterization
theorems. For instance, suppose that A ∨ B is provable in HAω0 + ACω + IPω∃free. By the characterization theorem, there are closed terms s0 and t, q such that,
HAω0 ⊢(s=0→Amr(t))∧(s̸=0→Bmr(q)).
Since s is a closed term, there is a numeral n such that HAω0 ⊢ s = n. Suppose n = 0 (the other case is similar). Then HAω0 ⊢ Amr(t) and, therefore, HAω0 ⊢ (A)mr. By the characterization theorem, we get the desired conclusion.
It is important to notice that the above argument works because, in the presence of ACω and IPω∃free, it is possible to come back from the formula (A)mr to the original formula A. The existence property has the following natural generalization:
Proposition 2.7. Let A be an arbitrary formula with free variables among x and y. Suppose that
HAω0 + ACω + IPω∃free ⊢ ∀x∃yA(x, y).
Then there is a closed term t of appropriate type such that
HAω0 + ACω + IPω∃free ⊢ ∀xA(x, tx).
This is not a conservation result anymore. However, it is still a sound
extraction result since the conclusion ∀xA(x, tx) is true.
Theorem 2.8 (Fan rule). Let A be an arbitrary formula containing only the
variables x1 and n0. Then the following rule holds: If HAω0 + ACω + IPω∃free ⊢ ∀x ≤1 1∃n0 A(x, n)