type theory and higher order logic? : Functional

This is maybe OT but I wonder if anyone can interpret this sentence
from Wikipedia's article "Second-order logic":

In mathematical logic, second-order logic is an extension of
first-order logic, which itself is an extension of propositional
logic. Second-order logic is in turn extended by type theory.

I'd like to know what it means that second-order logic is extended by
type theory, and reading the Wiki article about type theory hasn't
really clarified that.

I also wonder whether higher-order logic (in the sense of quantifying
over sets, then relations, then whatever) has something to do with
HOL, a theorem proving system written in ML.

I also wonder why first order logic is so bloody important anyway,
i.e. why do we go through the contortions of trying to base all of
mathematics on ZFC, a first-order axiomitization of set theory? It
means we need infinite axiom schema and we still end up with annoying
artifacts like Skolem's paradox. The usual formulations of the real
numbers and Peano arithmetic are written in second-order logic (to
express the least-upper-bound property and the induction principle,
respectively). Does something stop us from writing and formally
checking regular math proofs in 2nd (or higher) order logic? Is that,
heh heh, what HOL (the ML system) actually is?

Finally I think in recent decades logic has been reformulated
independently of set theory (in other categories or "topoi") and I
wonder if the concept of second-order logic still applies since there
aren't really sets, and if this stuff is of relevance to programming
language thoery.

I had one logic class in college a long time ago but am basically
getting my info from Wikipedia, so please be gentle, as I don't know
very much.

Paul Rubin wrote:
{stuff deleted}
> I'd like to know what it means that second-order logic is extended by
> type theory, and reading the Wiki article about type theory hasn't
> really clarified that.

I'm not 100% sure that makes sense to me either.. it is Wikipedia so
maybe it's just being a bit sloppy.

> I also wonder whether higher-order logic (in the sense of quantifying
> over sets, then relations, then whatever) has something to do with
> HOL, a theorem proving system written in ML.

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.

> I also wonder why first order logic is so bloody important anyway,
> i.e. why do we go through the contortions of trying to base all of
> mathematics on ZFC, a first-order axiomitization of set theory? It
> means we need infinite axiom schema and we still end up with annoying
> artifacts like Skolem's paradox. The usual formulations of the real
> numbers and Peano arithmetic are written in second-order logic (to
> express the least-upper-bound property and the induction principle,
> respectively). Does something stop us from writing and formally
> checking regular math proofs in 2nd (or higher) order logic? Is that,
> heh heh, what HOL (the ML system) actually is?

This is the like asking why do people program in C and not ML. The
answer is far more sociological then technical. Checking if a proof is
valid is no more difficult in a higher-order logic than a first-order
logic. Automatically, finding a proof is a bit easier if first-order
logics, but I personally think that is a poor reason to restrict your
foundations.

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

> Finally I think in recent decades logic has been reformulated
> independently of set theory (in other categories or "topoi") and I
> wonder if the concept of second-order logic still applies since there
> aren't really sets, and if this stuff is of relevance to programming
> language thoery.

Second-order ness is somewhat separate from the foundations of the
underlying logic. These days, I'm very agnostic about foundations, it's
very futile to argue about which set of axioms is the "right" set of
axioms. It all depends on what you're trying to do. I think,
higher-order logics have been easier to mechanize than systems based on
ZF, which is why I would tend to prefer HOL like systems.

> I had one logic class in college a long time ago but am basically
> getting my info from Wikipedia, so please be gentle, as I don't know
> very much.

Paul Rubin wrote:
{stuff deleted}
> I'd like to know what it means that second-order logic is extended by
> type theory, and reading the Wiki article about type theory hasn't
> really clarified that.

I'm not 100% sure that makes sense to me either.. it is Wikipedia so
maybe it's just being a bit sloppy.

> I also wonder whether higher-order logic (in the sense of quantifying
> over sets, then relations, then whatever) has something to do with
> HOL, a theorem proving system written in ML.

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.

> I also wonder why first order logic is so bloody important anyway,
> i.e. why do we go through the contortions of trying to base all of
> mathematics on ZFC, a first-order axiomitization of set theory? It
> means we need infinite axiom schema and we still end up with annoying
> artifacts like Skolem's paradox. The usual formulations of the real
> numbers and Peano arithmetic are written in second-order logic (to
> express the least-upper-bound property and the induction principle,
> respectively). Does something stop us from writing and formally
> checking regular math proofs in 2nd (or higher) order logic? Is that,
> heh heh, what HOL (the ML system) actually is?

This is the like asking why do people program in C and not ML. The
answer is far more sociological then technical. Checking if a proof is
valid is no more difficult in a higher-order logic than a first-order
logic. Automatically, finding a proof is a bit easier if first-order
logics, but I personally think that is a poor reason to restrict your
foundations.

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

> Finally I think in recent decades logic has been reformulated
> independently of set theory (in other categories or "topoi") and I
> wonder if the concept of second-order logic still applies since there
> aren't really sets, and if this stuff is of relevance to programming
> language thoery.

Second-order ness is somewhat separate from the foundations of the
underlying logic. These days, I'm very agnostic about foundations, it's
very futile to argue about which set of axioms is the "right" set of
axioms. It all depends on what you're trying to do. I think,
higher-order logics have been easier to mechanize than systems based on
ZF, which is why I would tend to prefer HOL like systems.

> I had one logic class in college a long time ago but am basically
> getting my info from Wikipedia, so please be gentle, as I don't know
> very much.

On 5 helmi, 08:49, Paul Rubin <http://phr...@NOSPAM.invalid> wrote:
> I also wonder why first order logic is so bloody important anyway,
> i.e. why do we go through the contortions of trying to base all of
> mathematics on ZFC, a first-order axiomitization of set theory?

Do we?

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. 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 - of form "the Diophantine
equation P(x_1, ..., x_n) = 0 has no solutions", even - can be proved.
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. Thus in the logical literature a
theory known as "second order arithmetic" and its subtheories are
studied, and confusingly, these are first order theories! In these
theories the induction axiom is a single statement, and not a scheme:

For all sets X, if 0 is in X and whenever n is in X, n+1 is in X,
then all naturals are in X

and in addition we have axioms guaranteeing the existence of sets
defined or characterized by some class of conditions.

Now, what about ZFC? Unlike often claimed, mathematics is not in any
interesting way based on the first order theory ZFC. 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. By the completeness
theorem for first order logic - and a few conceptual observations due
to Georg Kreisel - we know that whenever a mathematical statement A is
proved using principles P, the formalization of A is formally provable
from the formalization of P. It turns out, as established by careful
****ysis over a considerable period of time, that whenever a statement
A is proved in ordinary mathematics, its formalization is provable in
ZFC. We can thus, for example, conclude that using the principles
currently accepted in ordinary mathematics, the continuum hypothesis
can't be proved or refuted, from the fact that it is formally
unprovable and unrefutable in ZFC. So facts about formal theories,
such as ZFC, related to actual mathematical practice, sometimes tell
us something about the practice itself. But the formal theory ZFC in
no way justifies or constitutes mathematics.

> 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?

> Does something stop us from writing and formally checking regular math
> proofs in 2nd (or higher) order logic?

Regular mathematical proofs are not amenable to mechanical checking,
and formalizing them so as to be is a highly non-trivial task.
However, there is nothing special about second order logic in this
respect. 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. And, as
noted earlier, when we decide to accept some set of axioms A -
essentially telling us what sort of sets, sets of sets, and so forth,
exist - there is no essential difference between second order proofs
and first order proofs with A added as non-logical axioms about sets.

--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

Daniel C. Wang schrieb:
> Paul Rubin wrote:
>
>> I also wonder why first order logic is so bloody important anyway,
>> i.e. why do we go through the contortions of trying to base all of
>> mathematics on ZFC, a first-order axiomitization of set theory? It
>> means we need infinite axiom schema and we still end up with annoying
>> artifacts like Skolem's paradox. The usual formulations of the real
>> numbers and Peano arithmetic are written in second-order logic (to
>> express the least-upper-bound property and the induction principle,
>> respectively). Does something stop us from writing and formally
>> checking regular math proofs in 2nd (or higher) order logic? Is that,
>> heh heh, what HOL (the ML system) actually is?
>
> This is the like asking why do people program in C and not ML. The
> answer is far more sociological then technical. Checking if a proof is
> valid is no more difficult in a higher-order logic than a first-order
> logic. Automatically, finding a proof is a bit easier if first-order
> logics, but I personally think that is a poor reason to restrict your
> foundations.

That depends entirely on what you want to achieve.
If your domain is finding proofs for programs, then I'd tentatively agree.
Mathematicians might find those theorems interesting that are true in
first-order logic but not in higher orders.

Regards,
Jo

Joachim Durchholz wrote:
{stuff deleted}
> That depends entirely on what you want to achieve.
> If your domain is finding proofs for programs, then I'd tentatively agree.
> Mathematicians might find those theorems interesting that are true in
> first-order logic but not in higher orders.

I'll admit to a certain amount of tunnel vision with respect to what a
proof is "good for". I am curious about your second point. At some level
shouldn't the truth of a theorem be independent higher-order or
first-orderness?

On 6 helmi, 01:31, Joachim Durchholz <j...@durchholz.org> wrote:
> That depends entirely on what you want to achieve.
> If your domain is finding proofs for programs, then I'd tentatively agree.
> Mathematicians might find those theorems interesting that are true in
> first-order logic but not in higher orders.

What do you mean by this? Every first order proof of some statement in
some first order theory is also a proof - or can trivially be
translated into a proof - in a second order formulation of the same
theory. It is thus a bit obscure what yoyu have in mind with theorems
"that are true in first-order logic but not in higher orders".

To elaborate a bit on my earlier post, it might be noted that "second
order theories", in the sense of theories which include axioms about
sets, functions, and so forth, in addition to whatever specific axioms
pertain the subject matter of the theory - the naturals, inductively
defined structures, what have you - and also type theories, in which
the universe is divided into a rich hierarchy of types constructed in
all sorts of ways, such as Per Martin-Löf's constructive type theory
and various theories due to Feferman's, more closely mirror the way
mathematicians often actually reason, in the sense that the basic
principles and modes of reasoning employed in their "informal" proofs
have rather direct formal counterparts - for some values of "direct".
Set theory, on the other hand, in reducing all such stuff to a very
frugal set of primitives, does not allow such simple mapping from
ordinary modes of reasoning to formal proofs. So if one wishes to
actually produce formal proofs formal set theory is not the obvious
choice, similarly as programming in Haskell is much easier, at least
in the practical sense, than programming in some variant of lambda
calculus with no primitives for naturals and what not.

--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus

aatu.koskensilta@xortec.fi writes:
> > Mathematicians might find those theorems interesting that are true in
> > first-order logic but not in higher orders.
>
> What do you mean by this? Every first order proof of some statement in
> some first order theory is also a proof - or can trivially be
> translated into a proof - in a second order formulation of the same
> theory. It is thus a bit obscure what yoyu have in mind with theorems
> "that are true in first-order logic but not in higher orders".

Maybe he meanat the other way around, i.e. true (and provable) in
higher orders but not in first-order logic. Example: the set of real
numbers is uncountable. This of course requires the (second-order)
least upper bound axiom.

Joachim Durchholz schrieb:
> That depends entirely on what you want to achieve.
> If your domain is finding proofs for programs, then I'd tentatively agree.
> Mathematicians might find those theorems interesting that are true in
> first-order logic but not in higher orders.

The last phrase should have read

"that are true about first-order logic but not about higher orders".

Sorry for the confusion.

Regards,
Jo

On 6 Feb, 21:21, Joachim Durchholz wrote:
> Joachim Durchholz schrieb:
> > That depends entirely on what you want to achieve.
> > If your domain is finding proofs for programs, then I'd tentatively agree.
> > Mathematicians might find those theorems interesting that are true in
> > first-order logic but not in higher orders.
>
> The last phrase should have read
>
> "that are true about first-order logic but not about higher orders".

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? After
all, whatever interest formalizing such a proof might have -
mechanically checking the proof, extracting lower bounds, establishing
that some witnessing function belongs to some class of recursive
functions, extracting a program from the proof, providing the proof as
a witness of some invariant to a compiler, ... - are dependent on
proof theoretical, not semantic, properties of the theory (and
background logic) they're formalized in, and there is no essential
difference between first and higher order logics in this regard.
(There are, of course, all sorts of proof theoretical differences
between, say, predicative and impredicative comprehension on second
order level, but those don't go away just by going first order and
taking the logical principles as non-logical axioms.)

--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus