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.
On 1/8/23 03:23, 'Alexander van der Vekens' via Metamath wrote:
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
<http://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 <http://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
<https://groups.google.com/d/msgid/metamath/1b9f36b7-a37b-4e00-a222-769371acf11bn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/96e72c78-4bc2-c451-89aa-00bc5cb57378%40panix.com.
