Page 136 - Textos de Matemática Vol. 40

124 Chapter 3. Truth Theories
Partial models. The following model construction is an adaptation of the construction given by Strahm for the theory EMU, explicit mathematics with universes, in [Str99].
We start with a given formalization of CT T , the standard model of TON, in PA. Let N be the interpretation of N.
First, we extend this formalization to the additional constants =˙ , N˙ , ¬˙ , ∧˙ , ∀˙ and l of LU . Since there are no new equalities about these constants, the only requirement is the uniqueness of the formalized terms, e.g., t=˙ s has to be different from t ∧˙ s. To keep the notation simple, in the following, we do not distinguish between the terms of LU and theirs formalization in the model.
Now we define an inductive operator form Φ(X, Y, x, α) which captures the closure conditions of the predicate T.
Φ(X,Y,a,α) holds if there exist elements b,c and f of the model such that one of the following clauses holds. (Here S(α) means that α is a successor ordinal.)
1. 2. 3. 4. 5. 6. 7. 8. 9.
10. 11. 12.
a∈Y,
α=0∧a=(b=˙ c)∧b=c,
α = 0 ∧ a = ¬˙ (b =˙ c) ∧ b ̸= c,
α=0∧a=(N˙ b)∧N(b),
α=0∧a=¬˙(N˙ b)∧¬N(b),
a = ¬˙ (¬˙ b) ∧ a ̸∈ Y ∧ b ∈ X,
a = (b ∧˙ c) ∧ a ̸∈ Y ∧ b ∈ X ∧ c ∈ X,
a=¬˙(b∧˙ c)∧a̸∈Y ∧((¬˙ b∈X)∨(¬˙ c∈X)),
a=(∀˙f)∧a̸∈Y ∧∀x.fx∈X,
a = ¬˙ (∀˙ f) ∧ a ̸∈ Y ∧ ∃x.¬˙ (f x) ∈ X,
S(α)∧a=(lb)c∧a̸∈Y ∧¬˙ a̸∈Y ∧(∀x.bx∈Y ∨¬˙ (bx)∈Y)∧c∈Y, S(α)∧a=¬˙((lb)c)∧a̸∈Y∧¬˙a̸∈Y∧(∀x.bx∈Y∨¬˙(bx)∈Y)∧c̸∈Y.
In the proof-theoretic analysis of FSU we have to consider not only fixed points of Φ but consistent fixed points which are needed to verify the consistency axiom. Before we turn to these considerations let us describe briefly how we may form a full model of FSU+(LU-IN) by use of Φ. Let us define a Φ-sequence (Zβ ) of least fixed points Zβ for β ≤ α in the following way:
1. Z0 is the empty set ∅.
2. Zβ+1 istheleastfixedpointofΦ(Z,Zβ,x,β+1),