Page 112 - Textos de Matemática Vol. 40

100 Chapter 3. Truth Theories Remark 3.2.1. The equivalence of TON and BON + (Tot) can be extended
straightforwardly to FON and FDA + (Tot).
Now we define a suitable class of formulae φ of LFd , for which we can define a representation φ˙ , such that FDA plus the additional axiom (AllN) proves T(φ˙ ) ↔ φ. Moreover, this provides an embedding of ID1 within FDA + (AllN) + (F-IN). The axiom (AllN) is needed for a proper treatment of disjunctions to overcome the problem described above. The other problem, concerning possibly undefined terms in negated prime formulae, will be avoided by restricting the class of T- positive formulae:4
Definition 3.2.2. The class of weakly T-positive formulae is inductively defined as follows:5
1. t = s, ¬x = y, N(t), ¬N(x), and T(t) are weakly T-positive formulae.
2. If φ and ψ are weakly T-positive, then also φ∧ψ and φ∨ψ, i.e., ¬(¬φ∧¬ψ). 3. If φ is weakly T-positive, then also ∀x.φ and ∃x.φ, i.e., ¬∀x.¬φ.
As mentioned above a straightforward representation of conjunction, from which disjunction is derived, yields a problem with the interpretation of the fixed point constants of ID1. This problem can be avoided, if we represent conjunctions φ∧ψ by use of a function f, such that f0 ≃ φ˙ and fy ≃ ψ˙, if y ̸= 0. So in the case of disjunctions we get T(φ˙ ) ∨ T(ψ˙ ) ↔ ∃y.T(f y). Here we profit from the fact that in the axiom of truth for existential quantification f y needs not to be a proposition for every y. We will use the non-strict case distinction (see Subsection 1.3.4) dN (λz.φ˙) (λz.ψ˙) y 0 0, where y, z ̸∈ FV(φ˙, ψ˙), for the definition of f to ensure that the existence of f y only depends on the existence of its actual value φ˙ or ψ˙, but not on the other one. However, in the case of T(φ˙) ∧ T(ψ˙) f y must be true (and therefore defined) for all y to apply axiom II.(8).6 Because we have to use dN for the case-distinction in f, we need the assumption (AllN). Otherwise, dN (λz.φ˙) (λz.ψ˙) 0 y is not provably defined, if y does not belong to N.7
Definition 3.2.3. We inductively assign a term φ˙ to every formula φ of LFd , by ˙ ˙ ˙
setting t↓ :=t=˙ tandreplacing=,N,T,and¬by=˙,N,T,and¬˙,respectively.
4A similar problem with negated prime formulae occurs in the applicative theory FMT0 of Mancosu. His class of ∃+-formulae has the same restriction on negated equalities, cf. [Man91, Section 2.1.].
5We add ¬N(x) for reasons of completeness. Of course, in the presence of (AllN), ¬N(x) is meaningless. On the other hand, we leave out t ↓, because it is equivalent to t = t.
6A similar problem arises, if we try to carry over Beeson’s embedding of EETJ within FDA. In general, we cannot prove ∀x. q x ↓ for the function q used to represent the join operation, cf. [Bee85, p. 414]. But this would be needed to verify the join axiom of EETJ.
7In fact, it would be sufficient to add a definition by cases on the universe dV , cf. [Fef79, p. 183], to FDA instead of (AllN).