Constants and variables in first-order logic

[Russell Wallace]

Consider traditional first-order logic. More specifically, consider
clause normal form, with the usual motive of using it for automatic
theorem proving, where the objective is to prove a given set of
clauses is unsatisfiable.

Clauses are written with a combination of named constants and
variables (and optionally literals, e.g. numbers). I'll use Prolog
notation where lower case letters denote constants and uppercase
letters denote variables.

What exactly is the semantic difference between constants and variables?

Intuitively, the answer would seem to be that constants are, well,
constant, whereas variables are variable; this would seem to be the
justification for the usual procedure where we can only substitute for
variables.

But only some constants are really constant in the sense of having
known values. We can write as many constants as we like, and the
values of the extra ones will start off being unknown. We can then say
that a set of clauses is satisfiable if there is some set of values
that can be assigned to the constants and variables that will make
every clause return the value true.

For example, in TPTP format, $sum is defined to be the addition
function, so that $sum(X, Y) always means X+Y. But we can also write
f(X, Y), where f is a symbol we just introduced, the name of some
unknown function.

Constants can represent functions of one or more arguments, whereas
variables can only represent values. But a function of zero arguments
is the same as a value. If we write the constant x, it could have any
value, just as if we write the variable X.

Constants can be of type boolean as well as object, whereas variables
can only be of type object. Also, a given constant can occur in more
than one clause, whereas a given variable can only occur within a
clause.

In short, it would seem that constants are a strict superset of
variables in their capabilities. What would happen if we abolished
variables, and allowed substitution of constants? Would the resulting
system still be sound and complete?

In other words, is it the case that variables in first-order logic (at
least clause normal form - quantified variables are another matter)
are just an optimization hint, a way of telling a prover "you only
need to bother trying to substitute these variables, the constants are
really variables as well, but you don't need to spend time
substituting them"?

The reason I ask is that I'm working on doing higher-order logic with
combinators, in which scenario in a sense there aren't any variables;
or, it seems to me, in another sense variables and constants are the
same thing; I'm wondering if I'm missing anything fundamental.

[Russell Wallace]

Lukasz observes that in full first-order logic, constants are
existentially quantified whereas free variables are universally
quantified, so that e.g. X=0 is not a true statement.

However, if we focus specifically on clause normal form and the
question of satisfiability, everything is existentially quantified, so
x=0 and X=0 both have the same meaning and status: satisfiable.

Full first-order logic has quantifiers, which bind variables.

Lambda calculus also has quantifiers, which bind variables. Indeed,
when you go to higher-order logic, it becomes clear that quantified
statements are really just statements about the equivalent lambda
functions.

I've been chewing for quite some time now on the problem of reducing
lambda calculus to combinator logic for purposes of higher-order
theorem proving, based on the gut feeling that the simplification of
doing away with bound variables is a huge win.

It now seems to me we can say that this process would be _the same as_
the process in first-order logic of reduction to clause normal form:
get rid of bound variables, make everything existential, then focus
purely on the question of satisfiability; and when you do that, the
difference between constants and variables disappears.

Reduction to clause normal form has been an enormous boost to progress
in automated first-order theorem proving, roughly speaking, because by
flattening everything to a uniform representation, it lets the
automated systems run full throttle.

If the above considerations are true, they suggest reduction to
combinators may have the potential to be a similar boost to progress
in automated higher-order theorem proving for similar reasons.

[Abram Demski]

Russell,

Not sure if this will turn out to be relevant, but I'm going to try to spell out some things which have been going through my head.

In December, I was mulling over the problem of "transfer learning" for a system which initially ran on 1sr-order logic and started to learn 2nd-order logic (a scenario I find not-too-implausible). The issue is that if the system learned 2nd-order logic, it would be unable to learn a general schema for applying 2nd-order logic to its existing nth-order knowledge. (A similar concern, of course, is supposed to arise when learning further extensions to the logic.) Let's call this the "transfer principle": if a logical system (probabilistically) accepts that a more powerful logical system is correct, it should be able to apply that logic to its existing knowledge.

My solution was to require that the logic be syntactically self-available; so, for example, we might take the old idea that constants and variables are differentiated by adding a "prime" to them, so that all our constants are c, c', c'', c'''... and all our variables are v, v', v'', v'''... Then, we let the "prime" function be available to the system. The same must be done for predicates, functions, etc. Call this the "self-transparency principle".

I think the reason that this worked was actually irrelevant to the idea: my formalism snuck enough 2nd-order logic in to give it some of 2nd-order logic's power. What I didn't realise at the time is that, although 1st-order logic does not obey the transfer principle, 2nd-order logic (w/o 3rd-order constant*) has better properties in this respect. It at least follows an "order transfer principle": if a 2nd-order system is learning nth-order logic (for finite or ordinal n up to some high ordinal), it can also learn a schema to transfer all its knowledge into the new form (or, apply the new logic to the old knowledge).

*[What I mean by the parenthetical phrase: the syntax which results from adding just 2nd-order quantifiers to 1st-order logic, *not* the theory which also adds predicates on predicates.]

So, back to self-transparency. One feature it gives a logic the ability to "fill up" its universe-- a finite set of statements may imply something about every single constant name, so that we can no longer pull out a fresh, unused  constant when we need to. Furthermore, if the exact name of a variable is accessible at any time, it seems that substitution of variables would be broken anyway. In such a system, it seems like taking your suggestion would be quite justified.

Of course, the question is how a system with no variables should look, and whether this really gives any benefit.

--Abram

--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

--
Abram Demski
http://lo-tho.blogspot.com/
http://groups.google.com/group/one-logic

[Abram Demski]

However, if we focus specifically on clause normal form and the
question of satisfiability, everything is existentially quantified, so
x=0 and X=0 both have the same meaning and status: satisfiable.

But doesn't X=0 have the additional implication that everything is 0, so that it becomes unsatisfiable if something not equal to 0 is added?

--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

[Russell Wallace]

Right. I don't know where that leads yet, but as I remarked a while
ago, it does seem that some kind of 'quote' special form will be
needed - special form because it's an exception to the substitution
rule, i.e. just because x=y does _not_ mean q(x) can be substituted
for q(y).

[Russell Wallace]

On Sat, Jan 29, 2011 at 3:25 AM, Abram Demski <abram...@gmail.com> wrote:
>> However, if we focus specifically on clause normal form and the
>> question of satisfiability, everything is existentially quantified, so
>> x=0 and X=0 both have the same meaning and status: satisfiable.
>
> But doesn't X=0 have the additional implication that everything is 0, so
> that it becomes unsatisfiable if something not equal to 0 is added?

In the typical interpretation of first-order logic, yes, but not in
clause normal form where the question is of satisfiability. If you
feed X=0 into a first-order theorem prover, it will give the result
Satisfiable.

[Abram Demski]

But what if you feed in a larger set of which X=0 is a part, such as X=0 and y=12? Then doesn't variable/constant make a difference?

--Abram

--

You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

[Russell Wallace]

If you feed 'X=0 & y=12' into a first-order theorem prover, it will
give the result Satisfiable because there exist values for X and y
that will make the statement true. Am I misunderstanding what you
mean?

[Russell Wallace]

Mind you, it's indeed not cut and dried, I tried feeding the following
into E (one of the best first-order theorem provers currently
available):

cnf(1, plain, X=0).

And it gave the result Satisfiable.

But:

cnf(1, plain, X!=0).

gives the result Unsatisfiable, which would appear to be inconsistent.

But do we need to worry about that for higher-order logic? We are
entitled to wrap every free variable in the input in a universal
quantifier, which translates into a lambda expression, which
translates into combinators with no variables.

A caveat is that we still need to reintroduce free variables for
certain purposes, e.g. to prove SKK=I it is necessary to feed them
both the same variable and observe they then reduce to the same
result.

In that case, are we effectively using variables with implicitly
universally quantified semantics? In a sense we are using them for
that purpose, but it doesn't seem to me we are doing so in such a way
as to make it necessary to introduce such semantics as a primitive.

[Abram Demski]

I suppose what's vague here is really just the concept of "removing variables". :) It's more fruitful to discuss a specific system than the general idea.

So, as we've discussed before, universal statements would be represented by functions which yield more specific statements when fed arguments? The advantage of this would, I presume, be easily keeping track of instantiations (ie, instantiation is just feeding an argument and reducing to normal form). The disadvantages I can think of:

1) For statements which have several variables universally quantified, we would need to use special argument-shifting combinators to instantiate different variables.

2) We can't unify general statements with specific ones directly by form, since the universal statements will be "folded up" so to speak... we need to feed arguments to them arguments to unify. This is probably something we would need to do sometimes anyway, when unifying functions.

Can you think of any more pros/cons or specific aspects of the system that are still fuzzy?

--Abram

--

You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

[Russell Wallace]

I got word back from the author of E which resolves my confusion about
the first-order case. Turns out unsatisfiable is indeed the correct
answer for X!=0. So does the other answer for X=0 represent a bug in
E? Apparently not...

... it was merely using a model in which 0 is the only number.

(If your jaw didn't just hit the floor, I guess that means you're a
real mathematician :-))

[Russell Wallace]

Basically yes. Universal and existential statements get translated into lambda:

![X]: p(X) translates to ^[X]: p(X) = ^(X): true
?[X]: p(X) translates to ^[X]: p(X) != ^(X): false

If we then translate to combinators, we get rid of variable binding,
which has the huge advantage that terms become context free; the
meaning of a sub term does not depend on the larger term in which it
was embedded. (caveat: I'm not yet as sure as I'd like to be that this
remains true after we bring types into the picture.)

One disadvantage of translating to CL is that it becomes a bit more
difficult to determine when terms are equal. There are also the
practical difficulties of debugging output by eyeball and trying to
not get term size to blow up too much.

I don't have the algorithms nailed down yet, but as far as I can see,
regardless of whether we translate to CL, we will need to shift things
around, feed arguments etc. in order to do inference, as you say.