Axiomatisation

• Theorem 1. H_w should read H_c.
• Theorem 2 is refuted by a one-point total algebra with a unary operation S and a constant c. A⊨^∗ Sx ≈ c. Consider now the assignment v: x ↦ ∗. This is an assignment on A^∗. By definition, S^∗∗ ≈ ∗; and c ≉ ∗. So, A^∗ ⊭Sx ≈ c. This following seems to be a correct statement: s ≈ t is in the strong theory of A iff A^∗ ⊨ x₀ ≈ ∗ ∨ ... ∨ x_k-1≈ ∗ ∨ (s ≈ ∗ ∧ t ≈ ∗) ∨ s ≈ t where x_o through x_k-1 are the variables that occur only in one of s or t.
• Theorem 3. Burmeister's counterexample does not seem to be pertinent, it concerns partial many sorted algebras, not total ones.
• Theorem 10. This theorem is false. Here is a characterisation of typable algebras. Let A be a partial algebra. Say that a ≺_A b if either a is an argument of c (in other words: ca is defined) or a is a value of c (in other words: there is b such that a ≈ cb). Second, say that a polynomial function is definite on A if it has the form pq where either p is definite or q is not constant on A. (Thus, xy is definite since y is not constant, but xa is not definite where a is constant.) Now the correct version is this. Let Ω_A denote the congruence relation such that a ≅ c (Ω_A) iff whenever p is a polynomial then p(a) is defined whenever p(c) is.

  THEOREM. A partial algebra (A, ∘) is typable iff

  1. for all a, c from A, if there exists a definite polynomial p such that both p(a) and p(c) are defined then a and c are congruent modulo Ω_A; and
  2. ≺_A is well-founded.

  ---

  Marcus Kracht
  Last changed: Wed February 11, 2009 22:30:00