-
Notifications
You must be signed in to change notification settings - Fork 9
/
award2003.html
547 lines (448 loc) · 22.2 KB
/
award2003.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<HTML LANG="EN-US">
<HEAD>
<!-- improve mobile display -->
<META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0">
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<TITLE>AWARD-2003 Workshop Miscellany</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
<!--
<meta HTTP-EQUIV="REFRESH"
CONTENT="0; URL=award2003.html">
-->
</HEAD>
<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">
<CENTER>
<H1>Workshop Miscellany</H1>
<P> Norm Megill<BR> <FONT COLOR=BLUE>nm at alum dot mit dot edu</FONT>
</CENTER>
About this page: This page was originally created as part of a
presentation at the 2003 Argonne Workshop on Automated Reasoning and
Deduction (AWARD2003), and more material has been added over time. Items 2
through 17 each present one or more open problems (which in some cases
have been solved, as noted).
<UL>
<LI>Updated 11-Apr-2018 - Benoît Jubin solved the problem of
<A HREF="#14">item 14</A>, showing the "Axiom of Twoness" is needed
for completeness of the ZFC axioms without distinct variables.
<LI>Updated 30-Dec-2007 - Added <A HREF="#9b">item 9b</A>.
<LI>Updated 21-May-2007 - Eric Schmidt found two redundant axioms in the
list of axioms for complex numbers (see <A HREF="#11">item 11</A>).
<LI>Updated 26-Jul-2006 - Added <A HREF="#17">item 17</A>.
<LI>Updated 21-Jan-2006 - Juha Arpiainen solved the problem of <A
HREF="#9a">item 9a</A>, proving the independence of axiom ax-11. See
also <A HREF="#9">item 9</A>.
<LI>15-Aug-2005 - My 2005 talks were <A
HREF="downloads/megillaward2005he.pdf"> "Emulating Hilbert's Epsilon in
ZFC"</A> (PDF slide show) (<A HREF="latex/megillaward2005he.tex">LaTeX
source file</A>) and <A HREF="downloads/megillaward2005eu.pdf">
"Existential Uniqueness"</A> (PDF slide show) (<A
HREF="latex/megillaward2005eu.tex">LaTeX source file</A>).
<LI>Updated 12-Apr-2005 - Raph Levien solved the problem of <A
HREF="#16">item 16</A>, answering it in the negative. See also <A
HREF="#9">item 9</A>.
<LI>Updated 19-Feb-2005 - N. Megill found a redundant axiom in the list of
axioms for complex numbers (see <A HREF="#11">item 11</A>).
<LI>Updated 26-Jun-2004 - expanded the comment under <A HREF="#13">item
13</A>.
<LI>5-Aug-2004 - My 2004 talk was <A HREF="downloads/megillaward2004.pdf">
"Hilbert Lattice Equations"</A> (PDF slide show) (<A
HREF="latex/megillaward2004.tex">LaTeX source file</A>).
<LI>Updated 6-May-2004 - Kurt Maes found an <A
HREF="mpeuni/ackm.html">impressive new version</A> of the Axiom of
Choice (see <A HREF="#8">item 8</A>).
<LI>Updated 4-May-2004 - Greg Bush has found shorter proofs for 67 of the
193 propositional calculus theorems in Principia Mathematica (<A
HREF="#4">item 4</A>). See this <A
HREF="mmsolitaire/mms.html#shortest">note</A>.
<LI>As of 31-Jan-2004, all problems on this page are still open.
<LI>Updated 1-Jan-2004 - added <A HREF="#16">item 16</A>.
<LI>Updated 10-Aug-2003 - added <A HREF="#9a">item 9a</A>.
<LI>Updated 18-Jul-2003 - added <A HREF="#15">item 15</A> (regarding the
$100 prize problem).
</UL>
<CENTER><BLOCKQUOTE>This page was part of an informal talk I gave at the
AWARD-2003 Workshop on Jul. 12, 2003. My other (main) talk was <A
HREF="downloads/megillaward2003.pdf">
"Orthomodular Lattices and Beyond"</A> (PDF slide show) given on Jul.
11. (To make the slide show, I used the command "pdflatex <A
HREF="latex/megillaward2003.tex">megillaward2003.tex</A>".)</BLOCKQUOTE></CENTER>
<P>Back to the <A HREF="http://www.mcs.anl.gov/research/projects/AR/award-2003/">AWARD-2003
Workshop</A> page.<BR>
And the <A HREF="http://www.mcs.anl.gov/research/projects/AR/award-2004/">AWARD-2004
Workshop</A> page.<BR>
<!--
And the <A HREF="http://www-unix.mcs.anl.gov/AR/award-2005/">AWARD-2005
-->
And the <A HREF="http://www.mcs.anl.gov/research/projects/AR/award-2005/">AWARD-2005
Workshop</A> page.
<P>These are a few miscellaneous things
you can explore at your leisure.
<P>
<P><BR><A NAME="1"></A><B>1.</B> (deleted)
<!--
Quick overview of <A
HREF="http://us.metamath.org/index.html">Metamath</A> web site. If this
page is down, select another <A
HREF="http://metamath.org/index.html">mirror site</A>.
-->
<!-- Readable in a <A
HREF="mpeuni/mmset.html#textonly">text
browser</A>. Metamath proof language <A
HREF="screen1.html">snapshot</A> and
corresponding <A HREF="mpeuni/df-eu.html">web
page</A> display. The 4-page <A
HREF="index.html#language">language
specification</A>. How <A
HREF="mpeuni/mmset.html#proofs">proofs</A> work.
A 300-line <A HREF="downloads/mmverify.py">proof
verifier</A> in Python (written by Raph Levien).
-->
<P><A NAME="2"></A><B>2.</B> Open problem: Does a single
axiom (e.g. Sheffer-stroke) exist for
<A HREF="qlegif/mmql.html#weak">weakly
orthomodular lattices (WOML)</A>?
<P>
What I mean is a single identity added to the usual axioms and rules of
inference for identity (reflexivity, symmetry, transitivity,
substitution). In other words, it would be a single identity which,
together with these axioms, would determine the equational variety WOML
of weakly orthomodular lattices.
<P>It would be exactly analogous to McCune's
<A HREF="http://www.cs.unm.edu/~mccune/papers/olsax/oml-sax.html">Single
Axiom for Orthomodular
Lattices</A> with
"WOML" substituted for "OML". It was this page, in fact, that led me to
wonder about an analogous equation for WOML.
<!-- Related question: will one side
of this single axiom evaluate to 1? (I haven't been able to find
a WOML-law equivalent without this property, so if that is not the
case that would be interesting to me.)
-->
<P><A NAME="3"></A><B>3.</B> <A
HREF="qlegif/kalmbach.txt">Kalmbach's CN
(implication, negation) quantum propositional calculus</A> with modus
ponens as sole rule of inference. Open problems: (1) independence of
axioms; (2) more elegant, shorter axiomatization; (3) is A16 needed for
completeness? (4) is the system D-complete? (5) is there a single
axiom!? Another note on Kalmbach's system is <A
HREF="qlegif/mmql.html#prop">here</A>.
<P><A NAME="4"></A><B>4.</B> Using the standard three <A
HREF="mpeuni/mmset.html#scaxioms">classical
propositional calculus axioms</A>, here are <A
HREF="mmsolitaire/pmproofs.txt">condensed
detachment proofs</A> of the 193 propositional calculus theorems in
Principia Mathematica. Open problem: Are these the shortest proofs?
<I>Update 4-May-2004: Greg Bush has found shorter proofs for 67 of these.
See this <A
HREF="mmsolitaire/mms.html#shortest">note</A>.</I>
<P><A NAME="5"></A><B>5.</B> The 3-variable (weak) <A
HREF="qlegif/mmql.html#strong">orthoarguesian
law</A> ax-3oa can be derived from the modular law
av(b^(avc))=(avb)^(avc) added to an OL. Open problem: can the
standard orthoarguesian law ax-4oa be derived from the modular law + OL?
<P><A NAME="6"></A><B>6.</B> The <I>Arguesian law</I> is the same as the <A
HREF="qlegif/mmql.html#strong">orthoarguesian
law</A> in the form of oa6 with its 3 hypotheses removed. It has been
proved to be strictly stronger than the modular law, and the modular law
can be derived from it. Open(?) problem: does there exist a finite
ortholattice that is modular but non-Arguesian? [This lattice might
also answer the previous question (5)].
<P><A NAME="7"></A><B>7.</B> Open problem: can Godowski's 3-variable
equation (see slide 17 in my <A
HREF="http://www-unix.mcs.anl.gov/~mccune/award-2003/megill.pdf">AWARD-2003
Workshop presentation (PDF)</A>) be derived from OL + modular law? How
about the 4-, 5-,... variable versions? How about the new equation (32)
in slide 17?
<P><A NAME="8"></A><B>8.</B> A <A HREF="mpeuni/ax-ac.html">short
equivalent</A> of the Axiom of Choice. Open problem: Does a shorter
equivalent (expressed in first-order logic primitives) exist? (Here's a
<A HREF="mpeuni/ac2.html">another cute
version</A> using some abbreviations.)
<I>Update 6-May-2004: In April 2004,
Kurt Maes found a version of the Axiom of Choice
that has about the same length. More importantly,
his version has only 5 quantifiers in
prenex normal form, setting a new record.
See this <A
HREF="mpeuni/ackm.html">theorem ackm</A>.</I>
<P><A NAME="9"></A><B>9.</B> <A
HREF="mpeuni/mmset.html#pcaxioms">Metamath's
axiom system</A>. If the apparent willy-nilly mixing of free and
bound variables confuses you,
<A
HREF="mpeuni/mmset.html#axiomnote">read this</A>.
Open problems: (1) Are the axioms for predicate calculus
independent? (2) Can the axiomatization be simplified?
<P><I>Update 12-Apr-2005: Raph Levien proved that ax-9 is independent
from the others; see <A
HREF="#16">item 16</A> below.</I> Now we only have 12 more
(out of 13) independence proofs to go!
<P><I>Update 21-Jan-2006: Juha Arpiainen proved that ax-11 is independent
from the others; see <A
HREF="#9a">item 9a</A> below.</I> Now we only have 11 more
(out of 13) independence proofs to go!
<P><B><A NAME="9a"></A>9a.</B> The open problem stated in Remark 9.5 on
p. 16 (PDF p. 17) of <A HREF="downloads/finiteaxiom.pdf">"A Finitely
Axiomatized Formalization of Predicate Calculus with Equality"</A> is
still open (as of 10-Aug-2003). In terms of <A
HREF="mpeuni/mmset.html#pcaxioms">Metamath's axiom system</A>, the
problem asks whether <A HREF="mpeuni/ax-11.html">ax-11</A> can be proved
from ax-1 through ax-10, ax-12 through ax-15, ax-mp, and ax-gen, and no
others. It should be noted ax-11 is not <I>logically</I> independent,
because any <I>specific</I> instance of ax-11, where phi is replaced
with a subformula containing only set (meta)variables but no wff
(meta)variables, is provable from the others mentioned.
<P><I>Update 21-Jan-2006: Juha Arpiainen <B>solved</B> this problem and proved
that ax-11 is metalogically independent from the others. Hence,
there cannot exist a proof of ax-11 from the others. Here is his
seven-line proof:</I>
<P><CENTER><TABLE BORDER CELLSPACING=0 CELLPADDING=5
BGCOLOR="#F0F0F0"><TR><TD ALIGN=LEFT>
<PRE>
Ax-11 need not hold if there are additional predicates that do not
satisfy the analogues of ax-13 and ax-14. For example, consider the
system with one additional binary predicate "x ~ y". The set of ordered
pairs of integers is then a model of ax-1 to ax-10, ax-12 to ax-17 if
"x = y" and "x e. y" are interpreted as "the first components of x and y
are equal" and "x ~ y" as "the second components are equal". However,
equs5 (and therefore also ax-11) is false for the wff "x ~ y".</PRE>
</TD></TR></TABLE></CENTER>
<P><B><A NAME="9b"></A>9b.</B> An open problem is whether <A
HREF="mpeuni/ax-11o.html">ax-11o</A> can be derived in a predicate
calculus system that omits <A HREF="mpeuni/ax-16.html">ax-16</A> and <A
HREF="mpeuni/ax-17.html">ax-17</A> (but includes <A
HREF="mpeuni/ax-11.html">ax-11</A>). See the 5th table entry in <A
HREF="mpeuni/mmset.html#subsys">Appendix 7: Some Predicate Calculus
Subsystems</A>
<P><A NAME="10"></A><B>10.</B> A <A
HREF="mpeuni/mmdeduction.html#proof">weak
deduction theorem</A> for classical propositional calculus. <A
HREF="mpeuni/mmdeduction.html#quick">Example</A>
of its use. Open problem: In quantum propositional calculus, the
standard deduction theorem fails (and so does this weak deduction
theorem). What kind of "weak" deduction theorems are possible?
<P><A NAME="11"></A><B>11.</B> <A HREF="mpeuni/mmcomplex.html">Axiomatization
for complex numbers</A>. Open problem: are the
axioms independent? (N. Megill reduced the number from 28 to 27
on 19-Feb-2005. Eric Schmidt weakened "1 is real" to "1 is complex"
on 11-Apr-2007. Eric Schmidt reduced the number of axioms from 27
to 25 on 21-May-2007.)
<P><A NAME="12"></A><B>12.</B> Consider the "pure" fragment of Metamath
axiom system, <A HREF="mpeuni/mmset.html#pcaxioms">ax-1 through ax-7
(and ax-mp, ax-gen)</A>. Open problem: Can this fragment directly
prove all such theorem schemes of its kind*, i.e. is it complete for
this fragment? (I think so.) [* No predicate connectives (such as =),
no distinct variable restrictions.] Possible clue (suggested by Bob
Meyer): this fragment seems analogous to modal logic S5 (or monadic
predicate calculus), extended by introducing the second variable y in
ax-7.
<P><A NAME="13"></A><B>13.</B> Set theory can be added to standard first order logic
<I>without</I> equality by making the membership epsilon the only
primitive predicate and introducing equality as a defined symbol. The
usual axioms of equality then become theorems of set theory (see
comments under the <A HREF="mpeuni/ax-ext.html">Axiom of
Extensionality</A>). This provides a system that is quite beautiful
from a minimalist point of view. However, in Metamath's axiom system <A
HREF="mpeuni/mmset.html#pcaxioms">predicate calculus</A> there is no
primitive notion of proper substitution, and additional equality axioms
serve this role (see the definition of <A
HREF="mpeuni/df-sb.html">proper substitution</A> and related theorems).
So dispensing with equality would almost certainly require some
additional axioms with epsilon, beyond Extensionality, to fill the gap.
Problem: What would a "nice" set of epsilon-only axioms look like?
(The existing axioms could be expanded with the definition of equality,
of course, but they would be long and ugly with possible redundancies.)
Philosophical problem: Would these additional axioms be part of set
theory or logic? If they are considered part of logic, in what ways
does such a "minimal" predicate calculus, with a single arbitrary binary
predicate calculus, differ from standard predicate calculus? How much
of proper substitution is "pushed" into set theory, and what is the
character of the non-set-theory part left over?
<P><A NAME="14"></A><B>14.</B> In this odd formalization of <A
HREF="mpeuni/mmzfcnd.html">set theory axioms with
no distinct variable restrictions</A>, is the "Axiom of Twoness" essential
for completeness? (I think so.)
<P><I>Update 11-Apr-2018: Benoît Jubin proved this is the case.</I>
His proof is as follows:
<P><CENTER><TABLE BORDER CELLSPACING=0 CELLPADDING=5
BGCOLOR="#F0F0F0"><TR><TD ALIGN=LEFT>
<PRE>
In a model with a single element which does not contain itself, all
axioms and rules of predicate calculus, all axioms of "ZCF-no$d"
except twoness, and all axioms of standard ZFC except ax-pow and
ax-inf are satisifed. In other words, strip out all quantifiers,
evaluate all "X = Y" to True and all "X \in Y" to False. Then, all
axioms evaluate to True except ax-pow and ax-inf.
Interestingly, the model with a single element containing itself
satisfies all axioms except, of course, ax-reg (and ax-reg-no$d).
What is interesting is that it satisfies ax-inf (and ax-inf-no$d), but
of course it does not satisfy the real infinity axiom ax-inf2. This
proves that ax-reg is necessary in the derivation of
ax-inf2.</PRE></TD></TR></TABLE></CENTER>
<P><A NAME="15"></A><B>15.</B> Stuff related to the OI3 conjecture (slide 22 of PDF file
<A HREF="http://www-unix.mcs.anl.gov/~mccune/award-2003/megill.pdf">
Orthomodular Lattices and Beyond</A>)
[whose solution will earn a $100 prize (slide 23)]:
<OL>
<LI>As a "sanity check" it might be useful to show Otter can prove OI3
from OA3+OML. The proof is relatively simple (for Otter too, I think)
and is shown in Th. 4.10, p. 26, of
<A HREF="http://xxx.lanl.gov/abs/quant-ph/0009038">
http://xxx.lanl.gov/abs/quant-ph/0009038</A>.
<LI> It might be interesting to see which of the known implications on
slide 26 of
<A HREF="http://www-unix.mcs.anl.gov/~mccune/award-2003/megill.pdf">
http://www-unix.mcs.anl.gov/~mccune/award-2003/megill.pdf</A>
that Otter is
able to do. Some are easy, but others seemed tricky (to do by
hand anyway). I can provide the proofs of any of them if desired.
<LI> I would be interested in seeing a proof of (or counterexample to) any
of the open implication directions on slide 26, such as 48+OML => 47 or
45+OML => 49. (If a counterexample is found, that would of course also
disprove the OI3 conjecture and be eligible for the prize.)
<LI> I would also be interested in any <I>combinations</I> of equations in
slide 26 that together might produce others, in directions that are
currently unknown. For example, can OML+46+49+53 prove 44?
<LI> The equations in slide 26 that aren't known OA3 equivalents are 45,
46, 47, 48, 49, 50, 51, and 53. It would be interesting to see if any
equations in this set, or even all of them together, could (when added
to OML) prove the equation of slide 24. (The equation of slide 24
<I>can</I> be derived from OA3+OML.) It would not solve the OI3 conjecture
but might provide further clues.
</OL>
<P><A NAME="16"></A><B>16.</B> (Predicate calculus) In <A
HREF="mpeuni/mmset.html#axiomnote">A Note
on the (Metamath) Axioms</A>, 3rd paragraph,
an open problem is whether
"<img SRC='mpeuni/exists.gif' WIDTH=9 HEIGHT=19 ALT='E.'
ALIGN=TOP><I>x</I><SUB>4</SUB> <I>x</I><SUB>4</SUB> =
<I>x</I><SUB>4</SUB>"
can be proved from
"<img SRC='mpeuni/exists.gif' WIDTH=9 HEIGHT=19 ALT='E.'
ALIGN=TOP><I>x</I><SUB>3</SUB> <I>x</I><SUB>3</SUB> =
<I>x</I><SUB>3</SUB>"
in the absence of ax-9. Or expressed as a Metamath problem:
can
<P>
<CENTER>
<IMG SRC='mpeuni/_vdash.gif' WIDTH=10
HEIGHT=19 ALT='|-' ALIGN=TOP> <IMG SRC='mpeuni/exists.gif' WIDTH=9 HEIGHT=19
ALT='E.' ALIGN=TOP><IMG SRC='mpeuni/_x.gif' WIDTH=10 HEIGHT=19
ALT='x' ALIGN=TOP> <IMG SRC='mpeuni/_x.gif'
WIDTH=10 HEIGHT=19 ALT='x' ALIGN=TOP> <IMG SRC='mpeuni/eq.gif' WIDTH=12 HEIGHT=19
ALT='=' ALIGN=TOP> <IMG SRC='mpeuni/_x.gif'
WIDTH=10 HEIGHT=19 ALT='x' ALIGN=TOP>
<IMG SRC='mpeuni/bigto.gif' WIDTH=15
HEIGHT=19 ALT='=>' ALIGN=TOP>
<IMG SRC='mpeuni/_vdash.gif'
WIDTH=10 HEIGHT=19 ALT='|-' ALIGN=TOP> <IMG SRC='mpeuni/exists.gif' WIDTH=9 HEIGHT=19
ALT='E.' ALIGN=TOP><IMG SRC='mpeuni/_y.gif' WIDTH=9 HEIGHT=19
ALT='y' ALIGN=TOP> <IMG SRC='mpeuni/_y.gif'
WIDTH=9 HEIGHT=19 ALT='y' ALIGN=TOP> <IMG SRC='mpeuni/eq.gif' WIDTH=12 HEIGHT=19
ALT='=' ALIGN=TOP> <IMG SRC='mpeuni/_y.gif'
WIDTH=9 HEIGHT=19 ALT='y' ALIGN=TOP>
</CENTER><P>
be proved without using <A
HREF="mpeuni/ax-9.html">ax-9</A>? This can be expressed
equivalently as the following problem in the Metamath language:
<P><CENTER><TABLE CELLSPACING=0 CELLPADDING=5
BGCOLOR="#F0F0F0"><TR><TD ALIGN=LEFT> <PRE> ${
exeqid.1 $e |- E. x x = x $.
$( Open problem 16 in award2003.html $)
exeqid $p |- E. y y = y $=
? $.
$}</PRE></TD></TR></TABLE></CENTER>
<P><I>Update 12-Apr-2005: Raph Levien proved this is impossible.</I>
His proof is as follows:
<P><CENTER><TABLE BORDER CELLSPACING=0 CELLPADDING=5
BGCOLOR="#F0F0F0"><TR><TD ALIGN=LEFT>
<PRE>
Assume that we have a proof of E. y y = y starting from the hypothesis
E. x x = x. Expand out the proof so that all proof steps are
invocations of axioms 1-8, 10-12, 16-17, mp and gen, and all
metavariables are replaced by actual variables, including x_4 as the
replacement for y.
Now transform all proof steps so that any equality involving x_4
becomes "false", and check whether the resulting proof still holds.
All of the axioms not involving equality should be ok. ax-8 is ok
because in all cases where the consequent becomes false, at least one
of the antecedents also becomes false. ax-10 is ok because if either x
or y is x_4, then the antecedent is false. ax-11 is ok because the
second antecedent is false. ax-12 is trickier, but goes like this: if
z is distinct from x and y, then the consequent follows from ax-17
even if z is x_4. If x or y is x_4, then the third antecedent is
false. Lastly, ax-16 is ok because if x or y is x_4, then A. x x = y
becomes false.
Thus, all transformed proof steps are true when interpreted in
standard axioms. However, the transformed E. x_4 x_4 = x_4 is false,
which is a contradiction.</PRE></TD></TR></TABLE></CENTER>
<P>If you find the "meaning" of x_4 as a bound variable in Raph's proof
is troublesome, notice that all of the axioms and rules of logic (other
than ax-9 itself) hold if you simply strip out the quantifiers. So with
quantifiers stripped out, a purported proof would prove x_4 = x_4 from
x_3 = x_3. Then, using a model where x_4 does not equal anything,
Raph's contradiction follows.
<P>This also shows (as obvious corollaries) that ax-9 is independent
from the others, and also that we need ax-9 to prove x = x.
<P><A NAME="17"></A><B>17.</B> (Predicate calculus with equality) In <A
HREF="mpeuni/mmset.html#tradopn">Appendix 3: Traditional Textbook
Axioms of Predicate Calculus with Equality</A>, last paragraph, an open
problem is whether any or all of axioms <A
HREF="mpeuni/mmset.html#pcaxioms">ax-4 through ax-17</A> can be proved
(directly in Metamath) from the "traditional axioms" expressed as
theorems <A HREF="mpeuni/mmset.html#traditional">stdpc4, stdpc5, ax-gen,
stdpc6, and stdpc7</A>, using <A HREF="mpeuni/dfsb7.html">dfsb7</A> as the
definition for proper substitution. (The reason to choose dfsb7 over <A
HREF="mpeuni/df-sb.html">df-sb</A> is to be as conventional as
possible.) This is interesting because the traditional axioms provide a
<I>logically</I> complete system of predicate calculus that is familiar
to more people. We could separate the axioms for predicate calculus and
equality into two groups, the traditional logically complete set and a
supplemental "technical" set consisting of that subset of ax-4 through
ax-17 (or some variant of them) needed to achieve <I>metalogical</I>
completeness.
<P>
<HR NOSHADE SIZE=1>
<TABLE WIDTH="100%">
<TR>
<TD ALIGN=RIGHT>
<FONT FACE="ARIAL" SIZE=-2> <A
HREF="http://validator.w3.org/check?uri=referer">W3C HTML validation</A>
</FONT>
</TD>
</TR>
</TABLE>
<!-- <SCRIPT SRC="http://www.google-analytics.com/urchin.js" TYPE="text/javascript">
</SCRIPT>
<SCRIPT TYPE="text/javascript">
_uacct = "UA-1862729-1";
urchinTracker();
</SCRIPT>
-->
<HR NOSHADE SIZE=1>
<TABLE BORDER=0 WIDTH="100%"><TR>
<TD ALIGN=left VALIGN=TOP WIDTH="25%"><FONT SIZE=-2 FACE=sans-serif>
</FONT></TD>
<TD NOWRAP ALIGN=CENTER><I>This page was last updated on 11-Apr-2018.</I>
<BR><FONT SIZE=-2 FACE=ARIAL>
Copyright terms:
<A HREF="../copyright.html#pd">Public domain</A>
</FONT></TD>
<TD ALIGN=RIGHT VALIGN=BOTTOM WIDTH="25%">
<FONT FACE="ARIAL" SIZE=-2>
<A
HREF="http://validator.w3.org/check?uri=referer">W3C HTML validation</A>
[external]
</FONT>
</TD>
</TR></TABLE>
<!-- <SCRIPT SRC="http://www.google-analytics.com/urchin.js" TYPE="text/javascript">
</SCRIPT>
<SCRIPT TYPE="text/javascript">
_uacct = "UA-1862729-1";
urchinTracker();
</SCRIPT>
-->
</BODY></HTML>