Is MPE really *just* first order?

[David A. Wheeler]

Is MPE really *strictly* a first order logic (FOL)?
I thought first-order allows A. x .... where x must be a set variable, while
second order allowed A. F ... where F could be a relationship or function.

In MPE quantifiers must range over sets in FOL. That sounds first-order.
However, functions and relationships are *themselves* represented as sets
(well, pairs, which are implemented as sets).
E.g., in MPE you can say ` A. r A. x A. y ( ph -> x r y ) `which looks
a whole lot like quantifying over a relationship. So now I'm not sure I
understand the true distinction here.

Wikipedia's not helping:
https://en.wikipedia.org/wiki/Second-order_logic
That page claims that "one needs second-order logic to assert the
least-upper-bound property for sets of real numbers" - yet we seem
to have no problems in MPE with statements about surpremums.

I may just be tired & not seeing the obvious, but a quick clarification would be great...!

--- David A. Wheeler

[Jim Kingdon]

This is one of those things where the explanation can be more difficult than the concept. I'll give it a try but maybe there is a better explanation in the literature somewhere.

First-order logic is the system produced by the axioms of Margaris, or equivalently by the metamath axioms in the propositional and predicate logic sections.

Add the Peano axioms and you get first-order arithmetic. This is a theory that can talk about natural numbers but not sets of natural numbers.

Add the ability to quantify over propositions and you get second order arithmetic (I'm glossing over a bunch of details here, mostly because I don't know them). See https://plato.stanford.edu/entries/logic-higher-order/ especially the section "1. Syntax and translation"

On the other hand, if you go back to first order logic and add the axioms of ZF, you get set theory. In this case a set is just an individual variable. The logic itself doesn't give you sets, the ZF axioms do.

The reason people say that set theory is like second order arithmetic is that you can do much of the same mathematics (e.g. construction and theorems of real numbers) with either one. But they are built from axioms which look pretty different from each other, so they get there by different routes.

I'm sure there are people on the list who know this stuff much better than I do, but hopefully the above is both accurate and helpful.

[Mario Carneiro]

set.mm is not strictly first order, but not for the reasons you've identified. The "pseudo second order" has to do with the ability to state theorems with wff and class metavariables. This is not truly second order because we don't have existential quantification, only universal. But let's ignore this aspect for now and focus on just the actual forall quantifier of set.mm.

Ignoring classes, set.mm implements ZFC, which is a first order theory. There is one domain of quantification, whose elements are interpreted as sets. But because set theory provides such a rich structure in this domain, it is possible to emulate entire models of first order theory *inside* set theory. If you have a set M, then you can quantify over the elements of M with A. x e. M and E. x e. M . But because M is a set, we can also quantify over the powerset of M, and the powerset of that, so we get full higher order logic over M.

If you don't restrict to a set, you get something less than second order logic over the universe. There are objects that can pretend to be relations and predicates over the universe but they aren't all there, so some things turn out different to second order logic. With your example ` A. r A. x A. y ( ph -> x r y ) ` , the quantifier over r is not quantifying over all relations that could hold of x and y - for example we would want to include the relation { <. x , y >. | T. } = ( _V X. _V ), but this is not a set, so we can't instantiate the quantifier with it. Concretely, E. R A. x A. y x R y is provable in second order logic, but E. r A. x A. y x r y is disprovable in ZFC.

On Sat, Mar 9, 2019 at 12:03 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:

That page claims that "one needs second-order logic to assert the
least-upper-bound property for sets of real numbers" - yet we seem
to have no problems in MPE with statements about surpremums.

This example has to do with the example from the second paragraph above. ZFC is first order if the domain is the whole universe, but if you restrict the domain to a set then you get HOL, so the fact that we can deal with sets of reals and suprema has to do with the fact that RR is a set. One needs second-order logic to assert the LUB property *if the domain of discourse is RR*, but if the domain is all of set theory then you can deal with high order real quantifiers while staying first order ZFC.

Mario

[David A. Wheeler]

Thanks everyone!
Here's a summary that is hopefully actually correct.
I cobbled part of it from previous comments with a lot of tweaks
(I hope that's okay!).

I think this should go in some explanatory material, maybe the book
or mmset.html. There are a lot of references to "first order",
but not much explanation about that.

--- David A. Wheeler

=======

The logic system of the Metamath Proof Explorer (set.mm)
is a first order logic, and ZFC is a first order theory of sets.
First order systems are very widely-used systems.
In all first order systems,
quantifiers such as ` A. ` and ` E. ` can only
range over one domain or a subset of that one domain.
In our case, that one domain (called the "domain of quantification") is sets.
This means, for example,
that we cannot say ` E. ph ` ... (where ` ph ` is a wff)
or ` A. A ` ... (where ` A ` is a class, function, or relation).

Second order logic (SOL) and higher order logic (HOL) remove those constraints,
but that does not make those alternatives necessarily better.
Our set theory provides rich structures, so
first order logic is a powerful system and is generally quite sufficient.

If you have a set M, then you can quantify over the elements of M
with ` A. x e. M ` and ` E. x e. M ` .

In addition, because M is a set, we can also quantify

over the powerset of M, and the powerset of that, so we get full higher

order logic over M in that sense.

For example, there are some claims that to express the
least upper bound (LUB) property,

"one needs second-order logic to assert the
least-upper-bound property for sets of real numbers"

(Wikipedia page on Second-order logic).
Yet MPE has no problems making statements about supremums of the real numbers.

ZFC is first order if the domain is the whole universe, but if you restrict

the domain to a set that isn't *all* sets
then you get the effect of HOL.
So the fact that we can deal with

sets of reals and suprema has to do with the fact that RR is a set.

One needs second-order logic to assert the LUB property if the entire domain of
discourse is ` RR*m`m, but if the domain is all of set theory
(as it is in our case) then you can deal
with high order real quantifiers while staying within first order ZFC.

Our system supports relations, predicates, and functions with first order logic.
Some things are different than they would be in second order logic.
For example, we represent relations as sets that express the relationships
between sets, e.g., ` x R y ` expresses the relationship ` R ` between two
sets ` x ` and ` y ` .
We can easily express ` A. r A. x A. y ( ph -> x r y ) ` , because that quantifies
over a set ` r ` , but the quantifier over r is not quantifying over all
relations that could hold of ` x `and ` y ` .
For example, we might want to include
the relation ` { <. x , y >. | T. } = ( _V X. _V ) ` ,

but this is not a set, so
we can't instantiate the quantifier with it.
Concretely, ` E. R A. x A. y x R y `
is provable in second order logic, but ` E. r A. x A. y x r y `
is disprovable in ZFC.

In can be said that set theory is like second order arithmetic,
in the sense that you can do much of the same mathematics

(e.g. construction and theorems of real numbers) with either one.

But they are built from axioms which look very different from each other,

so they get there by different routes.

From a technical point of view set.mm is not strictly first order,
but for different reasons.
There is a "pseudo second order" capability that

has to do with the ability to state
theorems with wff and class metavariables.

This comes "for free" as part of the Metamath ability to do general substitutions,
and make it easy to express inference rules like modus ponens.

This is not truly second order
because we don't have existential quantification, only universal

(an implied "for all" when a variable is not bound).
However, it is fair to say that MPE is generally a first order system.

[Alexander van der Vekens]

Recently, I asked myself the same question "Is MPE really *just* first order?" as David did in 2019, but found an answer neither by myself nor by looking at the official material (set.mm, book, home page). Fortunately, I found this post! Unfortunalely, however, the proposal of David to make its results officially available is not realized yet. I think it would be very important to clearly state (and explain) why set.mm does not need second or higher order logic, compared with HOL light or Isabelle, which are  higher-order locgic theorem provers (although I do not know if or how they make use of HOL, especially for proving the top 100 mathematical theorems).  I would like to have the text proposed by David (maybe after a review by Mario?) placed on the Metamath Proof Explorer Home Page (https://us.metamath.org/mpeuni/mmset.html).

Alexander

[Jim Kingdon]

I'm not sure I have more insight than anyone else about how to organize our documentation, but this text does look pretty good. I always read such things with an eye towards whether it makes sense to someone who doesn't already know the topic (this is especially a problem with proof system documentation, which sometimes assumes a lot of logic background, however the target audience should include people who don't yet know logic, or people who want to write proofs but are more interested in analysis/trigonometry/geometry/etc).  This text seems pretty good to me on that point. Towards the end it wades into topics which aren't quite as easy to cover in a few words, but I suppose it does OK.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1b9f36b7-a37b-4e00-a222-769371acf11bn%40googlegroups.com.