type theory and higher order logic? : Functional

aatu.koskensilta@xortec.fi schrieb:
> Sure, higher order logic is not as well-behaved as first order logic;
> compactness fails, completeness fails, the Löwenheim-Skolem theorems
> don't hold, validity is straggeringly complex, ... However, why should
> this mean that someone wishing to prove something about programs would
> choose first order logic and not, say, some form of type theory?

Beats me either.
Personally, I'd use general boolean expressions over run-time and
compile-time entities when reasoning about programs, and never mind
undecidability - tools should infer as much as they can, and rely on
human help to get around the real problems. From that perspective, even
H-M and dependent-type theories are too restrictive.

I just found Daniels statement a bit too strong. There are valid reasons
why one would be interested in first-order logic; it does have some nice
properties, and if I were to write an inference engine, I'd try to stay
within the simplest theory that will do as long as possible, even if
that's just a heuristic.
(Reminds me of Haskell, where things are mostly H-M but you can add
annotations if you need to go beyond that.)

Regards,
Jo

aatu.koskensilta@xortec.fi writes:
> First, let's note a crucial difference between first and higher order
> logic. First order logic is complete, in the technical sense that
> there exists a set of logical axioms and rules of inference such that
> whenever a statement A is logically implied by some set of statements
> T, there exists a formal proof of A from T.

If I understand that, it says A is provable iff A is true in all
models of T. There are unprovable (independent of T) statements which
are necessarily true in some models but not others. While in higher
order, there are statements that are true in all models yet still
unprovable. Is that so bad? I mean Goldbach's conjecture might be
independent of ZFC, but that means there's no counterexample, which
means it's true in the actual integers, i.e. true in all models of
Peano arithmetic yet unprovable in them.

> Higher order logics, on
> the other hand, are incomplete in the sense that there is no such set
> of logical axioms and rules of inference. Whenever we wish to actually
> produce a proof in second (or higher) order settings we are faced with
> the problem of choosing these axioms and rules of inference, and,
> unlike with first order logic, there is no canonical choice. In case
> of arithmetic, for example, what *logical* axioms we choose affects
> what purely arithmetical statements -

Hmm, well that sounds like a disagreement about what the integers
really are, but it's the same way with set theory, some people believe
the axiom of choice and others don't. They might say the
Banach-Tarski paradox is obviously false and therefore AC must be false.

> of form "the Diophantine equation P(x_1, ..., x_n) = 0 has no
> solutions", even - can be proved.

I think I heard something like that, is there a name for the result?
Anyway it just means something is provable or not, it doesn't mean
it's true with one reasonable axiom set and false with another.

> Essentially these axioms postulate the existence of sets - of reals,
> of naturals, of whatever it is our theory is about - and effectively
> what we are doing with such higher order proofs is just what we would
> do with first order logic formulation of the original theory with
> added axioms about set existence.

But I thought it was impossible (because of Lowenheim-Skolem) to even
assert that some set was uncountable, for example.

> Now, what about ZFC? Unlike often claimed, mathematics is not in any
> interesting way based on the first order theory ZFC.

Well I mean in a cultural sense, we don't say a theorem is proved
unless there's detailed enough reasoning to translate to a ZFC proof.

> Rather, "ordinary" mathematics can be carried out in the framework
> of set theory - i.e. basic concepts can be given set theoretical
> definitions and the basic mathematical properties of these can be
> proved using set theoretical principles - the way mathematics always
> is: by producing proofs (in the ordinary, and not technical, sense
> of the word), devising new concepts, putting forth conjectures, what
> have you. To be sure, certain basic set theoretical principles are
> implicitly used in this activity, though seldom explicitly stated.

I'm not sure of this, but an example might be how a lot of
mathematical physics relies on various nice theorems about doing
calculus in Hilbert space, which in turn depend on the Hahn-Banach
theorem, which is usually proved using Zorn's lemma, a restatement of
AC. Or as a more severe example, the Banach-Tarski paradox in real
****ysis invokes AC directly. Or there's all that algebraic geometry
done over abstract categories, etc.

> > It means we need infinite axiom schema and we still end up with
> > annoying artifacts like Skolem's paradox.
>
> Why should technical results about first order logic annoy anyone? In
> particular, why should it annoy us that there is a countable model of
> set theory?

Because one of those sets is the real numbers, which we like to think
are uncountable .

> However, since there is no canonical set of axioms and rules
> of inference for second order logic, in checking a formal proof in
> higher order settings we must make non-trivial decisions with
> mathematical consequences regarding what axioms we accept.

Hmm, I should try to find out more about this. I'm looking at the
Wikipedia article about second-order arithmetic, which is pretty
interesting. Thanks!

In article <1170790310.745031.57940@a34g2000cwb.googlegroups.com>,
aatu.koskensilta@xortec.fi wrote:
>
> However, why should this mean that someone wishing to prove
> something about programs would choose first order logic and not,
> say, some form of type theory?

There are pragmatic reasons to do this, the primary one being that
first-order unification has a fast algorithm, and higher-order
unification is undecidable. As a result, automated theorem proving in
first order logic is occasionally tractable, and theorem proving in
higher-order logic is just basically utterly hopeless.

However, if you're building a proof assistant rather than a theorem
prover, using a very rich type theory makes the task of formalization
much, much easier on the human user.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

There is nothing preventing you for building a theorem prover for
higher-order logic that only deals with a first-order subset of the
logic. If the prover is too dumb to figure something out using
first-order reasoning, the user can just prove a first-order get the
prover unstuck.

That said it is interesting to study first-order logical systems because
they have better provability results, but unless you want your system to
prove all the theorems you care about fully automatically there's no
reason to stick to first-order logic. The minute you have any
semi-automated technique you might as well choose the most expressive
logic you can stomach and then try to develop complete theories and
provers for subsets of the logic as appropriate.

The alternative is to start with a first-order theory and discover you
have to continually hack in axioms or rule schema's to deal with
deductions that could probably be expressed in some richer logic. So
over time your systems is likely to collect a lot of cruft.

Neelakantan Krishnaswami wrote:
> In article <1170790310.745031.57940@a34g2000cwb.googlegroups.com>,
> aatu.koskensilta@xortec.fi wrote:
>> However, why should this mean that someone wishing to prove
>> something about programs would choose first order logic and not,
>> say, some form of type theory?
>
> There are pragmatic reasons to do this, the primary one being that
> first-order unification has a fast algorithm, and higher-order
> unification is undecidable. As a result, automated theorem proving in
> first order logic is occasionally tractable, and theorem proving in
> higher-order logic is just basically utterly hopeless.
>
> However, if you're building a proof assistant rather than a theorem
> prover, using a very rich type theory makes the task of formalization
> much, much easier on the human user.

"Daniel C. Wang" <danwang74@gmail.com> writes:
> I'm not 100% sure that makes sense to me either.. it is Wikipedia so
> maybe it's just being a bit sloppy.

I'm trying to read up on type theory. A friend of mine has Pierce's
book "Types and Programming Languages" and says I can borrow it but I
haven't had a chance to go see him for that. Do you think the book
will help?

> The underling logic use in the HOL system, is a higher-order logic
> based on a modern versions of Church's original typed lambda calculus.

Cool--but since it's full of classical math theorems, is there a way
to mechanically convert the HOL proofs into ZFC proofs?

> BTW you might find this link useful http://www.cs.ru.nl/~freek/100/

Oh yes, I saw that, I hadn't realized previously that so much had been
done, or that Mizar was no longer in the forefront of this stuff.
Still it looks like there's some fairly easy proofs on the list that
haven't yet been formalized.

> Second-order ness is somewhat separate from the foundations of the
> underlying logic.

Hmm, ok, I just am not sure what it means to quantity over sets, if
there aren't any sets to quantify over.

Paul Rubin <http://phr.cx@nospam.invalid> wrote:
> "Daniel C. Wang" <danwang74@gmail.com> writes:
>> I'm not 100% sure that makes sense to me either.. it is Wikipedia so
>> maybe it's just being a bit sloppy.
>
> I'm trying to read up on type theory.

The Wikipedia article on that subject isn't particularly good. You may
get a better idea what's it about by reading e.g.

http://plato.stanford.edu/entries/type-theory/

> A friend of mine has Pierce's book "Types and Programming Languages"
> and says I can borrow it but I haven't had a chance to go see him
> for that. Do you think the book will help?

IIRC, Pierce's book doesn't deal with type theory in the "mathematical"
sense.

- Dirk

Neelakantan Krishnaswami schrieb:
> However, if you're building a proof assistant rather than a theorem
> prover, using a very rich type theory makes the task of formalization
> much, much easier on the human user.

In what ways does a type system help here?

Regards,
Jo

In article <eqdacr$te0$1@online.de>, Joachim Durchholz wrote:
> Neelakantan Krishnaswami schrieb:
>> However, if you're building a proof assistant rather than a theorem
>> prover, using a very rich type theory makes the task of formalization
>> much, much easier on the human user.
>
> In what ways does a type system help here?

Thanks to Curry-Howard, a type system is a logic. If you have a rich
logic (eg, higher order logic), then you can express definitions much
more succintly and naturally than you can in a weaker one. This makes
the task of formalization easier, because the human user of the system
can keep his or her definitions and proofs closer to the mathematics.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Neelakantan Krishnaswami <neelk@cs.cmu.edu> writes:
> Thanks to Curry-Howard, a type system is a logic. If you have a rich
> logic (eg, higher order logic), then you can express definitions much
> more succintly and naturally than you can in a weaker one. This makes
> the task of formalization easier, because the human user of the system
> can keep his or her definitions and proofs closer to the mathematics.

Do humans use higher than second order logic? I gather 2-OL allows
quantification over sets, and 3-OL allows quantification over
relations. But we're taught in school that relations are just sets of
ordered pairs, and we really do think of them that way; it's not an
artificial construction like thinking of natural numbers as von
Neumann ordinals.

I'd like to tie this stuff back to programming though. What little
logic I know is from math class, and programmers (I mean those working
with software proofs etc.) seem to approach it differently. Is there
good stuff to read online?

My thanks to everyone who's been posting--it's all been informative.

Paul Rubin <http://phr.cx@nospam.invalid> wrote:
> Neelakantan Krishnaswami <neelk@cs.cmu.edu> writes:
>> Thanks to Curry-Howard, a type system is a logic. If you have a rich
>> logic (eg, higher order logic), then you can express definitions much
>> more succintly and naturally than you can in a weaker one. This makes
>> the task of formalization easier, because the human user of the system
>> can keep his or her definitions and proofs closer to the mathematics.

> I'd like to tie this stuff back to programming though. What little
> logic I know is from math class, and programmers (I mean those working
> with software proofs etc.) seem to approach it differently.

Programmers nearly always want to express information about the
programs they write> They just do it in different ways, and call it
unit tests, or pre- and postconditions, or other things. A type system
is just another way to express such information. With the additional
benefit that you have an "automatic theorem prover" (the compiler)
which checks statically that what you say about your program really
holds, always, no matter what actual values you use when the program
runs.

But of course, then you need to balance things: The more expressive
your type system is, the more you can say about your programs, but
the harder it gets to do type inference or type checking.

- Dirk