Formal Generalization Problem

Previous version was with an error, I post corrected version.

This article describes Formal Generalization Problem, a yet open mathematical problem. (This problem is probably simple but I formulated it just recently, so I have not yet succeed to 100% solve it, or maybe it is not an open problem and somebody has already solved a similar problem?)

Whether this problem is interesting by itself or not, it is important for certain revolutionary mathematical logic research (about a new definitional method replacing axiomatic method), and indirectly it is also important for General Topology.

I will reward anyone who will solve or significally help to solve it with links from my mathematical site.

This article is a more concrete formulation of a problem described in this message.

Terminology

A formula is a pair of a symbol and (recursively) a finite sequence of zero or more formulas. The formulas must be finite. The above mentioned finite sequence is called arguments of a formula.

(It does not matter what symbols are, these may be e.g. natural numbers.)

An example of a formula: p(s() d(u() u(e()))), where p, s, u, e are symbols.

By definition subformulas of a formula are:

• this formula itself;
• (recursively) the subformulas of the arguments of this formula.

For example, for above mentioned formula, the subformulas are:
p(s() d(u() u(e()))), s(), d(u() u(e())), u(), u(e()), e().

A specialization function is a function f on the set of all formulas such that f(A(B1...Bn)) = A(f(B1)...f(Bn) C1...Cm), where C1, ..., Cm are some formulas, for any formula A(B1...Bn).

That is, informally, a specialization function adds additional arguments to the symbols in formulas.

By definition the set A(...) of specializations of a formula A is:
A(...) = {f(A) | f is a specialization function}.

By definition if A, B, C are formulas and C in A(...), then (A-top->B)(C) = f(B), where f is such specialization function that f(A) = C and f(X) = X if the fomulas X and of A have no common subformulas X is not a subformula of A.

(It is simple to prove that there exist exactly one such f.)

Example: (x()-top->a(x() x())) (x(z())) = a(x(z()) x(z())).

Preformal Generalization

I will call a preformal generalization (This is a temporarily introduced math term, which may pass away, after we will solve the problem.) a pair of formulas (A,B) such that B in A(...).

The problem to solve: Find the condition required to warrant that:
C in ((A-top->B)(C))(...) for any C in A(...),
where (A,B) is a preformal generalization (that is B in A(...)).

We need to find a simple concise formulation of the condition. I'd like if we will find a condition which is both required and necessary, but a condition which is only required would be also an advance.

A more formal formulation of the problem: find an algorithm allowing (knowing A and B) to check whether
C in ((A-top->B)(C))(...) for all C in A(...).
Does this algorithm exists at all? If not what are the cases when it exists?

Please email the solutions to me. I will reward the first who will solve it or provide any significant help in solving it by a weblink from this site with the description and thanks what you've done.

See also this USENET message and followups.

---

Victor Porton, see also my math site.
Copyright © 2005 Victor Porton. You must refer to this URL if you copy this text. You are allowed to copy and modify it, with only restriction that you don't misrepresent the authorship.