Gilles Dowek
email: gilles.dowek@polytechnique.edu

Truth values algebras and proof normalization

come

Introduction

Proving that a theory has the cut elimination property has some similarities with proving that it has a model. These similarities appear, for instance, in the model theoretic proofs of cut elimination, where cut elimination is obtained as a corollary of a strengthening of the completeness theorem, expressing that if a formula is valid in all models of a theory, then it has a cut free proof in this theory. Such a method has been used, for instance, by Schütte, Kanger, Beth, Hintikka and Smullyan. It has then been used by Tait [START_REF] Tait | A non constructive proof of Gentzen's Hauptsatz for second order predicate logic[END_REF], Prawitz [START_REF] Prawitz | Hauptsatz for higher order logic[END_REF], Takahashi [START_REF] Takahashi | A proof of cut-elimination theorem in simple type theory[END_REF] and Andrews [START_REF] Andrews | Resolution in type theory[END_REF] to prove cut elimination for simple type theory. It has been generalized, more recently, by De Marco and Lipton [START_REF] Marco | Completeness and cut-elimination in the intuitionistic theory of types[END_REF] to prove cut elimination for an intuitionistic variant of simple type theory, by Hermant [START_REF] Hermant | A model based cut elimination proof[END_REF][START_REF] Hermant | Semantic cut elimination in the intuitionistic sequent calculus[END_REF] to prove cut elimination for classical and intuitionistic theories in deduction modulo and by Okada [START_REF] Okada | A uniform semantic proof for cut elimination and completeness of various first and higher order logics[END_REF] to prove cut elimination for intuitionistic linear logic.

An alternative method to prove cut elimination is to prove that all proofs strongly normalize. Following Tait [START_REF] Tait | Intentional interpretations of functionals of finite type I[END_REF] and Girard [START_REF] Girard | Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types[END_REF], this is proved by assigning a set of proofs, called a reducibility candidate, to each formula. Here also, the proofs have some similarities with the construction of models, except that, in these models, the truth values 0 and 1 are replaced by reducibility candidates. This analogy has been exploited in a joint work with Werner [START_REF] Dowek | Proof normalization modulo[END_REF], where we have defined a notion of reducibility candidate valued models, called pre-models, and proved that if a theory in deduction modulo has such a model, then it has the strong normalization property.

The fact that both cut elimination proofs and strong normalization proofs proceed by building models raises the problem of the difference between cut elimination and strong normalization. It is well-known that strong normalization implies cut elimination, but what about the converse ? This problem can be precisely stated in deduction modulo, where instead of using an ad hoc notion of cut for each theory of interest, we can formulate a general notion of cut for a large class of theories, that subsumes the usual ad hoc notions. This problem has been solved by Hermant [START_REF] Hermant | Méthodes sémantiques en déduction modulo[END_REF] and surprisingly the answer is negative: there are theories that have the cut elimination property, but not the strong normalization property and even not the weak normalization property. Thus, although the model theoretic cut elimination proofs and the strong normalization proofs both proceed by building models, these methods apply to different theories.

In this paper, we focus on the model theoretic characterization of theories in deduction modulo that have the strong normalization property. It has been proved in [START_REF] Dowek | Proof normalization modulo[END_REF] that a theory has the strong normalization property if it has a reducibility candidate valued model. However, the usual model constructions use very little of the properties of reducibility candidates. In particular, these constructions seem to work independently of the chosen variant of the closure conditions defining reducibility candidates. This suggests that this notion of reducibility candidate valued model can be further generalized, by considering an abstract notion of reducibility candidate.

Abstracting this way on the notion of reducibility candidate leads to introduce a class of algebras, called truth values algebras, that also generalize Heyting algebras. However there is an important difference between truth values algebras and Heyting algebras: in a Heyting algebra valued model the formula P ⇔ Q is valid if and only if the formulae P and Q have the same denotation. In particular, all theorems have the same denotation. This is not necessarily the case in truth values algebra valued models where two theorems may have different denotation. Thus, truth values algebra valued models are more "intentional" than Heyting algebra valued models. In particular, it is possible to distinguish in the model between the computational equivalence of formulae (the congruence of deduction modulo, or the definitional equality of Martin-Löf's type theory) and the provable equivalence: the denotations of two computationally equivalent formulae are the same, but not necessarily those of two logically equivalent formulae. Thus, independently of normalization, this generalization of Heyting algebras seems to be of interest for the model theory of deduction modulo and type theory.

We shall first introduce the notion of truth values algebra and compare it with the notion of Heyting algebra. Then, we shall consider plain predicate logic, define a notion of model based on these truth values algebras and prove a soundness and a completeness theorem for this notion of model. We shall then show that this notion of model extends to deduction modulo. Finally, we shall strengthen the notion of consistency into a notion of super-consistency and prove that all super-consistent theories have the strong normalization property.

Truth values algebras

Definition

Definition 1 (Truth values algebra). Let B be a set, whose elements are called truth values, B + be a subset of B, whose elements are called positive truth values, A and E be subsets of ℘(B), ⊤ and ⊥ be elements of B, ⇒, ∧, and ∨ be functions from B × B to B, ∀ be a function from A to B and ∃ be a function from E to B. The structure B = ⟨B, B + , A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ is said to be a truth value algebra if the set B + is closed by the intuitionistic deduction rules i.e. if for all a, b, c in B, A in A and E in E,

1. if a ⇒ b ∈ B + and a ∈ B + then b ∈ B + , 2. a ⇒ b ⇒ a ∈ B + , 3. (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c ∈ B + , 4. ⊤ ∈ B + , 5. ⊥ ⇒ a ∈ B + , 6. a ⇒ b ⇒ (a ∧ b) ∈ B + , 7. (a ∧ b) ⇒ a ∈ B + , 8. (a ∧ b) ⇒ b ∈ B + , 9. a ⇒ (a ∨ b) ∈ B + , 10. b ⇒ (a ∨ b) ∈ B + , 11. (a ∨ b) ⇒ (a ⇒ c) ⇒ (b ⇒ c) ⇒ c ∈ B + , 12. the set a ⇒ A = {a ⇒ e | e ∈ A} is in A and the set E ⇒ a = {e ⇒ a | e ∈ E} is in A, 13. if all elements of A are in B + then ∀ A ∈ B + , 14. ∀ (a ⇒ A) ⇒ a ⇒ ( ∀ A) ∈ B + , 15. if a ∈ A, then ( ∀ A) ⇒ a ∈ B + , 16. if a ∈ E, then a ⇒ ( ∃ E) ∈ B + , 17. ( ∃ E) ⇒ ∀ (E ⇒ a) ⇒ a ∈ B + .

Definition 2 (Full). A truth values algebra is said to be

full if A = E = ℘(B), i.e. if ∀ A and ∃ A exist for all subsets A of B.

Definition 3 (Trivial).

A truth values algebra is said to be trivial if B + = B.

Example 1. Let B = {0, 1}. Let B + = {1}, A = E = ℘(B), ⊤ = 1, ⊥ = 0, ⇒, ∧, ∨ be the usual boolean operations, ∀ be the function mapping the sets {0} and {0, 1} to 0 and ∅ and {1} to 1 and ∃ be the function mapping the sets ∅ and {0} to 0 and {1} and {0, 1} to 1. Then ⟨B, B + , A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ is a truth value algebra.

Example 2. Let B be an arbitrary set, B + = B, A = E = ℘(B) and ⊤, ⊥, ⇒, ∧, ∨, ∀ and ∃ be arbitrary operations. Then ⟨B, B + , A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ is a trivial truth value algebra.

Pseudo-Heyting algebras

In this section, we show that truth values algebras can alternatively be characterized as pseudo-Heyting algebras.

Definition 4 (Pseudo-Heyting algebra).

Let B be a set, ≤ be a relation on B, A and E be subsets of ℘(B), ⊤ and ⊥ be elements of B, ⇒, ∧, and ∨ be functions from B × B to B, ∀ be a function from A to B and ∃ be a function from E to B, the structure B = ⟨B, ≤, A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ is said to be a pseudo-Heyting algebra if for all a, b, c in B, A in A and E in E, (the relation ≤ is a pre-order)

-a ≤ a, -if a ≤ b and b ≤ c then a ≤ c,
( ⊤ and ⊥ are maximum and minimum elements (notice that these need not be unique))

-a ≤ ⊤, -⊥ ≤ a,
(a ∧ b is a greatest lower bound of a and b and and a ∨ b is a least upper bound of a and b (again, these need not be unique))

-a ∧ b ≤ a, -a ∧ b ≤ b, -if c ≤ a and c ≤ b then c ≤ a ∧ b, -a ≤ a ∨ b, -b ≤ a ∨ b, -if a ≤ c and b ≤ c then a ∨ b ≤ c, (the set A and E have closure conditions) -a ⇒ A and E ⇒ a are in A,
( ∀ and ∃ are infinite greatest lower bound and least upper bound) Proof. -Using 1. 2. and 3. we get that a ⇒ a ∈ B + .

-if a ∈ A then ∀ A ≤ a, -if for all a in A, b ≤ a then b ≤ ∀ A, -if a ∈ E then a ≤ ∃ E, -if for all a in E, a ≤ b then ∃ E ≤ b,
-Using 1. 2. and 3. we get that a

⇒ b ∈ B + and b ⇒ c ∈ B + then a ⇒ c ∈ B + . -Using 1. 2. and 4. we get that a ⇒ ⊤ ∈ B + . -⊥ ⇒ a ∈ B + is condition 5. -(a ∧ b) ⇒ a ∈ B + is condition 7. -(a ∧ b) ⇒ b ∈ B + is condition 8. -Using 1. 2. 3. and 6. we get that if c ⇒ a ∈ B + and c ⇒ b ∈ B + then c ⇒ (a ∧ b) ∈ B + , -a ⇒ (a ∨ b) ∈ B + is condition 9. -b ⇒ (a ∨ b) ∈ B + is
≤ a then ⊤ ≤ b. 2. We have ( ⊤ ∧ a) ∧ b ≤ ⊤ ∧ a ≤ a. Hence ⊤ ≤ a ⇒ b ⇒ a. 3. Let x = ⊤ ∧ (a ⇒ b ⇒ c) ∧ (a ⇒ b) ∧ a. We have x ≤ a ⇒ b ⇒ c, x ≤ a ⇒ b and x ≤ a.
Using the lemma three times, we get 13. If all elements of A are in B + then ∀ A ∈ B + . Indeed, for all elements x of A, ⊤ ≤ x hence ⊤ ≤ ∀ A. 14. Let x = ⊤ ∧ ∀ (a ⇒ A) ∧ a. Let y be an arbitrary element of A. Notice that, by definition of a ⇒ A, a ⇒ y ∈ a ⇒ A. We have x ≤ ∀ (a ⇒ A) hence x ≤ a ⇒ y. We also have x ≤ a, hence using the lemma x ≤ y. For all y ∈ A, we have x ≤ y,

x ≤ c. Hence ⊤ ≤ (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c. 4. We have ⊤ ≤ ⊤. 5. We have ⊤ ∧ ⊥ ≤ ⊥ ≤ a, thus ⊤ ∧ ⊥ ≤ a. Hence ⊤ ≤ ⊥ ⇒ a.
thus x ≤ ∀ A. Hence ⊤ ≤ ∀ (a ⇒ A) ⇒ a ⇒ ( ∀ A). 15. If a ∈ A, then we have ⊤ ∧ ( ∀ A) ≤ ∀ A ≤ a. Hence ⊤ ≤ ( ∀ A) ⇒ a. 16. If a ∈ A, then we have ⊤ ∧ a ≤ a ≤ ∃ A. Hence ⊤ ≤ a ⇒ ( ∃ A).
17. Let x = ⊤ ∧ ( ∃ A) ∧ ∀ (A ⇒ a). We have x ≤ ( ∃ A) and x ≤ ∀ (A ⇒ a). We have x ≤ ( ∃ A) and x ≤ x thus x ≤ ( ∃ A) ∧ x. As x ≤ ∀ (A ⇒ a). For all y in A, x ≤ y ⇒ a, i.e (x ∧ y) ≤ a. For all y in A, we have y ∧ x ≤ x ∧ y ≤ a i.e. y ≤ x ⇒ a. Thus, ∃ A ≤ x ⇒ a, i.e. ∃ A ∧ x ≤ a. By transitivity, we get x ≤ a. Hence ⊤ ≤ ( ∃ A) ⇒ ∀ (A ⇒ a) ⇒ a.

Definition 5 (Heyting algebra). A pseudo-Heyting algebra is said to be a Heyting algebra if the relation ≤ is antisymmetric

-x ≤ y ⇒ y ≤ x ⇒ x = y.
Remark. If the pseudo-Heyting algebra ⟨B, ≤, A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ is a Heyting algebra, then the set B + = {x | ⊤ ≤ x} is the singleton { ⊤}. Indeed, if a ∈ B + then ⊤ ≤ a and a ≤ ⊤. Hence a = ⊤. Definition 6. A function F from a truth value algebra B 1 to a truth value algebra B 2 is said to be a morphism of truth values algebras if

-x ∈ B + 1 if and only if F (x) ∈ B + 2 , -if A ∈ A 1 then F (A) ∈ A 2 , if E ∈ E 1 then F (E) ∈ E 2 , -F ( ⊤1 ) = ⊤2 , F ( ⊥1 ) = ⊥2 , F (a ⇒1 b) = F (a) ⇒2 F (b), F (a ∧1 b) = F (a) ∧2 F (b), F (a ∨1 b) = F (a) ∨2 F (b), F ( ∀1 A) = ∀2 F (A), F ( ∃1 E) = ∃2 F (E).
Morphisms of pseudo-Heyting algebras are defined in a similar way except that the first condition is replaced by Remark. We have proved that, in the definition of Heyting algebras, the antisymmetry is useless and can be dropped. The equivalence of truth values algebras and pseudo-Heyting algebras shows that antisymmetry is the only property that can be dropped and that truth values algebras are, in some sense, the best possible generalization of Heyting algebras, as we cannot require less than closure by intuitionistic deduction rules.

-x ≤ 1 y if and only if F (x) ≤ 2 F (y).

Examples of truth values algebras

We have seen that the algebra {0, 1} is a truth value algebra and more generally that all Heyting algebras are truth values algebras. We give in this section two examples of truth values algebras that are not Heyting algebras.

Example 3. The truth value algebra T 1 is defined as follows. The set T 1 is {0, I, 1} and the set T + 1 is {I, 1}. The sets A and E are ℘(T 1 ). The functions ⊤, ⊥, ∧, ∨, ∀ and ∃ are the same as in the algebra {0, 1}, except that their value on I is the same as their value on 1. For instance the table of the operation ∨ is

0 I 1 0 0 1 1 I 1 1 1 1 1 1 1
The function ⇒ is defined by the table

0 I 1 0 1 1 1 I 0 1 1 1 0 I I
Notice that as I ⇒ 1 and 1 ⇒ I are both in T + 1 we have I ≤ 1 and 1 ≤ I. Hence the relation ≤ is not antisymmetric and the truth value algebra T 1 is not a Heyting algebra.

Example 4. The truth value algebra T 2 is similar to T 1 , except that the function ⇒ is defined by the table 0 I 1 0 1 1 I I 0 1 I 1 0 1 I

Ordered truth values algebras

We consider truth values algebras extended with an order relation ⊑ on B. This order relation extends to sets of truth values in a trivial way: A ⊑ B if for all x in A there exists a y in B such that x ⊑ y.

Definition 7 (Ordered truth values algebra).

An ordered truth values algebra is a truth values algebra together with a relation ⊑ on B such that -⊑ is an order relation, -B + is upward closed, -⊤ is a maximal element, -∧, ∨, ∀ and ∃ are monotonous, ⇒ is left anti-monotonous and right monotonous.

Definition 8 (Complete ordered truth values algebra).

A ordered truth values algebra is said to be complete if every subset of B has a greatest lower bound for ⊑. Notice that this implies that every subset also has a least upper bound. We write glb(a, b) and lub(a, b) the greatest lower bound and the least upper bound of a and b for the order ⊑.

Example 5. The algebra T 1 ordered by 0 ⊑ I ⊑ 1 is complete. Example 6. The algebra T 2 cannot be extended to a complete ordered algebra. Indeed the set {I, 1} would need to have a least upper bound. This least upper bound cannot be 0 because T + 2 would then not be upward closed. If it were 1 then we would have I ⊑ 1 and thus 1 ⇒ I ⊑ 1 ⇒ 1, i.e. 1 ⊑ I. Thus the relation ⊑ would not be antisymmetric. If it were I then we would have 1 ⊑ I and thus 1 ⇒ 1 ⊑ 1 ⇒ I, i.e. I ⊑ 1. Thus the relation ⊑ would not be antisymmetric.

Proposition 4. The order relation ⊑ is finer than ≤, i.e. if a ⊑ b then a ≤ b. Proof. If a ⊑ b, then a ⇒ a ⊑ a ⇒ b, hence a ⇒ b ∈ B + , i.e. a ≤ b.

Completion

We now want to prove that for any truth value algebra B, there is another truth value algebra B C that is full, ordered and complete and a morphism Φ from B to B C . Notice that we do not require the morphism Φ to be injective.

There are two ways to prove this, the first is to use Proposition 3 in a first step to build a truth value algebra B/B + that is a Heyting algebra and a morphism for B to B/B + and then apply in a second step MacNeille completion to the algebra B/B + to embed it into a full Heyting algebra. Together with its natural order, this algebra is a full, ordered and complete truth value algebra. The second is to apply MacNeille completion directly to B noticing that antisymmetry is not used in MacNeille completion, except to prove the injectivity of the morphism.

To keep the paper self-contained we follow this second way.

Definition 9 (Closure). Let X a subset of B, then the set of upper bounds of X is u(X) = {y | ∀x (x ∈ X ⇒ x ≤ y)} the set of lower bounds of X is l(X) = {y | ∀x (x ∈ X ⇒ y ≤ x)} and the closure of X is C(X) = l(u(X).
It is easily checked that

X ⊆ Y ⇒ u(Y ) ⊆ u(X) X ⊆ Y ⇒ l(Y ) ⊆ l(X) X ⊆ Y ⇒ C(X) ⊆ C(Y ) Proposition 7. X ⊆ C(X) Proof. Consider x ∈ X. For all y ∈ u(X), x ≤ y. Hence x ∈ l(u(X)). Proposition 8. If X ∈ E, then ∃ X ∈ C(X)
Proof. For all y ∈ u(X), ∃ X ≤ y. Hence ∃ X ∈ l(u(X)).

Definition 10 (Closed). A subset X of B is said to be closed if C(X) = Xor, equivalently, C(X) ⊆ X.
Proposition 9. Any set of the form C(X) is closed.

Proof. Consider an arbitrary set Z. Consider z ∈ Z. For all y ∈ l(Z), y ≤ z.

Hence z ∈ u(l(Z)). Thus, for an arbitrary Z, Z ⊆ u(l(Z)) and in particular

u(X) ⊆ u(l(u(X))). Thus l(u(l(u(X)))) ⊆ l(u(X)), i.e. C(C(X)) ⊆ C(X). Proposition 10. a ∈ C({b}) ⇔ a ≤ b C({a}) ⊆ C({b}) ⇔ a ≤ b If X is closed, x ∈ X
) a ≤ b. If C({a}) ⊆ C({b}) then {a} ⊆ C({a}) ⊆ C({b}). Hence a ∈ C({b}), i.e. a ≤ b. Conversely, if a ≤ b then a ∈ C({b}), {a} ⊆ C({b}), hence C({a}) ⊆ C(C({b})) = C({b}).
If X is closed, x ∈ X and y ≤ x then let z be an element of u(X), we have x ≤ z and y ≤ x, thus, by transitivity, y ≤ z, i.e. y ∈ l(u(X)) = C(X) = X. Proposition 11. Let B be a pseudo-Heyting algebra. Let B C be the set of closed subsets of B, ≤ C be inclusion,

A C = E C = ℘(B C ), ⊥C = C({ ⊥}), ⊤C = C({ ⊤}), ∧C be intersection, ∨C be defined by X ∨C Y = C(X ∪ Y ), ∀C be intersection, ∃C be defined by ∃C E = C( E), ⇒C be defined by X ⇒C Y = C({x})⊆X,Y ⊆C({y}) C({x ⇒ y}).
Then the structure ⟨B C , ≤ C , A C , E, ⊥C , ⊤C , ⇒C , ∧C , ∨C , ∀C , ∃C ⟩ is a full, ordered and complete Heyting algebra.

Proof. 1. Inclusion is trivially an order relation.

The set

C({ ⊥}) is closed. It is a minimum in B C , because if X is closed, it is a set of lower bounds and hence ⊥ ∈ X. Thus C({ ⊥}) ⊆ C(X) = X. 3. The set C({ ⊤}) is closed. It is a maximum in B C , because it is equal to B. 4.
Let us check that binary and arbitrary intersections of closed sets are closed sets. We detail only the case of the operation ∀, the binary operation being a particular case. If all elements of A are closed sets, we have for every Example 7. The algebra T 2 cannot be extended to a complete ordered algebra, but it can be embedded with a non injective morphism in the full ordered and complete algebra {0, 1}.

X in A, ∀C A ⊆ X, C( ∀C A) ⊆ C(X) = X. Thus C( ∀C A) ⊆ ∀C A.
if X is an element of E, X ⊆ E ⊆ C( E). Then, it is the least as, if A is an element of B C such that for all X in E, X ⊆ Z then E ⊆ Z hence C( E) ⊆ C(Z) and C( E) ⊆ Z. 6. The set C({x})⊆X,Y ⊆C({y}) C({x ⇒ y}) is closed as it is an intersection of closed sets. Let us check that X ≤ C A ⇒C B if and only if X ∧C A ⊆ B. Assume X ⊆ A ⇒C B and let x ∈ X ∧C A. Let b ∈ u(B). We have x ∈ X, thus x ∈ A ⇒C B. We have x ∈ A, thus C({x}) ⊆ C(A) = A. We have b ∈ u(B), thus ∀y (y ∈ B ⇒ y ≤ b), ∀y (y ∈ B ⇒ y ∈ C({b})) and B ⊆ C({b}). We have x ∈ A ⇒C B, C({x}) ⊆ A, and B ⊆ C({b}) thus x ∈ C({x ⇒ b}), i.e. x ≤ x ⇒ b, x ∧ x ≤ b, x ≤ b. Thus, for all b in u(B), x ≤ b, i.e. x ∈ l(u(B)), x ∈ C(B) and x ∈ B. Conversely, assume X ∧C A ⊆ B. Let x ∈ X. Let a such that C({a}) ⊆ A and b such that B ⊆ C({b}). We have x ∧ a ≤ x and x ∈ X, hence x ∧ a ∈ X. We have x ∧ a ≤ a ∈ C({a}) ⊆ A, hence x ∧ a ∈ A. Thus x ∧ a ∈ X ∧C A ⊆ B ⊆ C({b}). Therefore x ∧ a ∈ C({b}), x ∧ a ≤ b, x ≤ a ⇒ b and x ∈ C({a ⇒ b}). Thus x ∈ A ⇒C B.
∈ C({a}) ∪ C({b}), thus if x ∈ u(C({a}) ∪ C({b})), then a ≤ x. In a similar way, if x ∈ u(C({a}) ∪ C({b})), then b ≤ x. Thus if x ∈ u(C({a}) ∪ C({b})), then a ∨ b ≤ x, i.e. if x ∈ u(C({a}) ∪ C({b})), then x ∈ u({a ∨ b}) i.e. u(C({a}) ∪ C({b})) ⊆ u({a ∨ b}). Hence l(u({a ∨ b})) ⊆ l(u(C({a}) ∪ C({b}))) i.e. C({a ∨ b}) ⊆ C(C({a}) ∪ C({b}))) i.e. C({a ∨ b}) ⊆ C({a}) ∨C C({b})).
3 Predicate Logic

Models

Definition 11 (B-valued structure). Let L = ⟨f i , P j ⟩ be a language in predicate logic and B be a truth values algebra, a B-valued structure for the language L, M = ⟨M, B, fi , Pj ⟩ is a structure such that fi is a function from M n to M where n is the arity of the symbol f i and Pj is a function from M n to B where n is the arity of the symbol P i . This definition extends trivially to many-sorted languages.

Definition 12 (Denotation). Let B be a truth values algebra, M be a B-valued structure and ϕ be an assignment. The denotation A ϕ of a formula A in M is defined as follows

-x ϕ = ϕ(x), -f (t 1 , ..., t n ) ϕ = f ( t 1 ϕ , ..., t n ϕ ), -P (t 1 , ..., t n ) ϕ = P ( t 1 ϕ , ..., t n ϕ ), -⊤ ϕ = ⊤, -⊥ ϕ = ⊥, -A ⇒ B ϕ = A ϕ ⇒ B ϕ , -A ∧ B ϕ = A ϕ ∧ B ϕ , -A ∨ B ϕ = A ϕ ∨ B ϕ , -∀x A ϕ = ∀ { A ϕ+⟨x,e⟩ | e ∈ M}, -∃x A ϕ = ∃ { A ϕ+⟨x,e⟩ | e ∈ M}.
Notice that the denotation of a formula containing quantifiers may be undefined, but it is always defined if the truth value algebra is full.

Definition 13 (Model).

A formula A is said to be valid in a B-valued structure M, and the B-valued structure M is said to be a model of A, M |= A, if for all assignments ϕ, A ϕ is defined and is a positive truth value. The B-valued structure M is said to be a model of a theory T if it is a model of all the axioms of T .

Soundness and completeness

As the notion of truth values algebra extends that of Heyting algebra, the completeness theorem for the notion of model introduced above is a simple corollary of the completeness theorem for the notion of model based on Heyting algebras. But, it has a simpler direct proof. It is well-known that completeness proofs for boolean algebra valued models and Heyting algebra valued models are simpler than for {0, 1}-valued models. For truth values algebra valued models, it is even simpler. We want to prove that if A is valid in all models of T where it has a denotation then T ⊢ A. To do so, we consider a theory T and we construct a model of T such that the formulae valid in this model are the intuitionistic theorems of T .

Definition 14 (Lindenbaum model). Let T be a theory in a language L. Let S be an infinite set of constants and L ′ = L∪S. Let M be the set of closed terms of L ′ and B T be the set of closed formulae of L ′ . Let B + T be the set of elements A of B T , such that the sequent T ⊢ A is provable. Let A = E be the set of subsets of B T of the form {(t/x)A | t ∈ M} for some A. Notice that, in this case, the formula A is unique.

The operations ⊤, ⊥, ⇒, ∧ and ∨ are ⊤, ⊥, ⇒, ∧ and ∨. The operations ∀ and ∃ are defined as follows

-∀ {(t/x)A | t ∈ M} = (∀x A), -∃ {(t/x)A | t ∈ M} = (∃x A).
If f is a function symbol, we let f be the function mapping t 1 , ..., t n to f (t 1 , ..., t n ). If P is a predicate symbol, we let P be the function mapping t 1 , ..., t n to P (t 1 , ..., t n ). Proposition 14. The algebra B T is a truth values algebra.

Proof. The condition 1. to 11. are trivial recalling that B + T is the set of theorems of T . The condition 12. is a simple consequence of the definition of A and E.

For condition 13., consider a set A = {(t/x)P | t ∈ M} and c a constant occurring neither in T nor in P . If all elements of A are in B + T , (c/x)P is in B + T thus T ⊢ (c/x)P is provable. Thus, T ⊢ ∀x P is provable and ∀x P is in B + T , i.e. ∀ A is in B + T . For condition 14. consider an element A of A, by definition there exists a formula P such that A = {(t/x)P | t ∈ M} and we have ∀ A = ∀x P and ∀ (a ⇒ A) = ∀x (a ⇒ P ). Thus, the condition rephrases T ⊢ (∀x (a ⇒ P )) ⇒ a ⇒ ∀x P which is obvious as the formula (∀x (a ⇒ P )) ⇒ a ⇒ ∀x P is intuitionisticaly provable. The conditions 15., 16. and 17. are checked in a similar way. Proposition 15. Let A be a formula and ϕ be an assignment mapping the free variables of A to elements of M. Notice that ϕ is also a substitution and that ϕA is a closed formula. Then A ϕ is always defined and

A ϕ = ϕA
Proof. By induction over the structure of A. We consider only the case where Proof. If A is valid in the Lindenbaum model then for every assignment ϕ, A ϕ ∈ B + T , i.e. T ⊢ A ϕ is provable. Thus, T ⊢ ϕA is provable and in particular T ⊢ A is provable.

A = ∀x B. We have ∀x B ϕ = ∀ { (t/x)B ϕ | t ∈ M} = ∀ {ϕ((t/x)B) | t ∈ M} = ∀ {(t/x)(ϕB) | t ∈ M} = ∀x (ϕB) = ϕ(∀x B).

Proposition 17 (Completeness).

If A is valid in all the models of T where it is defined, then T ⊢ A.

Proof. It is valid in the Lindenbaum model of T .

Using Proposition 13, we can strengthen this completeness theorem. Proposition 18. If A is valid in all the models of T where the truth values algebra is full, ordered and complete then T ⊢ A.

The converse is a simple induction over proof structure.

Proposition 19 (Soundness). If T ⊢ A then A is valid in all the models of T where the truth value algebra is full, ordered and complete.

We finally get the following theorem.

Theorem 1. T ⊢ A if and only if

A is valid in all the models of T where the truth values algebra is full, ordered and complete.

Consistency Definition 15.

A theory is said to be consistent if there exists a non provable formula in this theory.

In the completeness theorem above, we did not assume the theory T to be consistent. If it is not, then the algebra of the Lindenbaum model is trivial, i.e. all truth values are positive and every formula is valid. But we have the following theorem.

Proposition 20. The theory T is consistent if and only if it has a B-valued model, for some non trivial full, ordered and complete truth values algebra B.

Proof. The algebra of the Lindenbaum model and its completion are non trivial.

Deduction modulo

Deduction modulo

In Deduction modulo [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Proof normalization modulo[END_REF], a theory is defined by a set of axioms T and a congruence ≡ defined by a confluent rewrite system rewriting terms to terms and atomic formulae to formulae. The deduction rules are modified to take the congruence ≡ into account. For instance, the modus ponens rule is not stated as usual

Γ ⊢ A ⇒ B Γ ⊢ A Γ ⊢ B but Γ ⊢ ≡ C Γ ⊢ ≡ A C ≡ A ⇒ B Γ ⊢ ≡ B
In deduction modulo, there are theories for which there exists proofs that do not normalize. For instance, in the theory formed with the rewrite rule P -→ (P ⇒ Q), the proof

axiom P ⊢ ≡ P ⇒ Q axiom P ⊢ ≡ P ⇒-elim P ⊢ ≡ Q ⇒-intro ⊢ ≡ P ⇒ Q axiom P ⊢ ≡ P ⇒ Q axiom P ⊢ ≡ P ⇒-elim P ⊢ ≡ Q ⇒-intro ⊢ ≡ P ⇒-elim ⊢ ≡ Q
does not normalize and, moreover, the formula Q has no normal proof.

But, as we shall see, in some other theories, such as the theory formed with the rewrite rule P -→ (Q ⇒ P ), all proofs strongly normalize.

In deduction modulo, like in predicate logic, normal proofs of a sequent of the form ⊢ ≡ A always end with an introduction rule. Thus, when a theory can be expressed in deduction modulo with rewrite rules only, i.e. with no axioms, in such a way that proofs modulo these rewrite rules strongly normalize, then the theory is consistent, it has the disjunction property and the witness property, various proof search methods for this theory are complete, ... Many theories can be expressed this way in deduction modulo, in particular arithmetic [START_REF] Dowek | Arithmetic as a theory modulo[END_REF] and simple type theory [START_REF] Dowek | HOL-lambda-sigma: an intentional firstorder expression of higher-order logic[END_REF] and the notion of cut of deduction modulo subsumes the ad hoc notions of cut defined for these theories. In the same way, if B be an arbitrary full, ordered and complete truth value algebra, then the theory P -→ (⊥ ⇒ P ) has a B-valued model.

Example 10. The theory P -→ (P ⇒ Q) has a {0, 1}-valued model ( P = Q = 1), but no T 1 -valued model. Indeed there is no 0 in the line 0 of the table of the function ⇒ of T 1 , no I in the line I and no 1 in the line 1.

Soundness and completeness

To extend the completeness and the soundness theorem to deduction modulo, we replace terms by classes of congruent terms and formulae by classes of congruent formulae.

Definition 17. Let T , ≡ be a theory in a language L. Let S be an infinite set of constants and L ′ = L ∪ S. We define an equivalence relation ∼ on formulae of L ′ inductively as the smallest congruence such that if

A ≡ B then A ∼ B, if A ∼ B and A ′ ∼ B ′ then (A ∧ A ′ ) ∼ (B ∧ B ′ ), (A ∨ A ′ ) ∼ (B ∨ B ′ ), and (A ⇒ A ′ ) ∼ (B ⇒ B ′ )
, and if for each term t there exist a term u such that (t/x)A ∼ (u/x)B and for each term u there exist a term t such that (u/x)B ∼ (t/x)A then ∀x A ∼ ∀x B and ∃x A ∼ ∃x B.

Remark that if we consider the congruence ≡ defined by the rewrite rule f (f (x)) -→ x we have ∀x P (x) ̸ ≡ ∀x P (f (x)) but we have ∀x P (x) ∼ ∀x P (f (x)) as P (x) and P (f (x)) have the same instances (the instance t in one formula corresponds to the instance f (t) in the other).

Proposition 21. If t ≡ u and A ∼ B then (t/x)A ∼ (u/x)B.

Proof. By induction on the derivation of

A ∼ B. Proposition 22. If A ∼ B then A ⇔ B is provable modulo ≡.
Proof. By induction on the derivation of A ∼ B if A = ∀x A ′ and B = ∀x B ′ and for each term t there exist a term u such that (t/x)A ∼ (u/x)B and for each term u there exist a term t such that (u/x)B ∼ (t/x)A then let c be a constant of S occurring neither in A nor in B. We have to prove the sequent ∀x A ′ ⊢ (c/x)B ′ . Let t be a term such that (t/x)A ′ ∼ (c/x)B ′ , by induction hypothesis we get (t/x)A ′ ⇔ (c/x)B ′ , and as we have ∀x A ′ we can deduce (t/x)A ′ , and thus (c/x)B ′ .

Definition 18 (The Lindenbaum model). Let T , ≡ be a theory in a language L. Let S be an infinite set of constants and L ′ = L ∪ S. Let M be the set of ≡-classes of closed terms of L ′ and B be the set of ∼-classes of closed formulae of L ′ . Let B + be the set of elements A of B, such that the sequent T ⊢ ≡ A is provable. Let A = E be the set of subsets of B of the form {(t/x)A/ ∼ | t ∈ M} for some A.

The operations ⊤, ⊥, ⇒, ∧ and ∨ are ⊤, ⊥, ⇒, ∧ and ∨ extended to ∼classes. To define the operations ∀ and ∃, we choose for each element a of A and E a formula A such that a = {(t/x)A/ ∼ | t ∈ M} and we let

-∀ a = (∀x A)/ ∼, -∃ a = (∃x A)/ ∼.
Notice that the elements (∀x A)/ ∼ and (∃x A)/ ∼ are independent of the choice of A.

If f is a function symbol, we let f be the function mapping the classes of t 1 , ..., t n to that of f (t 1 , ..., t n ). If P is a predicate symbol, we let P be the function mapping the classes of t 1 , ..., t n to that of P (t 1 , ..., t n ).

Proposition 23. Let A be a formula and ϕ be a assignment mapping the free variables of A to elements of M. Notice that ϕ is also a substitution and that ϕA is a closed formula. Then A ϕ = ϕA/ ∼. Proof. By induction over the structure of A. We consider only the case where A = ∀x B. We have ∀x

B ϕ = ∀ { B ϕ+(x=a) | a ∈ M}. By induction hypothesis, ∀x B ϕ = ∀ {(a/x)ϕB/ ∼ | a ∈ M} = (∀x ϕB)/ ∼= ϕ(∀x B)/ ∼.
Proposition 24. The algebra B is a truth values algebra.

Proof. The condition 1. to 11. are trivial using the fact that B + is the set of theorems of T , ≡. The condition 12. is a simple consequence of the definition of A and E.

For condition 13., consider a set A in A and P the formula associated to this set, and c a constant occurring neither in T nor in the rewrite system defining the congruence ≡, nor in P . If all elements of A are in B + , (c/x)P is in B + thus T ⊢ ≡ (c/x)P is provable. Thus, T ⊢ ≡ ∀x P is provable and ∀x P is in B + , i.e. ∀ A is in B + .

For condition 14., consider an element A of A and the formula P associated to this element and Q the formula associated to the set a ⇒ A. By Proposition 22, the formula (∀x (a ⇒ P )) ⇔ (∀x Q) is provable. We have ∀ A = ∀x P and ∀ (a ⇒ A) = ∀x Q. Thus, the condition rephrases

T ⊢ ≡ ∀x Q ⇒ a ⇒ ∀x P
which is a consequence of the fact that the formula (∀x (a ⇒ P )) ⇔ (∀x Q) is provable. The conditions 15., 16. and 17. are checked in a similar way.

Proposition 25. The closed formulae valid in the Lindenbaum model of T , ≡ in L are intuitionistic theorems of T , ≡.

Proof. If A is valid in the Lindenbaum model, then for every assignment ϕ, A ϕ ∈ B + , i.e. T ⊢ ≡ A ϕ is provable in deduction modulo. Thus, T ⊢ ≡ ϕA is provable in deduction modulo and in particular T ⊢ ≡ A is provable in deduction modulo.

Proposition 26 (Completeness). If A is valid in all the models of T , ≡ where it is defined, then T ⊢ ≡ A.

Proof. It is valid in the Lindenbaum model of T , ≡.

Using Proposition 13, we can strengthen this completeness theorem.

Proposition 27. If A is valid in all the models of T , ≡ where the truth values algebra is full, ordered and complete then T ⊢ ≡ A.

The converse is a simple induction over proof structure.

Proposition 28 (Soundness). If T ⊢ ≡ A then A is valid in all the models of T , ≡ where the truth value algebra is full, ordered and complete.

We finally get the following theorem.

Theorem 2. T ⊢ ≡ A if and only if A is valid in all the models of T , ≡ where the truth values algebra is full, ordered and complete.

Consistency

Proposition 29. The theory T , ≡ is consistent if and only if it has a B-valued model, for some non trivial full, ordered and complete truth values algebra B.

Proof. The algebra of the Lindenbaum model and its completion are non trivial.

Definition

By Proposition 29, a theory is consistent if it has a B-valued model for some non trivial full, ordered and complete truth values algebra. We now strengthen this condition and require that the theory has a B-valued model for all full, ordered and complete truth values algebras B.

Definition 19 (Super-consistent). A theory T , ≡ in deduction modulo is super-consistent if it has a B-valued model for all full, ordered and complete truth values algebras B.

Notice that, as there exists non trivial full, ordered and complete truth values algebras (e.g. {0, 1}), super-consistent theories are consistent.

Examples of super-consistent theories

We have seen that the theories P -→ (Q ⇒ R) and P -→ (Q ⇒ P ) are super-consistent, but that the theory P -→ (P ⇒ Q) is not. We give other examples of super-consistent theory. In particular, we show that all the theories that have been proved to have the strong normalization property in [START_REF] Dowek | Proof normalization modulo[END_REF][START_REF] Dowek | Arithmetic as a theory modulo[END_REF] are super-consistent.

Definition 20 (Simple type theory). Simple type theory is a many-sorted theory defined as follows. The sorts are inductively defined by ι and o are sorts and if T and U are sorts then T → U is a sort. The language contains the constants S T,U,V of sort Definition 21 (Arithmetic). Arithmetic is a many-sorted theory defined as follows. The sorts are ι and κ. The language contains the constant 0 of sort ι, the function symbols S and Pred of rank ⟨ι, ι⟩ and + and × of rank ⟨ι, ι, ι⟩, the predicate symbols = of rank ⟨ι, ι⟩, Null and N of rank ⟨ι⟩ and ∈ of rank ⟨ι, κ⟩ and for each formula P in the language 0, S, Pred , +, ×, =, Null and N and whose free variables are among x, y 1 , . . . , y n of sort ι, the function symbol f x,y1,...,yn,P of rank ⟨ι, . . . , ι, κ⟩. The rewrite rules are x ∈ f x,y1,...,yn,P (y 1 , . . . , y n )

(T → U → V ) → (T → U ) → T → V , K T,U of sort T → U → T , ⊤ of
α(α(K T,U , x), y) -→ x ε( ⊤) -→ ⊤ ε( ⊥) -→ ⊥ ε(α(α( ⇒, x), y)) -→ ε(x) ⇒ ε(y) ε(α(α( ∧, x), y)) -→ ε(x) ∧ ε(y) ε(α(α( ∨, x), y)) -→ ε(x) ∨ ε(y) ε(α( ∀T , x)) -→ ∀y ε(α(x, y)) ε(α( ∃T , x)) -→ ∃y ε(α(x,
-→ P y = z -→ ∀p (y ∈ p ⇒ z ∈ p) N (n) -→ ∀p (0 ∈ p ⇒ ∀y (N (y) ⇒ y ∈ p ⇒ S(y) ∈ p) ⇒ n ∈ p) Pred (0) -→ 0 Pred (S(x)) -→ x Null (0) -→ ⊤ Null (S(x)) -→ ⊥ 0 + y -→ y S(x) + y -→ S(x + y) 0 × y -→ 0 S(x) × y -→ x × y + y Proposition 31. Arithmetic is super-consistent.
Proof. Let B be a full, ordered and complete truth value algebra. We take M ι = N, M κ = B N . The denotations of 0, S, +, ×, Pred are obvious. We take N ull (0) = ⊤, N ull (n) = ⊥ if n ̸ = 0. The denotation of ∈ is the function mapping n and f to f (n). Then, we can define the denotation of ∀p (y ∈ p ⇒ z ∈ p) and the denotation of = accordingly.

To define the denotation of N , for each function f of B N we can define an interpretation M f of the language of the formula

∀p (0 ∈ p ⇒ ∀y (N (y) ⇒ y ∈ p ⇒ S(y) ∈ p) ⇒ n ∈ p)
where the symbol N is interpreted by the function f . We define the function Φ from B N to B N mapping f to the function mapping the natural number x to the truth value

∀p (0 ∈ p ⇒ ∀y (N (y) ⇒ y ∈ p ⇒ S(y) ∈ p) ⇒ n ∈ p) M f x/n
The order on B N defined by f ⊑ g if for all n, f (n) ⊑ g(n) is a complete order and the function Φ is monotonous as the occurrence of N is positive in

∀p (0 ∈ p ⇒ ∀y (N (y) ⇒ y ∈ p ⇒ S(y) ∈ p) ⇒ n ∈ p)
Hence it has a fixed point g. We interpret the symbol N by the function g. Finally, the denotation of the symbols of the form f x,y1,...,yn,P is defined in the obvious way.

Proposition 32 (Quantifier free). A theory defined by a confluent and terminating rewrite systems such that no quantifier appears in the rewrite rules is super-consistent. For instance, the theory defined by the rewrite system P -→ Q ⇒ R is super-consistent.

Proof. Let B be an arbitrary full truth value algebra. We associate an element of B to each normal closed quantifier free formula as follows: if A is atomic then

|A| = ⊤, |⊤| = ⊤, |⊥| = ⊥, |A ⇒ B| = |A| ⇒ |B|, |A ∧ B| = |A| ∧ |B|, |A ∨ B| = |A| ∨ |B|.
We then define a B-valued model as follows: M is the set of normal closed terms, f (t 1 , . . . , t n ) = f (t 1 , . . . , t n ) ↓, P (t 1 , . . . , t n ) = |P (t 1 , . . . , t n ) ↓ | where a ↓ is the normal form of the a.

Proposition 33 (Positive terminating). A theory defined by a confluent and terminating rewrite systems such that all atomic formulae appear at positive occurrences in the rewrite rules is super-consistent. For instance the theory defined by the rewrite system P (0) -→ ∀x P (x) is super-consistent.

Proof. Consider a full, ordered and complete truth value algebra B. Let T be the set of closed terms and M = T / ≡. Let f be the function mapping the classes e 1 , ..., e n to the class of the term f (t 1 , . . . , t n ) where t 1 , ..., t n are elements of e 1 , ..., e n (since the relation ≡ is a congruence, this class does not depend of the choice of representatives). Let C be the set of models that have the domain M, the truth value algebra B and where the function symbols f are interpreted by the functions f . Two models of C differ only by the interpretation of predicate symbols. Let M 1 and M 2 be two models of the class C, we say that M 1 ⊑ M 2 if and only if for every predicate symbol P and sequence of elements of M e 1 , . . . , e n , we have P M1 (e 1 , . . . , e n ) ⊑ P M2 (e 1 , . . . , e n )

As the algebra B is complete, the set C is a complete lattice for the order ⊑. Let F be the function from C to C defined by P F (M) (e 1 , . . . , e n ) = P (e 1 , . . . , e n ) ↓ M ∅ As all atomic formulae appear at positive occurrences in the rewrite system, the function F is monotone. Hence, as C is a complete lattice, it has a fixed point. This fixed point is a B-valued model of the theory.

Proposition 34 (Positive deterministic). A theory defined by a rewrite systems such that each atomic formula has at most one one-step reduct and all atomic formulae appear at positive occurrences in the rewrite rules is superconsistent. For instance, the theory defined by the rewrite system P -→ (P ∧ P ) is super-consistent.

Proof. As in the proof of Proposition 33, we consider a full, ordered and complete truth value algebra B and we define the complete lattice C of models.

Let F be the function from C to C defined by

P F (M) (t 1 , . . . , t n ) = P (t 1 , . . . , t n )+ M ∅
where A+ is the unique one-step reduct of A if it exists and A otherwise. As all atomic formulae appear at positive occurrences in the rewrite system, the function F is monotone. Hence, as C is a complete lattice, it has a fixed point. This fixed point is a B-valued model of the theory.

Normalization

We have seen that the theory P -→ (P ⇒ Q), that does not have the strong normalization property, is consistent but not super-consistent, i.e. it has B-valued models for some non trivial, full, ordered and complete truth values algebras B, but not all. We prove now that, in contrast, all super-consistent theories have the strong normalization property. To prove this, we build a particular full, ordered and complete truth values algebra: the algebra of reducibility candidates. We refer, for instance, to [START_REF] Dowek | Proof normalization modulo[END_REF] for the definition of proof-terms, neutral proofterms and of proof-term reduction ▷ and we define the following operations on sets of proofs.

Definition 22. -The set ⊤ is the set of strongly normalizing proof-terms.

-The set ⊥ is the set of strongly normalizing proof-terms.

-If a and b are two sets of proofs-terms, then a ⇒ b is the set of strongly normalizing proof-terms π such that if π reduces to λα π 1 then for every π ′ in a, (π ′ /α)π 1 is in b. -If a and b are two sets of proof-terms, then then a ∧ b is the set of strongly normalizing proof-terms π such that if π reduces to ⟨π 1 , π 2 ⟩ then π 1 is in a and π 2 is in b. -If a and b are two sets of proof-terms, then a ∨ b is the set of strongly normalizing proof-terms π such that if π reduces to i(π 1 ) (resp. j(π 2 )) then π 1 (resp. π 2 ) is in a (resp. b). -If A is a set of sets of proof-terms, then ∀ A is the set of strongly normalizing proof-terms π such that if π reduces to λx π 1 then for every term t and every element a of A, (t/x)π 1 is in a. -If A is a set of sets of proof-terms, then ∃ A is the set of strongly normalizing proof-terms π such that if π reduces to ⟨t, π 1 ⟩, there exists an element a of A such that π 1 is an element of a.

Definition 23 (Reducibility candidate). A set R of proof-terms is a reducibility candidate if

-if π ∈ R, then π is strongly normalizable, -if π ∈ R and π ▷ * π ′ then π ′ ∈ R, -if π is neutral and if for every π ′ such that π ▷ 1 π ′ , π ′ ∈ R then π ∈ R.
Proposition 35. The set of reducibility candidates is closed by the operations of Definition 22.

Proof. All the cases are similar. Let us detail, for instance, the case of the operation ∀. Let A be a set of candidates and let us prove that the set ∀ A is a candidate.

By definition, all proof-terms of ∀ A are strongly normalizing. Closure by reduction is a simple consequence of the fact that if π ∈ ∀ A and π ▷ * π ′ then π is strongly normalizing and thus so is π ′ and if π ′ reduces to λx π 1 then so does π and thus for every term t and every a in A, (t/x)π 1 is in a. Now, assume that π is a neutral proof-term and that for every π ′ such that π ▷ 1 π ′ , π ′ ∈ ∀ A. We want to prove that π is in ∀ A. Following the definition of ∀ A, we first prove that π is strongly normalizing and then that if it reduces to λx π 1 then for every term t and every a in A, (t/x)π 1 is in a.

Consider a reduction sequence issued from π. If it is empty it is finite. Otherwise it has the form π ▷ 1 π 2 ▷ 1 ... The proof-term π 2 is an element of ∀ A thus it is strongly normalizing and the reduction sequence is finite. If π reduces to λx π 1 then consider a reduction sequence from π to λx π 1 . As π is neutral and λx π 1 is not, this sequence is not empty. Thus, there exists a proof-term π 2 such that π ▷ 1 π 2 ▷ * λx π 1 . We have π 2 ∈ ∀ A and thus for every term t and every a in A, (t/x)π 1 is in a.

Definition 24 (The algebra of reducibility candidates). The set B is the set of reducibility candidates. The set B + may be any set closed by intuitionistic deduction rules, e.g. the set of all candidates. The sets A and E are ℘(B). The operations are those of definition 22. The order ⊑ is inclusion.

Theorem 3 (Normalization). If the theory T , ≡ is super-consistent, then all proofs strongly normalize in T , ≡.

Proof. Consider the full, ordered and complete truth values algebra B of reducibility candidates. As it is super-consistent, the theory T , ≡ has a B-valued model. This model is a reducibility candidate valued model of ≡ [START_REF] Dowek | Proof normalization modulo[END_REF], called premodels there. Hence all proofs strongly normalize in T , ≡.

An alternative would be to define the set of candidates directly as the smallest set of sets of proofs closed by the operations of definition 22 and arbitrary intersections, like [START_REF] Parigot | Strong normalization for the second orclassical natural deduction[END_REF].

Notice that the pre-order ≤ is trivial and thus not antisymmetric. Hence, the truth values algebra of reducibility candidates is not a Heyting algebra. The fact that the choice of the set B + is immaterial is due to the fact that B + matters for the interpretation of axioms but not for that of the congruence and cut elimination is a property of the congruence of a theory, not of its axioms.

We have generalized the notion of Heyting algebra into a notion of truth values algebra and proved that a theory is consistent if and only if it has a B-valued model for some non trivial full, ordered and complete truth values algebra B. Unlike Heyting algebra valued models, truth values algebra valued models allow to distinguish computational equivalence from provable equivalence.

When a theory has a B-valued model for all full, ordered and complete truth values algebras, it is said to be super-consistent and all proofs strongly normalize in this theory. Proving strong normalization by proving super-consistency is easier than proving strong normalization directly. For instance the proof that simple type theory is super-consistent (Proposition 30) takes only a few lines. All the technicalities related to the notion of reducibility candidate are now hidden in the proof that super-consistency implies strong normalization and are not used in the proof that the theory of interest is super-consistent.

The notion of super-consistency is a model theoretic sufficient condition for strong normalization. It remains to understand if it also a necessary condition or if some theories have the strong normalization property without being super-consistent. To prove that strong normalization implies super-consistency, we might need to restrict further the notion of super-consistency. For instance, we have already restricted it by considering only ordered and complete truth values algebras. Indeed, without such a completeness property, we could not use the fixed point theorem to prove that the theory P -→ (⊥ ⇒ P ) had a Bvalued model for all B, and indeed, this theory does not have a T 2 -valued model. Thus, the fact that the algebra of reducibility candidates, ordered by inclusion, is complete seems to be an essential property that needs to be kept when abstracting on reducibility candidates. It remains to understand if there are other essential properties of candidates that need to be kept this way, so that strong normalization may imply super-consistency.

  and a ≤ b ⇒ c if and only if a ∧ b ≤ c. Proposition 1. Consider a truth values algebra ⟨B, B + , A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ then the algebra ⟨B, ≤, A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩ where the relation ≤ is defined by a ≤ b if and only if a ⇒ b ∈ B + is a pseudo-Heyting algebra.

6 .

 6 We have ( ⊤ ∧ a) ∧ b ≤ ⊤ ∧ a ≤ a and ( ⊤ ∧ a) ∧ b ≤ b. Hence ( ⊤ ∧ a) ∧ b ≤ a ∧ b and ⊤ ≤ a ⇒ b ⇒ (a ∧ b). 7. We have ⊤ ∧ (a ∧ b) ≤ (a ∧ b) ≤ a. Hence ⊤ ≤ (a ∧ b) ⇒ a. 8. We have ⊤ ∧ (a ∧ b) ≤ (a ∧ b) ≤ b. Hence ⊤ ≤ (a ∧ b) ⇒ b. 9. We have ⊤ ∧ a ≤ a ≤ (a ∨ b). Hence ⊤ ≤ a ⇒ (a ∨ b). 10. We have ⊤ ∧ b ≤ b ≤ (a ∨ b). Hence ⊤ ≤ b ⇒ (a ∨ b). 11. Let x = ⊤ ∧ (a ∨ b) ∧ (a ⇒ c) ∧ (b ⇒ c). We have x ≤ a ∨ b, x ≤ a ⇒ c and x ≤ b ⇒ c. We have x ≤ a ∨ b and x ≤ x, hence x ≤ (a ∨ b) ∧ x. We have a ∧ x ≤ x ∧ a ≤ c, thus a ≤ x ⇒ c and, in a similar way, b ≤ x ⇒ c. Thus, we have a ∨ b ≤ x ⇒ c, i.e. (a ∨ b) ∧ x ≤ c. By transitivity, we conclude x ≤ c. Hence ⊤ ≤ (a ∨ b) ⇒ (a ⇒ c) ⇒ (b ⇒ c) ⇒ c. 12. The closure conditions of A and E are the same.

Proposition 3 .

 3 Let B be a pseudo-Heyting algebra, then there exists a pseudo-Heyting algebra B/B + that is a Heyting algebra and a morphism of pseudo-Heyting algebras Φ from B to B/B + . Proof. We define a relation ≃ on elements of B by a ≃ b if and only if a ≤ b and b ≤ a. It is routine to check that this relation is an equivalence relation and that all the operations of B are compatible with this relation. We define B/B + as the quotient B/ ≃ and the morphism Φ by Φ(a) = a/ ≃.

Proposition 5 .Proposition 6 .

 56 glb(a, b) ≤ a ∧ b ≤ glb(a ∧ ⊤, ⊤ ∧ b) Proof. We have glb(a, b) ⊑ a and glb(a, b) ⊑ b. Thus, by Proposition 4, glb(a, b) ≤ a and glb(a, b) ≤ b. Thus glb(a, b) ≤ a ∧ b. We have a ⊑ a and b ⊑ ⊤ thus a ∧ b ⊑ a ∧ ⊤. Similarly, a ∧ b ⊑ ⊤ ∧ b. Thus a ∧ b ⊑ glb(a ∧ ⊤, ⊤ ∧ b) and, by Proposition 4, a ∧ b ≤ glb(a ∧ ⊤, ⊤ ∧ b). In a Heyting algebra, ≤ and ⊑ are extensionally equal, i.e. a ⊑ b if and only if a ≤ b. Proof. In a Heyting algebra the relation ≤ is antisymmetric and a = a ∧ ⊤ = ⊤ ∧ a. Thus, from Proposition 5, we get glb(a, b) = a ∧ b. If a ≤ b, we have a ∧ b = a, thus glb(a, b) = a, thus a ⊑ b. Conversely, by Proposition 4, if a ⊑ b then a ≤ b.

Proposition 12 .

 12 The function a → C({a}) is a morphism of pseudo-Heyting algebras. Proof. 1. a ≤ b ⇔ C({a}) ⊆ C({b}). 2. C({ ⊤}) = ⊤C by definition. 3. C({ ⊥}) = ⊥C by definition. 4. C({a ∧ b}) = C({a}) ∧C C({b}). Indeed x ∈ C({a ∧ b}) if and only if x ≤ a ∧ b if and only if x ≤ a and x ≤ b if and only if x ∈ C({a}) and x ∈ C({b}) if and only if x ∈ C({a}) ∧C ({b}). 5. C({a ∨ b}) = C({a}) ∨C C({b}). Indeed we have a

  Conversely, we have a ≤ a ∨ b, thus C({a}) ⊆ C({a ∨ b}). In a similar way C({b}) ⊆ C({a ∨ b}). Thus C({a}) ∪ C({b}) ⊆ C({a ∨ b}) andC(C({a}) ∪ C({b})) ⊆ C(C({a ∨ b})) i.e. C({a}) ∨C C({b}) ⊆ C({a ∨ b}). 6. C({ ∀ A}) = ∀C {C({a}) | a ∈ A}. Indeed, x ∈ C({ ∀ A}) ifand only if x ≤ ∀ A if and only if for all a in A, x ≤ a if and only if for all a in A, x ∈ C({a}) if and only if x ∈ ∀C {C({a}) | a ∈ A}. 7. C({ ∃ E}) = ∃C {C({e}) | e ∈ E}. Indeed, for all e in E we have e ∈ C({e}) and thus E ⊆ {C({e}) | e ∈ E} and C(E) ⊆ C( {C({e}) | e ∈ E}) i.e. C(E) ⊆ ∃C {C({e}) | e ∈ E}. As, by Proposition 8, ∃ E ∈ C(E), we have C({ ∃ E}) ⊆ C(E), and thus C({ ∃ E}) ⊆ ∃C {C({e}) | e ∈ E}. Conversely, for all e in E, e ≤ ∃ E, hence C({e}) ⊆ C({ ∃ E}). Thus, {C({e}) | e ∈ E} ⊆ C({ ∃ E}) and C( {C({e}) | e ∈ E}) ⊆ C({ ∃ E}) i.e. ∃C {C({e}) | e ∈ E} ⊆ C({ ∃ E}). 8. C({a ⇒ b}) = C({a}) ⇒C C({b}). Indeed, z ∈ C({a}) ⇒C C({b}) if and only if for all x and y such that C({x}) ⊆ C({a}) and C({b}) ⊆ C({y}) we have z ∈ C({x ⇒ y}) if and only if for all x and y such that x ≤ a and b ≤ y, we have z ≤ x ⇒ y if and only if z ≤ a ⇒ b if and only if z ∈ C({a ⇒ b}). Proposition 13. Let B be a truth value algebra, then there exists a full, ordered and complete truth value algebra B C and a morphism of truth values algebras from B to B C . Proof. The Heyting algebra B C is a full, ordered and complete truth value algebra and the function a → C({a}) is a morphism of truth values algebras.

Proposition 16 .

 16 The closed formulae valid in the Lindenbaum model of T in L are intuitionistic theorems of T .

4. 2

 2 ModelsDefinition 16 (Model). Let T , ≡ be a theory in deduction modulo. The Bvalued structure M is said to be a model of the theory T , ≡ if all axioms of T are valid in M and for all terms or formulae A and B such that A ≡ B and assignments ϕ, A ϕ and B ϕ are defined and A ϕ = B ϕ .Example 8. Let B be an arbitrary truth value algebra, then the theory P -→ (Q ⇒ R) has a B-valued model. We take P = ( ⊤ ⇒ ⊤) and Q = R = ⊤.Example 9. Let B be an arbitrary full, ordered and complete truth value algebra, then the theory P -→ (Q ⇒ P ) has a B-valued model. The function a → ( ⊥ ⇒ a) is monotonous for the order ⊑ and this order is complete. Hence, it has a fixed point b. We define a B-valued model of this theory by P = b and Q = ⊥.

  sort o and ⊥ of sort o, ⇒, ∧ and ∨ of sort o → o → o, ∀T and ∃T of sort (T → o) → o, the function symbols α T,U of rank ⟨T → U, T, U ⟩ and the predicate symbol ε of rank ⟨o⟩. The rules are α(α(α(S T,U,V , x), y), z) -→ α(α(x, z), α(y, z))

  y)) Proposition 30. Simple type theory is super-consistent. Proof. Let B be a full truth values algebra. The model M ι = {0}, M o = B, M T →U = M M T U , ŜT,U,V = a → (b → (c → a(c)(b(c)))), KT,U = a → (b → a), α(a, b) = a(b), ε(a) = a, ⊤ = ⊤, ⊥ = ⊥, ⇒ = ⇒, ∧ = ∧, ∨ = ∨, ∀T = a → ∀(Range(a)), ∃T = a → ∃(Range(a)) where Range(a) is the range of the function a, is a B-valued model of simple type theory.

  condition 10. -Using 1. 2. 3. and 11. we get that if a ⇒ c ∈ B + and b ⇒ c ∈ B + then (a ∨ b) ⇒ c ∈ B + . -The closure conditions are 12. -If a ∈ A then ( ∀ A) ⇒ a ∈ B + is condition 15. -From 13. and 14. we get if for all a ∈ A b ⇒ a ∈ B + , then b ⇒ ∀ A ∈ B + , -If a ∈ A then a ⇒ ( ∃ A) ∈ B + is condition 16. Let us first prove the following lemma: if x ≤ a ⇒ b and x ≤ a then x ≤ b. From x ≤ x and x ≤ a, we get x ≤ x ∧ a and as x ≤ a ⇒ b, we have x ∧ a ≤ b. By transitivity, we get x ≤ b. 1. Using the lemma above, we get that if ⊤ ≤ a ⇒ b and ⊤

	-From 1. 2. 3. 13. and 17. we get that if for all a ∈ A a ⇒ b ∈ B + , then
	∃ A ⇒ b ∈ B + ,
	-From 1. 2. 3. 6. 7. and 8. we get that a ⇒ (b ⇒ c) ∈ B + if and only if
	(a ∧ b) ⇒ c ∈ B + .
	Proposition 2. Consider a pseudo-Heyting algebra ⟨B, ≤, A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩,
	then the algebra ⟨B, B + , A, E, ⊤, ⊥, ⇒, ∧, ∨, ∀, ∃⟩, where B + = {x | ⊤ ≤ x} is a
	truth values algebra.
	Proof.

  Moreover, binary and arbitrary intersections are obviously greatest lower bounds in B C . 5. The sets C(X ∪ Y ) and C( E) are closed. Let us check that they are least upper bounds. Again, we detail case of the case of the operation ∃C , the binary operation being a particular case. The operation ∃C is an upper bound as

Acknowledgments

Thierry Coquand suggested to characterize truth values algebras as pseudo-Heyting algebras. Lisa Allali, Frédéric Blanqui, Olivier Hermant and Milly Maietti provided many helpful comments on a previous version of the paper.


Introduction

Flash absorption spectroscopy is used to monitor the kinetics and spectra of flash- induced absorption changes, which may provide information on molecular events in the sample. Usually, the system is perturbed by a light pulse (actinic flash) which is short compared to the characteristic time of the reaction(s) to be studied. The absorption changes induced by the actinic flash are probed by a usually continuous light beam (measuring light) passing through the sample. This technique has proven particularly useful in photosynthesis research, because the stimulus, light, is the natural driving force of photosynthesis, and because many of the photosynthetic light reactions are accompanied by rather characteristic absorption changes in the visible, near UV and near infrared spectral regions.

Flash absorption spectroscopy and its application in photosynthesis research has been reviewed in detail by Junge in 1976 [1]. In this contribution, I will first summarise the principle and the instrumentation of flash absorption spectroscopy and then focus on practical aspects, some of which are related to the use of lasers as measuring light sources and were not yet treated in the review by Junge Il]. 2. Principle Suppose that the sample to be studied is contained in a cuvette with an optical path I (Fig. l) and that the actinic flash induces a reaction X + Y. This reaction will be accompanied by an absorbance change AA (at wavelength 1") AA: Ae'Ac'l (l) where Ae = eyex is the difference of the molar decadic absorption coefficients (at wavelength )") of Y and X, and Ac is the change in concentration of the product Y (Eq. I can easily be extended to more complicated reactions). The cuvette is crossed by a beam Kev words: Flash absorption spectroscopy; Photosynthesis Actinic flash Po(À) P, P' Photodetecfor (l'leasuring beaml '1 Vottage (Vl ôv Fig. 1. Principle of measurement of flash-induced absorption changes of continuous monochromatic light of wavelength l" (monitoring or measuring light) with a radiant power Po at the entrance of the cuvette. The measuring light is attenuated by the absorption due to the molecules in the sample (including molecules which do not participate in the flash induced reaction), the windows of the cuvette and possibly other optical elements between the cuvette and the photodetector. The radiant power seen by the photodetector is P prior to the actinic flash and P'(t) at time t after the actinic flash. ÀP = P'-P can be positive or negative, depending on whether the reaction is accompanied by a bleaching or by an absorption increase. Using the definition of absorbance, A: lg(Po/P), we can write (before the flash) A.u*pr" * Aoth". "r". : lg(PoAE)

(after the flash) A'.u.pr" f Aorh"r"l.,n = lg(P¡/P') Substituting A'.u^pt" -A.u*pl" = AA, one obtains AA = lg(P/P') : lg[P/(P+AP)] : -lg(l+APAE)

(2)

In the limit of small absorbance changes (i.e. AP/P << l), Eq. 2 can be approximated by The photodetector usually produces a photocurrent proportional to the incident radiant power (at a given wavelength) which is afterwards converted to a voltage V (which varies by AV), so that AV/V: APAE. Recording the time course of AV, the kinetics of the flash induced reaction(s) can be measured. A difference spectrum of the absorbance changes at a given time can be recorded by repeating the measurements at various waveiengths l. of the monitoring light and then plotting-(U23) 'AP/P versus 1". These measurements directly give spectral and kinetic information They often allow determination of the species involved (e.g. the electron carriers in photosynthesis) and of the sequence and kinetics ofthe flash-induced reaction(s).

.,f 3. Main elements of the experimental set-up Actinic flash its duration has to be short compared to the kinetics of the reaction to be studied. In the time range above a few microseconds, xenon flashes may be used, combined with optical filters if excitation at a special wavelength is required. For faster reactions, pulse lasers have to be used. They are inherently monochromatic; with some of them (e.g. dye lasers) the emission wavelength can be tuned.

Meaxtring light

Conventional lamps (tungsten, xenon, mercury etc.) or continuous lasers may be used. As most conventional lamps have a broad emission spectrum, monochromators or optical filters have to be used to obtain (nearly) monochromatic light. Lasers have the advantage of emitting monochromatic light of high intensity. They can be focused on a small photodetector. Tuning of the wavelength is limited, however.

Detection system

It consists in general of a photodetector (photodiode or photomultiplier), electronic amplifiers and a transient recorder (analog/digital converter and storage element). Photomultipliers provide internal, low-noise amplification of the photocurrent and are the best choice when the measuring light intensity is low. At higher intensities, they become saturated, and a photodiode with subsequent electronic amplifier should be used. The amplifier is often the main source of noise in such a detection system.

In many cases it is necessary to place optical filters in front of the photodetector.

They transmit the measuring light, but block scattered light from the actinic flash which otherwise could be misinterpreted as a transient bleaching of the sample. 4. Some practical aspects

Time resolution

The time resolution of the apparatus can be limited by the duration of the actinic flash, the electronic bandwidth of the detection system or by the sampling rate of the transient recorder. The fastest commercially available transient recorders have an electronic bandwidth from DC to about I GHz and sampling rates of a few Gigasamples T per second, allowing a time resolution in the order of 1 ns. It should also be mentioned that the response of fast detection systems is often far from perfect and can falsify the kinetics considerably (e.g. overshooting upon a fast transition; see [2] for a method of detector testing).

Faster reactions (down to the fs range) can be resolved by the "pump and probe" technique where the continuous measuring light is replaced by short laser pulses ("probe") at various delay times after the actinic flash ("pump"). As the time resolution is obtained by delaying the probe pulses, an integral measurement of the energy of the probe pulse behind the sample is sufficient and a fast detection system is not required (see 13] for a recent review on this technique; the same principle can also be used on slower tir¡e scales [4]).

2. Signal-to-noise ratio

As the flash-induced absorbance changes in photosynthetic samples from plants are usually rather small (rarely larger than l0-3), monitoring by flash absorption spectroscopy is often hindered by a insufficient signal to noise ratio (SAI), expressed as the ratio of AV and the noise voltag€ Vn, i.e SÂ'{: AV/V.. When the noise is purely random ("white noise"), Vn is proportional to the square root of the electronic bandwidth of the detection system, so that the difficulties to obtain a sufücient signal-to-noise ration increase with increasing rate of the reaction to be studied.

It is possible to improve the signal-to-noise ratio by adding up a certain number (n) of signals measured under identical conditions. Because the accumulated signal amplitude increases proportional to n, but the random noise only proportionaltoJi, SAI increases proportional toJi. However, due to practical limitations (time, quantity of sample) it is often not convenient to accumulate a too large number of signals. Therefore, one should first look for other possibilities to improve the signal-to-noise ratio.

The noise originates from three major sources:

(l) From the statistics of the photons of the measuring light and of the photoelectrons created in the detector (shot noise); the shot noise voltage is proportional to the square root of the primary photocurrent in the detector.

(2) From additional fluctuations of the radiant power emitted by the measuring light source; the resulting noise voltage is proportional to the radiant power reaching the detector and hence proportional to the photocurrent.

( 3) From the thermal movements of the electrons in the detection system (thermal noise); the thermal noise is independent of the measuring light.

In a widely used set-up, a tungsten incandescent lamp serves as the measuring light source, and a photomultiplier as the detector. In this case, noise sources (2) and (3) are usually negligible, and the signal-to-noise ratio increases proportional to the square root of the radiant power P reaching the detector (according to Eq. 3, AP cc P for a given absorbance change AA of the sample, while the shot noise is "only" proportionat toJF).

Because of the limited spectral radiant intensity of incandescent lamps, it is hardly possible to resolve reactions in the sub-microsecond range in photosynthetic samples from plants.

Much higher spectral intensities of the measuring light are now available from laser sources. As photomultipliers support only weak light, one has to use a photodiode coupled to an electronic amplifìer as detection system, which introduces additional (thermal) noise. This disadvantage is, however, largely overcompensated by the gain in signal amplitude due to the higher radiant power. Thus, it became possible to monitor some reactions in plant photosynthesis with a time resolution close to 1 ns (see section 4.5).

Evidently, AA can be increased by increasing the concentration c of the sample or the optical path l(see Eq. l). However, for agiven measuring light source, an increase of c or I decreases the radiant power P arriving at the detector, so that the signal-to-noise ratio would decrease when the transmission of the sample becomes too low. In fact, there exists an optimum for the product c'l with respect to the signal-to-noise ratio. Fø the simplest case, when the shot noise is the only noise source, it has been shown [5] that the best signal-to-noise ratio is obtained when c'l is chosen such that the transmission of the sample is approx. L4Yo at the wavelength of the measuring light (trace a in Fig. 2). The general case, that all three noise sources mentioned above contribute, has also been analysed ([6], see Fig. 2 for examples) leading to the following conclusions. When the thermal noise of the detection system becomes dominating (trace b), the optimum shifts to a higher transmission (i.e. a less concentrated sample or a shorter optical path) rvVhen, however, The following assumptions about the noise sources were made: Trace a: shot noise is the only noise source. Trace b: thermal noise of the detection system contributes in addition to the shot noise; the ratio of thermal noise to shot noise isJ2 .l at T = 0.14.

Trace c: fluctuations of the radiant power of the measuring light source contribute in addition to the shot noise, the ratio of these fluctuations to the shot noise is Jã: I at T : 0.14. Trace d: all three noise sources contribute equally at T = 0.14. the optimum occurs at a transmission below l4%. Whenever the signal-to-noise ratio is critical for a flash absorption experiment, it is worthwhile to check for the optimal concentration and optical path of the sample.

Actinic effect of the meaxring light

The measuring light can have the undesirable effect of inducing the (photo)reaction to be studied already prior to the actinic flash This effect can be diminished (at the expense of the signal to noise ratio) by decreasing the intensity of the measuring light. Another possibility is to switch on the measuring light only very shortly before the actinic flash. Sometimes the reaction can be studied at a wavelength, where only/the product(s) absorb, but not the dark adapted state of the sample. In this case, even high intensities of the measuring light do not disturb the experiment.

Fhtorescence arteþct

Similarly to scattered light (see section 3), flash induced fluorescence reaching the photodetector would pretend a transient bleaching of the sample. If fluorescence occurs at the wavelength of the measuring light, it can not be blocked by optical filters. In this case, it can be helpful to increase the distance between sample and detector and to place a small diapkagm in front of the detector. This decreases the fraction of the fluorescence which is "seen" by the detector because the fluorescence of the sample is emitted in all directions in space. In addition, one may record the fluorescence artefact separately (in the absence of the measuring light) and subtract it from the signal recorded in the presence of the measuring light. 4.5. Examples of set-ups with sttb-microsecond time-resolution . The photoreactions of the chlorophyll-a type primary electron donors of photosystem I (P700) and photosystem II e680) can be studied conveniently with a set-up using a laser diode emitting at 820 nm as the measuring light source and a fast (and small) photodiode as detector. As the chlorophyll-a cation absorbs at around 820 nm, but neutral chlorophyll a does not, photooxidation of P700 or P680 is accompanied by an absorption increase at 820 nm. High measuring light intensities can be used without actinic effect on the sample, because the absorbance at 820 nm of the photosynthetic apparatus is virtually zero in the dark adapted state (prior to the actinic flash). Furthermore, provided that the sample is optically clear, high concentrations of the sample and a long optical path I can be used without decreasing the radiant power P reaching the detector. As another advantage, the laser light can be readily focused on a small photodiode at a large distance from the sample, thus decreasing the fluorescence artefact. Such a set-up was introduced by van Best and Mathis [7] to study the rereduction kinetics of P680.. With some more recent technicalimprovements, it is now possible to study P680. [8-10] and P700. I l, l2] with a time resolution close to I ns. . To monitor the photoreactions of P680 in the red-most absorption band of its neutral form (around 680 nm; this band is bleached upon photooxidation of P680), a tuneable dye laser (pumped by an Ar ion laser) was used as measuring light source. The fluorescence artefact, which is very strong around 680 nm in a standard set-up, could be largely reduced by using a small photodiode at a large distance (approx. 2 m) from the f sample. The measuring light was pulsed by means of an electro-optical modulator in order to diminish the actinic effect [13, 14,9]. More recently, red laser diodes (which are rather cheap) were used as measuring light sources [0].

. To study absorption changes in the [fV and blue spectral regions with a time resolution of a few nanoseconds, a pulsed measuring light of high radiant power was realised using a Xe flash lamp emitting flashes of approx. 50 ¡rs duration. The top of the flash is suffìciently flai to be used as a quasi continuous measuring light during approx. I ps. Such a set-up was applied successfully to monitor the oxidation of the immediate electron donor to P680. (which turned out to be a tyrosine) [5, l6], and electron transfer through the secondary electron acceptor A1 (phylloquinpne) in¿photosystem I 117-re1.

  Io/ofor IAP/PI <0.01 andapprox.5Yofor IAP/PI = o.l.

Fig. 2 .

 2 Fig.2. Dependence of the signal-to-noise ratio on the transmission T of the sample. Different T values represent different optical paths I or different concentrations c of the same sample. The following assumptions about the noise sources were made: Trace a: shot noise is the only noise source. Trace b: thermal noise of the detection system contributes in

  See text and Ref.[6] for further details. Redrawn fromRef. [6]. radiant power of the measuring light source are dominating (trace c),


Daniele Funaro
email: daniele.funaro@unimore.it

Spacetime deformations of electromagnetic nature are far from negligible

We would like to collect a series of considerations concerning the influence, which we believe is relevant, that phenomena of an electromagnetic nature have on the geometry of spacetime. The approach, supported by the critical observation of already wellknown properties and sustained by theoretical elements, leads us to attribute a primary role to electric and magnetic interactions. In fact, a seemingly small interpretative effort can help link theories elegantly and mathematically which at the moment appear independent. Einstein's equations have a validity that goes beyond the cosmological one and, with the appropriate corrections, they can clarify what really happens inside matter, starting with the bonds that dominate at the molecular level all the way up the description of the macroscopic characteristics. This analysis allows us to leave the context hitherto reserved exclusively for quantum mechanics and to place the study of the structure of matter in a more classic framework.

Like any other form of energy, electromagnetic radiation is capable of warping spacetime geometry. From a purely mathematical viewpoint, this is obtained by placing to the righthand side of Einstein's equations an appropriate forcing term related to the electromagnetic stress tensor. Rainich's pioneering article [START_REF] Rainich | Electrodynamics in general relativity[END_REF], and the subsequent paper by Witten [START_REF] Witten | Geometry of gravitation and electromagnetism[END_REF] show how formal solutions can be derived from this type of approach. The results have been taken up and improved on some crucial issues ( [START_REF] Funaro | Electromagnetism and the Structure of Matter[END_REF], sections 4.5, 5.1; [START_REF] Funaro | From Photons to Atoms, The Electromagnetic Nature of Matter[END_REF], appendix E) that we do not intend to discuss here in order not to make the exposition too technical. Unfortunately, the interest in this branch of general relativity has never attracted great interest, above all because the phenomenon of curvature variation associated with electromagnetic waves has never been considered quantitatively relevant. The theory was born in the gravitational and cosmological context and has always had applications in these fields as its main focus.

However, as soon as you enter an atomic structure, where electric and magnetic forces are dominant, the gravitational contribution can become far from negligible. It is evident that here the term "gravitational" should not be correlated with the presence of significant masses in the way we commonly refer to. Although used incorrectly, the adjective testifies to the presence of nontrivial geometric deformations. Results and considerations in this direction have been brought to light in recent publications [START_REF] Sabín | Phonon creation by gravitational waves[END_REF][START_REF] Nicolis | Mutual interactions of phonons, rotons, and gravity[END_REF][START_REF] Kornreich | Light induced gravity phonons[END_REF][START_REF] Esposito | Gravitational mass carried by sound waves[END_REF]]. As will be better specified later on, electromagnetic-type phenomena evolve following specific geodesics "carved" in the inter-atomic lattice. Practical details are available in the preprints [START_REF] Funaro | The impact of a pervasive electrodynamical background on biological interactions[END_REF][START_REF] Funaro | Newtonian forces exerted by electromagnetic waves traveling into matter[END_REF], in part well formalized and in part only sketched out in a heuristic way. We will, however, remain in this Essay in a predominantly descriptive area.

When we talk about the laws of gravitation, it is important to note that the concept of mass is linked to objects which, however small they may be, are nonetheless made up of a gigantic number of atoms. This means that in the classic gravitational context, the way matter is made does not come into play in the specification of the laws, implicitly treating the masses as volume integrals of a homogeneous density of mass. However, we know that this is not correct, as the actual mass is concentrated in the atomic nuclei, which occupy a much smaller portion of space than the entire atom. This disproportion radically changes the points of view, considering that an atom has an average diameter of the order of 10 -10 meters, while the nucleus has an average diameter of the order of 10 -15 meters. The ratio in terms of volume becomes 10 15 . Certainly not a trivial amount! In truth, the singular masses involved are extremely small and it is the enormous quantity of particles that generates the global mass. But it is also true that between one nucleus and the next the gravitational force density is decidedly negligible so that the volume integral is the result of a sum of an overwhelming number of peaks concentrated almost punctually.

If instead we focus on quantities of an electromagnetic nature, things change. The intensity of the fields between one nucleus and another is very large, to the point of having, for example, magnetic fields of the order of Teslas. The stability of matter (which is actually almost devoid of "real" matter) is the consequence of considerable energies which, compared to almost zero average, retain strong chemical bonds. According to this interpretation, "solid" objects appear as a mixture of physical particles and energy in constant evolution. In this regard, we specify that the vacuum, whether internal or external to matter, is not actually "empty" but it is comparable to an electromagnetic background that permeates everything (see, e.g.: [START_REF] Milonni | The Quantum Vacuum: An Introduction to Quantum Electrodynamics[END_REF][START_REF] Meis | Light and Vacuum[END_REF]). This brings Einstein's equations back into play, and it is obvious that in the new context the constants involved will have to be rethought, and this will also depend on the type of material with which we are dealing. In a revised interpretation of the equations of general relativity the constants that multiply the right-forcing term will be much larger. We can even be more courageous and advance the guess that the intense spacetime deformations that take place inside the electromagnetic background, can also model with the same constants the phenomena classified up to now as essentially gravitational in nature. In fact, the very weak gravitational attraction between two large masses could be the result of more intense electromagnetic forces between the innumerable particles that make up the two bodies, whose nonlinear interactions cancel each other out, providing a result that is not null but definitely smaller. This would be an elegant way to address the chapter concerning the unification of gravitational and electromagnetic forces, about which we would not venture to say any more.

At this point it is necessary to mention some experimental evidence to what has been stated above, namely that geometric changes take place inside matter which are not trivial at all. These deformations are not due to the presence of elementary particles as massive elements, but to an energy density which lives inside the material bodies and which is distributed over their entire volume. We claim that the tireless electromagnetic agitation of the vacuum is adapted by the presence of the atoms which display a non-stationary activity inside them, strongly dependent on the type of nuclei. When we were still talking about aether, many supporters believed that it was not at rest (in a reference system integral with the fixed stars), but that it was constantly evolving, being able to adapt dynamically by fluctuating ceaselessly among the atoms [START_REF] See | New theory of aether[END_REF]. Nowadays, there is no longer any need to suppose the existence of the aether; however, electromagnetic radiation and its associated geometry remain. The two interpenetrate each other, acting on each other and evolving like a fluid, which, although it does not contain masses, behaves as if some mass density really existed. As also underlined in [START_REF] Funaro | From Photons to Atoms, The Electromagnetic Nature of Matter[END_REF][START_REF] Funaro | The impact of a pervasive electrodynamical background on biological interactions[END_REF], matter could be defined as the indissoluble union of small units of mass and charge that determine the scaffolding, plus something that could be given the name of pseudo-matter. Pseudo-matter cannot be isolated. It is mass density without a container. It is spread and takes both positive and negative values, the contribution of which, integrated in physical space and time, provides a null resultant. To say that pseudo-matter can somehow be assimilated to dark matter is perhaps a bit far-fetched, but we believe that the family it belongs to is the same, as we will analyze below.

It is not necessary to choose sophisticated examples to defend the hypothesis of the existence of strong curvatures within matter. The case of diffraction is emblematic. From abstract rules of geometrical optics, mostly based on phenomenological descriptions, we move on to a relativistic interpretation, where the deviation of light is due to the presence of pre-existing geodesics. The phenomenon is nonlinear and back-reacting, i.e. the very passage of photons inside matter contributes to the variation of the geometry. We specify once again that there are no specific masses or black holes to bend the trajectories of the rays. The effect is instead due to the geometry induced by the pseudo-matter, which in turn originates from the presence of atomic nuclei and at the same time helps to keep them together. With these assumptions, even deterministic explanations are starting to come to life in a context hitherto relegated to quantum phenomena. In the double-slit experiment, the background radiation, due to the presence of closely spaced holes, assumes a conformation that already prefigures the existence of interference fringes. Particles (materials or photons) only show predetermined paths. Their dynamic behavior depends on how the geodesic system is approached. It is therefore not the interaction between particles (which in some experiments are only sent one at a time to the device) that produces wave interference, but the control that is carried out on them by the modified geometry around the peculiar electromagnetic framework surrounding the two slits (see figure 3.18 in [START_REF] Funaro | From Photons to Atoms, The Electromagnetic Nature of Matter[END_REF]). This also explains why the observation of the phenomenon by masking (even partially) one of the slits disturbs the whole experiment. The act of "observing" has not influence on the single particle, but on the whole apparatus in such a way to reconfigure the preexisting interference fringes. The presence or absence of the particles is irrelevant. We realize we have taken a rather slippery path so we stop here with this topic and we refer to [START_REF] Funaro | From Photons to Atoms, The Electromagnetic Nature of Matter[END_REF] for more explanations.

The existence of electromagnetic waves (possibly mixed with particles to form a plasma) trapped by their own self-generated geodesics, may explain the ball-lightning phenomenon (see, e.g. [START_REF] Stenhoff | Ball Lightning: An Unsolved Problem in Atmospheric Physics[END_REF][START_REF] Shmatov | Advances in ball lightning research[END_REF]). The natural shape for this type of structures is the toroid, which dynamically behaves like a fluid dynamic vortex ring [START_REF] Funaro | Ball lightning as plasma vortexes: a reinforcement of the conjecture[END_REF]. If it is therefore true that electromagnetism acts on geometry in such a marked way, one can think that the action can be extended to phenomena of a classically gravitational type, such as the motion of the planets around our Sun. Magneto-hydrodynamics (see, e.g. [17,[START_REF] Davidson | An Introduction to Magnetohydrodynamics[END_REF]) studies the evolution of plasma at both the solar system and cosmological levels. A geometry altered by the presence of masses and combined with that coming from electromagnetic radiation provides new vistas. In [START_REF] Fatone | Electromagnetic fields simulating a rotating sphere and its exterior with implications to the modeling of the Heliosphere[END_REF], it is hypothesized that the Sun can impose its presence through three types of phenomena: the emission of photons, the solar wind, the generation of encapsulated and geometrically growing electromagnetic structures. Precise construction details based on the resolution of Maxwell's equations are provided for the latter. If the effect has some weight on the evolution of the planets, it would not be difficult to explain the coplanarity of their orbits and the geometric growth of their distances from the Sun (Titius-Bode law).

It's time to introduce the model equations and we will do it as concisely as possible due to lack of space. However, all explanations are accessible in [START_REF] Funaro | From Photons to Atoms, The Electromagnetic Nature of Matter[END_REF]. It should first be observed that the electromagnetic background contains regions where the divergence ρ of the electric field is non-zero at points where there may be no charges. This statement may seem very unconventional, but sooner or later becomes necessary to face the issue if we want to fully understand the dynamics of electromagnetic phenomena. To introduce the problem, the most basic example is that of a charged capacitor with parallel plates of infinite size. The charge or the distance of the plates is then altered in a uniform manner, always maintaining parallelism so as not to develop magnetic fields. Since information travels at a finite speed (that of light) it is inevitable that momentary zones are created between the plates with ρ = 0 which compensate each other between positive and negative values, so that Gauss's theorem still applies to the whole system. A full discussion of this problem is available [START_REF] Funaro | Charging capacitors according to Maxwell's equations: Impossible[END_REF].

Thus, the non-stationary electromagnetic vacuum also contains a pseudo-charge, which does not correspond to the presence of physical charges. On the other hand, in subatomic physics it is convenient to define virtual pairs of particles and anti-particles, in our opinion precisely to meet the need to give meaning to the presence of charge density without charge.

We denote by E the electric field, by B the magnetic one, and by V a velocity vector field. In particular, V indicates the evolution of the electromagnetic information, which, as said, is not necessarily carried by real massive bodies like charged particles. The set of model equations in Minkowski space, coupling Maxwell's equations and Euler's equation for non viscous fluids, reads as follows:

∂ E ∂t = c 2 curl B -ρ V ∂ B ∂t = -curl E div B = 0 (1) ρ µ -1 D V Dt + ( E + V × B) = --1 0 ∇p (2)
with ρ = div E; c is the speed of light and 0 the vacuum permittivity constant. The setting is not dissimilar from those analyzed within the framework of plasma physics or magneto-hydrodynamics. The nontrivial exception is that we do not introduce any mass density here. The scalar p is a potential denoting pressure density per unit of surface, which, differently from fluid dynamics, can also attain negative values. It represents the link between electromagnetic and Newtonian-type forces. The term E + V × B recalls Lorentz's force.

Finally, the constant µ is dimensionally equivalent to Coulomb/Kg. The set of equations extends the classical Maxwell's model in vacuum (just impose ρ = 0).

The equations can be derived through an energy tensor, which, in addition to including the well-known electromagnetic stress, incorporates a mass tensor resembling that of a dust of particles for a perfect fluid (remember, no mass density though!). The same energy tensor is the one to plug on the right-hand side of Einstein's equation. Among the extraordinary properties of this system of equations there is the possibility of constructing explicit solutions of (1)-( 2) which, despite being of the classical type, reflect all the prerogatives of photons, i.e. they travel without dispersion along straight lines at the speed of light; they behave like particles and electromagnetic waves at the same time; they respect the rules of geometrical optics. Although the theme has now become out of fashion, the result answers the ageold question of attributing a clear definition to the notion of wave-particle. Furthermore, associated with these waves, exact solutions of Einstein's equation are computable. It is also surprising to note that to construct the photon-waves it is necessary to hypothesize that inside them ρ = 0; nevertheless, in the metric generated by their passage we find the condition ρ = 0, thus rediscovering the standard Maxwell's equations in vacuum. All of this material is well documented and available in [START_REF] Funaro | Electromagnetism and the Structure of Matter[END_REF][START_REF] Funaro | From Photons to Atoms, The Electromagnetic Nature of Matter[END_REF]. We would like to dwell on the exposition but this is not possible in order to remain within the limits of this Essay.

From these reasoning it follows that the actual matter is immersed in an electromagnetic soup which already contains the essence of the matter itself, and the laws that regulate its dynamics are the embryo of those that will become known laws in the presence of matter.

In this primordial universe, the only law that is not established a priori is that of Coulomb, which will automatically derive from the basic model once elementary particles are introduced. There is no precise metric that describes this universe (bad news for cosmologists!), presenting itself as a predominantly calm ocean, but full of constantly evolving substructures at various scales of magnitude, which can be created or annihilated depending on the circumstances. The structures develop approximately respecting the basic rule that the frequencies of the vortexes involved are inversely proportional to their dimensions.

Arrived at this point the reader, alongside the considerations made above which some may consider fanciful, will wish to know innovative extensions. A very recent experiment still awaiting replication would not only validate the above, but would pave the way for revolutionary applications. The recipe is to put pseudo-matter into rotation inside an asymmetrical cavity. In the specific case it is a dielectric ring with an appropriate design. The ring is stressed through a conductive winding to which a radio-frequency signal is applied.

Via a high voltage power supply, a stationary electric field is also added. For an appropriate choice of the input frequency, internal Newtonian forces with non-zero average resultant begin to press on the entire apparatus, exerting a side thrust in violation of the action-reaction principle. The thrust is orders of magnitude greater than expected, somehow confirming that the constants involved need to be revisited. The laboratory test is documented in [START_REF] Funaro | An efficient ring-shaped electromagnetic thruster[END_REF], and some partial explanations in relativistic terms are provided in [START_REF] Funaro | Newtonian forces exerted by electromagnetic waves traveling into matter[END_REF], where Einstein's equations are exactly solved in simplified situations. Hopefully, future numerical approximations will provide more details. We remind that pseudo-mass and pseudo-charge are not relativistic invariants. This means that the reaction of the vacuum can be different depending on how we stress it, and therefore that we can exploit this property to our advantage (any relation to the Unruh effect [START_REF] Fulling | Nonuniqueness of canonical field quantization in Riemannian space-time[END_REF]? Or to the work of Woodward on capacitors [START_REF] Woodward | A new experimental approach to Mach's principle and relativistic graviation[END_REF]?). The distortion that the pseudo-matter in asymmetrical rotation brings to the molecular lattice is momentary. The possibility of "deceiving" the classical conservation principles may be based on the recovery delay of the initial molecular configurations and the repetition of the impulses at a rate of billions times per second. The ring is about ten centimeters in size and the information travels at speeds comparable to that of light. There are margins for hypothesizing that the "reaction" does not occur instantaneously but that there is room for a new "action", thus circumventing fundamental theories. The importance of this discovery is primary, for example, in the construction of the so-called "EM-thrusters" in the space sector.

The moral of this article, which deliberately does not report theoretical mathematical passages, is that with common sense and a necessary correction of the gravitational constant in the case of electromagnetic fields, a sequence of practicable paths is obtained aimed at answering ancient questions without the need to introduce a "new physics". The revision requires a wide-ranging intervention that cannot be carried out by a single individual, and touches on many crucial aspects underlying theories that are considered already consolidated.

However, we believe that an effort must be made in the directions indicated, in order to acquire a unified and deeper understanding of the matter that surrounds us.