On Sun, Oct 20, 2019 at 1:31 PM Brian Nguyen <[email protected]>
wrote:
> Metamath uses disjoint variables instead of proper substitution as a
> primitive notion, and as stated in the Metamath book, "substitution and
> equality are intimately tied to each other" in Tarski's system for
> first-order logic with equality. The book also claims that "the traditional
> approach is also possible", so how do I encode traditional first-order
> logic without equality in Metamath? I tried something like this (added to
> set.mm):
> $c NFQ $.
> $v S S_1 S_2 v $.
> ${
> $f setvar v $.
> $f wff S $.
> $a wff NFQ v S $.
> $d v S $.
> $a |- NFQ v S $.
> $}
> ${
> $f setvar v $.
> $f wff S_1 S S_2 $.
> $f |- NFQ v S $.
> $d v S_1 $.
> $d v S_2 $.
> $a |- NFQ x S_1 S S_2 $.
> $}
> but this doesn't work because Metamath requires every variable to have a
> typecode.
>
It doesn't really make sense for a variable to not have a typecode, as that
defines what the variable is supposed to range over. FOL has two types,
"setvar" and "wff", (or just "var" and "wff" in this case), denoting
variables that range over the universe of discourse, and well formed
formulas containing those variables.
The issue with your example, aside from the lack of labels on $f/$a
statements, is that $f |- NFQ v S $. should be a $e statement, because it
is a logical hypothesis, not a variable declaration. Moreover, $a |- NFQ x
S_1 S S_2 $. doesn't make sense because "S_1 S S_2" is not a wff (it is the
concatenation of three wffs). You write $f wff S_1 S S_2 $. but I don't
know what this is supposed to mean. If you intend for the concatenation of
three wffs to be a wff, then this would be written $a wff S_1 S S_2 $.
instead, but I don't know what operation this is intended to denote, and
this isn't likely to achieve the goal because it's ambiguous.
What I'm trying to say is that the syntax errors make it difficult to guess
what you are trying to express here. That's not your fault, but perhaps it
might be more fruitful if you express yourself using words instead (or
symbols in a more familiar notation).
> There are many other stupid restrictions in Metamath, for example that the
> typecode of variables are global, that label tokens may not collide with
> math symbol tokens, or that dummy disjoint variable restrictions are
> required. ... And why do these useless restrictions exist even though they
> have nothing to do with proof validity?
>
These are all there to make verification, automated processing, and similar
actions simpler. None of them affect expressivity, and when faced with the
choice between simplicity of the language and ergonomics for theorem
writers, metamath comes solidly on the side of simplicity. This is not a
choice that everyone is willing to make, but it makes Metamath rather
unique in the space of theorem provers. (You could also put mandatory
spaces and one letter keywords in this category.)
> How do I encode the traditional notion of free variables and proper
> substitution in Metamath?
> ...
>
Which doesn't solve the actual problem: encoding *exactly* traditional
> first-order logic without equality in Metamath. Whether it is a
> "conservative extension" does not matter. Is it possible to encode
> traditional first-order logic without equality with no additional symbols
> in Metamath?
>
Not "with no additional symbols", because you at least need symbols to
represent the functions and judgments that encode proper substitution and
not-free checking. This question is related to a recent thread on github:
https://github.com/metamath/set.mm/issues/1183 , so you can get some
additional reading, but I will try to answer your exact question here.
In order to encode *exactly* traditional FOL without equality, we first
need a definition of what that is. I will suppose for now that there is one
non-logical relation, but to make it clear that this doesn't have to be set
theory I will use the notation "R x y" for it. I will use
https://people.math.ethz.ch/~halorenz/4students/LogikML/Nutshell.pdf as the
guide for the quantifier axioms, although they have a silly number of
propositional axioms so I will use the Lukasiewicz axioms instead.
Every rule in metamath acts like a pattern, that does a syntactic match and
does a local manipulation. All recursive functions can be recast as
axiomatic judgments with clauses given by axioms, so we will do that here
for the relations of "substitution" and "not-free". Besides that, we only
need the core judgments of FOL: provability, with the types "var" and "wff"
giving us the necessary syntactic classes.
$( "silly boilerplate" section $)
$c var term wff |- -> ( ) -. A. F/ subst substT = / $.
$v x $. vx $f var x $. $( x denotes a variable. $)
$v y $. vy $f var y $. $( y denotes a variable. $)
$v ph $. wph $f wff ph $. $( ph denotes a wff. $)
$v ps $. wps $f wff ps $. $( ps denotes a wff. $)
$v ch $. wch $f wff ch $. $( ch denotes a wff. $)
$v th $. wth $f wff th $. $( th denotes a wff. $)
$( I assume the Lukasiewicz axioms for propositional logic are
non-controversial. $)
wi $a wff ( ph -> ps ) $.
wn $a wff -. ph $.
ax-1 $a |- ( ph -> ( ps -> ph ) ) $.
ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $.
ax-3 $a |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) $.
${
ax-mp.1 $e |- ( ph -> ps ) $.
ax-mp.2 $e |- ph $.
ax-mp $a |- ps $.
$}
wal $a wff A. x ph $. $( forall is a wff if x is a variable and ph is a wff
$)
$( A and B denote terms. Since there are no function symbols,
this is a bit silly since terms are the same as variables, but this is how
FOL does it and it makes it clearer how to extend the language, so
let's stick with the distinction. $)
$v A $. tA $f term A $.
$v B $. tB $f term B $.
$v C $. tC $f term C $.
$v D $. tD $f term D $.
$v E $. tE $f term E $.
tv $a term x $. $( A variable is a term. $)
$( We will use the judgments
substT B ( x / A ) = C
subst ph ( x / A ) = ps
to denote that the substitution is admissible, and the result of
substituting x
for A in ph is ps. Almost all the notation here is superfluous; the real
content
is the typecodes substT and subst that indicate the new judgments. In
particular,
despite the use of an equality sign, this defines no relation called
equality,
indeed no new wffs at all, just a new judgment. In a more traditional
database we
would probably define these as new wffs, so that we could write |- B ( x
/ A ) = C
instead, but I want to keep everything clean and separate here, so that
we get
"exactly traditional first-order logic without equality in Metamath". $)
$( Metamath doesn't require that you declare these in advance, so there is
nothing
to write here. $)
$( Substitution on terms is trivial: $)
sbcv1 $a substT x ( x / A ) = A $. $( substitution when the variable
matches $)
${
$d x y $.
$( substitution when the variable doesn't match $)
sbcv $a substT y ( x / A ) = y $.
$}
${
$( Substitution into a negation $)
sbn.1 $a subst ph ( x / A ) = ps $.
sbn $a subst -. ph ( x / A ) = -. ps $.
$}
${
$( Substitution into an implication $)
sbim.1 $a subst ph ( x / A ) = ch $.
sbim.2 $a subst ps ( x / A ) = th $.
sbim $a subst ( ph -> ps ) ( x / A ) = ( ch -> th ) $.
$}
$( Substitution into a forall that binds the variable. $)
sbal1 $a subst A. x ph ( x / A ) = A. x ph $.
${
$d x y $. $d y A $.
$( Substitution into a forall that doesn't bind the variable.
For the substitution to be admissible, A must not contain
any occurrences of y, that is, they are disjoint variables. $)
sbal.1 $e subst ph ( x / A ) = ps $.
sbal $a subst A. y ph ( x / A ) = A. y ps $.
$}
$( Similarly, we need to define the judgment x e/ free(ph), that is,
x is not a free variable in ph. You might wonder why we are negating
the judgment here, and the reason is because it has a natural inductive
characterization, and also this is the polarity we actually need for
axiom L12. We notate it by F/ x ph by analogy to set.mm, but again,
this is not a wff, so it does not enlarge the collection of wffs with
these auxiliary meta-predicates.
We could declare not-free for terms as well, but in FOL terms never have
binders in them, so not-free and disjoint coincide. Therefore we can
save some trouble and use $d instead. $)
${
$( Not free for a negation $)
nfn.1 $e F/ x ph $.
nfn $a F/ x -. ph $.
$}
${
$( Not free for an implication $)
nfim.1 $e F/ x ph $.
nfim.2 $e F/ x ps $.
nfim $a F/ x ( ph -> ps ) $.
$}
$( Not free for a forall when the variables match $)
nfal1 $a F/ x A. x ph $.
${
$d x y $.
$( Not free for a forall when the variables don't match $)
nfal.1 $e F/ x ph $.
nfal $a F/ x A. y ph $.
$}
${
$( Axiom L10: A. x ph(x) -> ph(x/A), if ph(x/A) is admissible. $)
ax-L10.1 $e subst ph ( x / A ) = ps $.
ax-L10 $a |- ( A. x ph -> ps ) $.
$}
${
$( Axiom L12: A. x (ps -> ph(x)) -> (ps -> A. x ph(x)), if x is not free
in ps $)
ax-L12.1 $e F/ x ps $.
ax-L12 $a |- ( A. x ( ps -> ph ) -> ( ps -> A. x ph ) ) $.
$}
$( We're done! Let's show how to add a relation symbol and a function
symbol to this: $)
$c R , $.
$( The relation R(A, B) applied to two terms is a wff.
This is using a lot of superfluous notation; A R B or R A B would both
work as well. $)
wr $a wff R ( A , B ) $.
${
$d x A $. $d x B $.
$( The inductive definition for NF needs a new case for R. Note that we
wouldn't
normally need this theorem, if we had the equivalent of ax-16, but
again I'm
sticking to the classical rules, not the admissible extensions to that
that are natural for Metamath. $)
nfr $a F/ x R ( A , B ) $.
$}
${
$( The inductive definition for substitution also needs a new case. $)
sbr.1 $e substT B ( x / A ) = D $.
sbr.2 $e substT C ( x / A ) = E $.
sbr $a subst R ( B , C ) ( x / A ) = R ( D , E ) $.
$}
$c f $.
$( The expression f(A) is a term if A is. $)
tf $a wff f ( A ) $.
$( NF doesn't need a new case because this is a term and $d can handle NF
for terms. $)
${
$( Substitution into f(B). $)
sbf.1 $e substT B ( x / A ) = C $.
sbf $a substT f ( B ) ( x / A ) = R ( C ) $.
$}
Mario
--
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/CAFXXJSvRROXpMP%2BegAgY8XggiasWwf-WgDm5SqrvdsAbL0XwZA%40mail.gmail.com.
