Page 106 - Textos de Matemática Vol. 40

94 Chapter 3. Truth Theories Definition 3.1.4. 1. t = s, N(t), ¬t = s and ¬N(t) are T-positive as well as
T-negative.
2. T(t) is T-positive; ¬T(t) is T-negative.
3. If φ is T-positive (T-negative), then ¬φ is T-negative (T-positive).
4. If φ and ψ are T-positive (T-negative), then so is φ ∧ ψ.
5. If φ is T-positive (T-negative), then so is ∀x.φ.
Now, we can prove by straightforward induction that FON provides a truth
definition for T-positive formulae [Can96, Theorem 8.8.]:
Proposition 3.1.5. If φ is a T-positive formulae of LFt , then we have: FON ⊢ T(φ˙) ↔ φ.
This Proposition is the essential tool to introduce abstraction terms or a notion of sets with an element relation on the basis of the truth predicate, cf. [Sco75].
Definition 3.1.6. Given two LFt terms t and s and an LFt formula φ, we define: {x|φ} := λx.φ˙,
t∈s :⇔ T(st).
Since the term {x|φ} is defined for arbitrary formulae φ, we may say that Frege structures allow full or unrestricted comprehension. But it is clear that the element relation has its intended meaning for T-positive formulae only. From Proposition 3.1.5, we get as a Corollary:
Corollary 3.1.7. If φ is a T-positive formulae of LFt , then we have: FON ⊢ x ∈ {x|φ} ↔ φ.
3.1.3 Fixed points
In [Sco75], Scott defined a fixed point of sets by use of a Fixed Point Theorem on the ground structure. In the same manner, Cantini proved that the truth theories may be used to define fixed points of positive operator forms, [Can96, §10A]. For it, and in analogy to ID1, we define the notion of positive operator form in FON as a T-positive formulae φ(R, x) which contains the (unary) relation variable R only positively. Now, we can use Proposition 3.1.5 to define fixed points of such operator forms within FON. The proof makes essential use of the possibility to define fixed points on the term level.