lambda logic
Abram Demski
Since early December, I have been working on a
hopefully-foundation-worth logic with the following properties.
The language of the logic is lambda calculus augmented with an
equality function that is treated as a first-class function:
Syntax:
a, b, c, ... [a variable-name is a term]
(t1 t2) [function application: a term applied to a term is a term]
lambda v . t [lambda abstraction: for any variable b and any
term t, lambda v . t is a term]
t1 = t2 [equality: a term set equal to a term is a term]
Note: I could also just say "= is a term", but this is a bit nicer.
"Sentences" can be distinguished from other terms by specifying that
they are of the form t1 = t2.
The idea here is to create an untyped version of Church's
higher-order-logic, similar to what Luke Palmer was talking about on
this list during the summer. The motivation for the logic was Russell
Wallace's desire to have an untyped foundation for his system, which
was to perform automated reasoning about computer programs.
Actually, since I augment lambda calculus with equality rather than
with truth functions (as is more traditional), it's more an untyped
version of the HOL Light system than of Church's original calculus. In
the typed higher-order logics, these two alternatives can be shown to
be equivalent. In the untyped system I created, however, I found that
I could define truth functions and quantifiers based on equality, but
the usual definition of equality in terms of truth functions and
quantifiers failed.
To avoid paradox despite the absence of type theory, my idea was to
adapt Kripke's least-fixed-point construction, normally applied to
create languages containing their own truth predicates.
The idea behind the construction is simple: let statements be
"grounded" if their truth or falsehood depends just on some basic
level of untroubled truths and falsehoods. (This would typically be
facts "about the world", but essentially all that's required is that
we know that the basic level is free of paradox.) A grounded statement
can be one which refers just to the world, or it can be grounded by
virtue of depending on other grounded statements. Tim Maudlin's "Truth
and Paradox: Solving the Riddles." Statements which are ungrounded are
taken to be meaningless.
For my system, this means that equality (and inequality) is considered
meaningful only in some cases: we start with basic cases which are
obviously well-defined (such as the comparison of pure lambda terms to
each other) and mark a statement grounded whenever its truth depends
just on grounded statements.
Unlike type theory, this method of avoiding paradox does not
distinguish between meaningful and meaningless terms, only meaningful
and meaningless statements. Undefinedness does not result from just
any nonterminating lambda evaluation: only nonterminating
truth-functional evaluations. (Thus the Y combinator is usable.) If we
think of sets as functions which return true or false, then this
theory is a naive set theory in the sense that a set can be formed
from any statement; however, set membership is not always defined.
(For example, the Russel set "all sets which do not include
themselves" exists; however, it is undefined whether it is a member of
itself or not.)
The logic also has a few other pleasing properties.
However, I've found that this logic has some apparently-fatal flaws
which prevent it from defining basic notions such as numbers.
Specifically, universally quantified statements come out meaningless
too often to be of much use.
Suppose we want to define numbers as the least set which includes zero
and is closed under the successor function. In other words, it is the
intersection of all sets which include zero and which include s(x)
whenever they include x.
The intersection of all sets satisfying some predicate P should be
defined as the set of elements e for which "for all x, P(x) implies e
is an element of x" holds.
Unfortunately, this universal statement will never come out true. The
set for which membership is always meaningless (such a set is easy to
construct) will serve as a "counterexample" to the statement; not a
real counterexample, because it doesn't make the statement false, but
it does make the statement always meaningless: because there is one
meaningless instance, it can never be the case that all instances are
true (which is what's required).
So, the natural-seeming definition of the set of natural numbers
fails: it ends up telling us that membership is always undefined in
that set.
Basically, this is an extension of an observation Tim Maudlin made in
his book: we can't really properly formulate restricted quantification
in a fixed-point logic.
I am thinking of a possible solution. If it turns out to work well,
I'll have more to say later. :)
--
Abram Demski
http://dragonlogic-ai.blogspot.com/
http://groups.google.com/group/one-logic
YKY (Yan King Yin, 甄景贤)
> Since early December, I have been working on a
> hopefully-foundation-worth logic with the following properties.
Perhaps you can say a bit more about your objective for the logic, do
you want to achieve maximal "generality", and what does generality
mean (even informally described).
I read that if a logic can axiomatize Peano arithmetics then it would
be incomplete by Godel incompleteness -- meaning there are some valid
statements in it that allow no proof.
HOL under standard semantics can axiomatize Peano arithmetics,
therefore it is incomplete, but under Henkin semantics it can be made
complete but at the cost of losing the ability to axiomatize N and R
(the natural numbers and the reals).
It seems that if a logic cannot axiomatize N and R would not be able
to describe some parts of mathematics. Thus, if you want the
generality to describe all of mathematics, the logic would be
necessarily incomplete.
Facing this dilemma, what would be your goal?
> The idea behind the construction is simple: let statements be
> "grounded" if their truth or falsehood depends just on some basic
> level of untroubled truths and falsehoods. (This would typically be
> facts "about the world", but essentially all that's required is that
> we know that the basic level is free of paradox.) A grounded statement
> can be one which refers just to the world, or it can be grounded by
> virtue of depending on other grounded statements. Tim Maudlin's "Truth
> and Paradox: Solving the Riddles." Statements which are ungrounded are
> taken to be meaningless.
Sounds reasonable.
> If we
> think of sets as functions which return true or false, then this
> theory is a naive set theory in the sense that a set can be formed
> from any statement; however, set membership is not always defined.
> (For example, the Russel set "all sets which do not include
> themselves" exists; however, it is undefined whether it is a member of
> itself or not.)
Very interesting...
> The intersection of all sets satisfying some predicate P should be
> defined as the set of elements e for which "for all x, P(x) implies e
> is an element of x" holds.
>
> Unfortunately, this universal statement will never come out true. The
> set for which membership is always meaningless (such a set is easy to
> construct) will serve as a "counterexample" to the statement; not a
> real counterexample, because it doesn't make the statement false, but
> it does make the statement always meaningless: because there is one
> meaningless instance, it can never be the case that all instances are
> true (which is what's required).
Wait... your pseudo-counter-example, does not mean that the for-all
statement can never be satisfied for *some* sets. It merely shows
that it fails for one set, namely your always-meaningless set.
> Basically, this is an extension of an observation Tim Maudlin made in
> his book: we can't really properly formulate restricted quantification
> in a fixed-point logic.
I'll check out his book and reply on this point later...
YKY
Abram Demski
To make it clear I'll have to copy the formalisation which I've
written down, but basically: because the property of "containing zero
and containing a successor for each element" relies on evaluating
"containing zero", it will come out undefined for the always-undefined
set. This means we don't know whether this set is one of the ones in
the intersection or not. We *also* don't know anything about the
nature of this set *otherwise*... for all we know it could be the
empty set. But then the intersection would also be the empty set, so
no numbers would exist.
Of course, if the set really were the empty set (or some other set not
containing the numbers), then it would not meet the condition for the
intersection in the first place... so it really shouldn't cause a
problem. However, the fixed point construction does not reason this
way. It doesn't matter if all possible combinations of values for
currently-undefined statements *would* imply a particular statement--
if they are undefined, then no implications follow from them.
> Perhaps you can say a bit more about your objective for the logic, do
> you want to achieve maximal "generality", and what does generality
> mean (even informally described).
I'm not really striving for some sort of universal generality with
this logic; at least not at this stage. It's not the "one logic" I'm
looking for-- just a study of some desirable properties.
I'm ok with incompleteness-- I want to be able to interpret peano
arithmetic. For a "true foundation," I would like a story that
explains in a satisfying manner how a mere machine (the brain) can
ascribe to sentences a semantics which cannot be captured by any
formal system (for a very specific meaning of the word "captured").
But, this logic is not intended to help that.
I'm also ok with undefinability; some people take the fixed point to
be a solution to that problem, but I do not. For the true foundation,
again, I'd like a "good story" that explains why it looks like no
logic (finite or infinite, machine-able or otherwise) can express
every meaningful statement; but this logic is not intended to do that.
Still, it has some interesting properties in this area.
What this logic is intended to do is provide a practical foundation
for computerised theorem proving which (1) implements an essentially
naive set theory without leading to paradox, and (2) satisfies the
property that any computable enumeration of statements within the
language can be asserted within the language (ie, we never have to
resort to an "axiom schema" to say something meaningful, as we do with
FOL).
Of course I also hope that these two properties are useful in the
eventual resolution of foundational problems.
--Abram
2010/1/27 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>:
> --
> 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.
YKY (Yan King Yin, 甄景贤)
> To make it clear I'll have to copy the formalisation which I've
> written down, but basically: because the property of "containing zero
> and containing a successor for each element" relies on evaluating
> "containing zero", it will come out undefined for the always-undefined
> set. This means we don't know whether this set is one of the ones in
> the intersection or not. We *also* don't know anything about the
> nature of this set *otherwise*... for all we know it could be the
> empty set. But then the intersection would also be the empty set, so
> no numbers would exist.
>
> Of course, if the set really were the empty set (or some other set not
> containing the numbers), then it would not meet the condition for the
> intersection in the first place... so it really shouldn't cause a
> problem. However, the fixed point construction does not reason this
> way. It doesn't matter if all possible combinations of values for
> currently-undefined statements *would* imply a particular statement--
> if they are undefined, then no implications follow from them.
OK, now I understand the problem.
> I'm not really striving for some sort of universal generality with
> this logic; at least not at this stage. It's not the "one logic" I'm
> looking for-- just a study of some desirable properties.
>
> I'm ok with incompleteness-- I want to be able to interpret peano
> arithmetic. For a "true foundation," I would like a story that
> explains in a satisfying manner how a mere machine (the brain) can
> ascribe to sentences a semantics which cannot be captured by any
> formal system (for a very specific meaning of the word "captured").
> But, this logic is not intended to help that.
>
> I'm also ok with undefinability; some people take the fixed point to
> be a solution to that problem, but I do not. For the true foundation,
> again, I'd like a "good story" that explains why it looks like no
> logic (finite or infinite, machine-able or otherwise) can express
> every meaningful statement; but this logic is not intended to do that.
> Still, it has some interesting properties in this area.
>
> What this logic is intended to do is provide a practical foundation
> for computerised theorem proving which (1) implements an essentially
> naive set theory without leading to paradox, and (2) satisfies the
> property that any computable enumeration of statements within the
> language can be asserted within the language (ie, we never have to
> resort to an "axiom schema" to say something meaningful, as we do with
> FOL).
>
> Of course I also hope that these two properties are useful in the
> eventual resolution of foundational problems.
My current idea of how to achieve universality is to augment the logic
with "procedural" elements, but I don't have any concrete idea of how
to do that yet.
About enumerability: I've read that the set of second-order valid
formulae is not arithmetically definable, let alone recursively
enumerable. I don't know the exact reasons behind that, nor do I
understand the implications of non-enumerability. I'll think about
these issues...
YKY
Abram Demski
The enumerability constraint is simply based on the intuition that if
I can specify a pattern for writing down certain sentences, then I can
point at it and say "all those are true".
Following the constraint implies being too powerful for a complete
deductive system to exist: there's no computable way to determine
which such patterns satisfy the predicate "all those are true".
The search for the correct logic has been characterised as one in
which there are many desirable properties, and strong negative results
showing that not all of them can be had simultaneously. I don't have
any argument showing that this particular property is desirable *above
all the others which conflict with it*... it's just one direction for
research among many.
I think the ideas which will persist in this field, as in any field,
are those which hold true regardless of methodology employed; those
results which can be seen independently of a particular approach.
Ideally, one should subsume and transcend other systems.
On that note, so far my attempts to fix this logic to get it to
interpret talk about numbers (in the way I want) have failed.
How are you doing with HOL Light?
--Abram
2010/2/1 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>:
YKY (Yan King Yin, 甄景贤)
> The search for the correct logic has been characterised as one in
> which there are many desirable properties, and strong negative results
> showing that not all of them can be had simultaneously. I don't have
> any argument showing that this particular property is desirable *above
> all the others which conflict with it*... it's just one direction for
> research among many.
>
> I think the ideas which will persist in this field, as in any field,
> are those which hold true regardless of methodology employed; those
> results which can be seen independently of a particular approach.
> Ideally, one should subsume and transcend other systems.
Good point. I'm now working on my AGI book again, and will include a
section on higher-order logics. I plan to gather all the relevant
background knowledge in one summary (without getting too technical).
Maybe I'll show you the draft and you can contribute something to it
=) ... My knowledge in this area is still very scant.
> On that note, so far my attempts to fix this logic to get it to
> interpret talk about numbers (in the way I want) have failed.
Is your definition of N the simplest or most natural? Is there some
other way to state the set { S(0), S(S(0)) ... } ?
> How are you doing with HOL Light?
Still trying to understand the source code. But I'm now learning a
bit about Cambridge LCF first. Lawrence C Paulson has done a lot in
this area...
YKY