Equality from the Constructive Point of View

Valeri Plisko & Dmitri Viter

We consider equality in the framework of the constructive model theory developed in [1]. Let (M, ν) be an enumerated set. A constructive equality structure compatible with (M, ν) is a function E : N^{2} → 2^{N} such that E(m, n) ≠ ∅ ⇔ ν(m) = ν(n). The elements of E(m, n) are treated as the realizations (in the Kleene sense) of the sentence m = n. The set of realizations of a sentence in the language with the only predicate symbol = is defined in accordance with Kleene’s recursive realizability. The theory of a constructive equality structure is defined as the set of all sentences whose set of realizations is not empty.

In the classical logic, the equality theory of a set M depends only of the cardinality of M. In the constructive case the situation is rather different.

An equality structure is said to be normal if the sentence ∀x(x = x) is realizable. It is proved that all normal constructive equality structures compatible with a given enumerated set have the same theory.

The next step is extracting structures with decidable equality, i. e. equality structures where the sentence ∀x∀y(x = y ∨ ¬x = y) is realizable. It is proved that the theory of a normal constructive equality structure with decidable equality compatible with a given enumerated set (M, ν) is just the classical equality theory of M.

There are different constructive equality theories with undecidable equality even in the case of a 2-element enumerated set.

The first author is partially supported by RFBR grant 98-01-00249.

[1] V. Plisko. On languages with constructive logical connectives. Dokl Akad. Nauk SSSR 296 (1987), pp. 35-38

Address: Department of Mathematical Logic and Theory of Algorithms, Faculty of Mechanics and Mathematics, Moscow State University, Moscow, 119899, Russia

E-mail: plisko@ttk.ru, plisko@lpcs.math.msu.ru