Re: Universal grammar

In article <87bqo27ygx.fsf@xxxxxx>, Markus Triska <triska@xxxxxx> wrote:

In a Prolog *program*, the fact:

thing(X).

translates to: Everything is a thing. (For all X, thing(X) holds.)
Also consider:

natnum(0).
natnum(s(X)) :-
natnum(X).

The second clause is read: *FOR ALL* X it holds that natnum(X) implies
natnum(s(X)). Clearly, free variables are all-quantified in clauses.

In Prolog *queries*, free variables are *also* all-quantified
intitially, and the query is negated to search for a refutation.

Strictly speaking, in quantification theory, these are free variables
without quantifications. There is also a symbol "all" used to bind
variables, like in
  all x A(x)
where A(x) is a predicate. These are combined with axioms (medelson, p.57):
  (K4)   all x A(x) => A(t) if t is a term free for x in A.
  (Gen)  A |- all x A(x).  (Generalization)
The symbol "exist" can also be mixed into this bag.

I am glossing over some of the details. But these formally correct axioms
are quite complicated, expressing how variables are bound and freed. With
them in hand, one can express infinities.

Common Prolog interpretations often mix up the symbols "=>", implication
of the object theory, and "|-", provability in the metatheory.

--
Hans Aberg
.