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
On Saturday, March 9, 2019 at 6:45:43 PM UTC+1 David A. Wheeler wrote:
> 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.
>
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/1b9f36b7-a37b-4e00-a222-769371acf11bn%40googlegroups.com.
