Page 134 - Textos de Matemática Vol. 40

122 Chapter 3. Truth Theories
for the negation of the corresponding relation symbols of LU resulting in a new language LTU . By de Morgan’s laws we define negation for arbitrary formulae. WedealwithfinitesetsofLTU formulae(Γ,∆,...),theintendedlogicalmeaning being the disjunction of its elements. We use the usual short hand notation (e.g., φ is used for the singleton {φ}) and we abbreviate union of sets by use of commas.
Definition 3.4.16. A LTU formula φ is called a T+ formula, if it contains no subformulae of the form T(t) and U(s); it is called T− formula, if it contains none of the form T(t) and U(s).
To deal with class and truth induction, we introduce the sequent calculus FSUT . For formula induction, we have to define a semi-formal system FSU∞ which will be described later.
ThelogicalaxiomsandrulesofFSUT areasusual,containingequalityand the cut rule:
(Cut) Γ, φ Γ, ¬φ Γ
where φ is called the cut formula.
The non-logical axioms are as usual. The axioms of TON can be chosen
in the standard way. To ensure that all the main formulae are either T+ or T− formulae, we have to split the closure conditions of FSU into two axioms. For instance, the closure under double negation of FSU reads as
(7a) Γ, U(s), T(s t), T(s (¬˙ (¬˙ t))), (7b) Γ, U(s), T(s (¬˙ (¬˙ t))), T(s t).
In addition, we get for the basic axioms, order structure, local consistency, and the limit axiom of FSU the following axioms in FSUT :
(1) Γ, U(s), T(s t) ∨ T(¬˙ (s t)),
(2) Γ, U(s), T(s t), T(t),
(12) Γ, U(r), U(s), T(s (r t)), T(s t),
(13) Γ, U(s), T(s t), T(s (¬˙ t)),
(14a) Γ, (∃x.T(t x) ∧ T(¬˙ (t x))), U(l t),
(14b) Γ, (∃x.T(t x) ∧ T(¬˙ (t x))), T(t s), T(l t (t s)),
(14c) Γ, (∃x.T(t x) ∧ T(¬˙ (t x))), T(¬˙ (t s)), T(l t (¬˙ (t s))).
For class and truth induction, we have to use in FSUT the following rules: