-
Notifications
You must be signed in to change notification settings - Fork 88
/
mmfrege.raw.html
605 lines (525 loc) · 23.1 KB
/
mmfrege.raw.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
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"https://www.w3.org/TR/html4/loose.dtd">
<!-- The file mmfrege.html is generated from mmfrege.raw.html -
see the regen-from-raw script for details -->
<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=UTF-8">
<TITLE>Frege Notation - Metamath Proof Explorer</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
<STYLE TYPE="text/css">
<!--
/* Math symbol image will be shifted down 4 pixels to align with normal
text for compatibility with various browsers. The old ALIGN=TOP for
math symbol images did not align in all browsers and should be deleted.
All other images must override this shift with STYLE="margin-bottom:0px".
(2-Oct-2015 nm) */
img { margin-bottom: -4px }
-->
</STYLE>
</HEAD>
<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%">
<TR>
<TD ALIGN=LEFT VALIGN=TOP><A HREF="mmset.html"><IMG SRC="mm.gif"
BORDER=0
ALT="Metamath Proof Explorer Home"
TITLE="Metamath Proof Explorer Home"
HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A>
</TD>
<TD ALIGN=CENTER VALIGN=TOP><FONT SIZE="+3"
COLOR="#006633"><B>Metamath Proof Explorer</B></FONT><BR>
<FONT SIZE="+2" COLOR="#006633"><B>Frege Notation</B>
</FONT>
</TD>
<TD NOWRAP ALIGN=RIGHT VALIGN=TOP>
</TD>
</TR>
<TR>
<TD COLSPAN=3 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif>
<A HREF="../mm.html">Mirrors</A> >
<A HREF="../index.html">Home</A> >
<A HREF="mmset.html">MPE Home</A> >
Frege Notation
</FONT>
</TD>
</TR>
</TABLE>
<!--
<CENTER><FONT SIZE="+2" COLOR="#006633"><B>ZFC Axioms Without Distinct
Variable Conditions</B></FONT></CENTER>
-->
<HR NOSHADE SIZE=1>
<B><FONT COLOR="#006633">Frege Notation and
Metamath</FONT></B> While Frege, in his 1879 work
<I>Begriffsschrift</I>, dealt with a calculus of concepts and ideas,
the paradoxes of naive set theory require a translation to separate
statements on logical propositions from those on classes so that
the correct notation is used for each. And when quantifiers are
used, we must quantify over set variables which consequently means
for substitution into such terms, we must require any class to be
a set by means of an explicit hypothesis to preserve the correlation
between Frege and the translation.
<P>Frege used Greek letters to stand for concrete propositions,
propositional formulae with one or more indeterminate slots (which
he called functions), and concepts similar to our classes and
relations; Latin letters to serve as placeholders within the scope
of a judgment similar to the metavariables in the axiom schema of
Metamath; and introduced Fraktur (German blackletter) for the
variables introduced by quantifiers. In 1910, Frege wrote to Philip
Jourdain that these conventions were not a barrier to substitution
but more of an aid to exposition.
<P>In the following, parenthesized expressions like
𝐹 (𝑥) and 𝑓 (𝑥, 𝑦)
have no fixed meaning in the notation, but are placeholders for
indeterminate propositions where terms 𝑥 (and 𝑦)
may appear. If we interpret 𝑥 and 𝑦 as sets, then
𝐹 (𝑥) may be interpreted as membership in a
class while 𝑓 (𝑥, 𝑦) may be interpreted
as membership in a relation. Alternately, they may be interpreted
as placeholders for an arbitrary proposition following proper
substitution for the symbols 𝑥 and 𝑦.
<P><CENTER>
<TABLE BORDER=0 CELLSPACING=0 STYLE="max-width:90%"><TR><TD>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Guide to Frege Notation">
<CAPTION><B>Guide to Frege Notation</B></CAPTION>
<COLGROUP>
<COL STYLE="width: 10em; max-width: 25em">
<COL STYLE="width: 110px">
<COL STYLE="width: 14em">
<COL STYLE="width: 15em; max-width: 25em">
</COLGROUP>
<THEAD>
<TR><TH WIDTH="10em">Statement
</TH><TH WIDTH="110px">Frege
</TH><TH WIDTH="14em">Metamath</TH><TH WIDTH="15em">Notes</TH></TR>
</THEAD>
<TBODY>
<TR ALIGN=LEFT><TD>The proposition, an idea which may be judged
true or false, 𝛢.</TD>
<TD><IMG SRC="_frege_A.svg" WIDTH="80" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top" ALT="Alpha"></TD>
<TD> ` ph `
<BR> ` A ` </TD>
<TD ROWSPAN=4> 𝛢 maps to proposition ` ph ` or class ` A ` .
<BR> ` _V ` is the universal class of all sets.
<BR> ` (/) ` is the empty class.
<BR> Direct translation of a judgment into class notation requires
both the introduction of a dummy set variable and an assertion that
it has no unbound appearance in the class expression. Colloquially,
this is equivalent to saying it is equal to the class of all
sets.</TD></TR>
<TR ALIGN=LEFT><TD>Proposition 𝛢 holds true.</TD>
<TD><IMG SRC="_frege_jA.svg" WIDTH="80" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top" ALT="Judgment Alpha"></TD>
<TD> ` |- ph `
<BR> ` |- ( F/_ x A /\ A. x x e. A ) `
<BR> ` |- A = _V ` </TD></TR>
<TR ALIGN=LEFT><TD>The negation of proposition 𝛢.</TD>
<TD><IMG SRC="_frege_nA.svg" WIDTH="80" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top" ALT="negated Alpha"></TD>
<TD> ` -. ph `
<BR> ` ( _V \ A ) ` </TD></TR>
<TR ALIGN=LEFT><TD>Proposition 𝛢 holds false.</TD>
<TD><IMG SRC="_frege_jnA.svg" WIDTH="80" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negated Alpha"></TD>
<TD> ` |- -. ph `
<BR> ` |- ( _V \ A ) = _V `
<BR> ` |- A = (/) `
</TD></TR>
<TR ALIGN=LEFT><TD>The idea that 𝛣 implies 𝛢.</TD>
<TD><IMG SRC="_frege_BimA.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top" ALT="Beta implies Alpha"></TD>
<TD> ` ( ph -> ps ) `
<BR> ` ( ( _V \ B ) u. A ) ` </TD>
<TD ROWSPAN="10"> 𝛣 maps to ` ph ` or ` B ` .
<BR>𝛢 maps to ` ps ` or ` A ` .
<BR> Since Metamath's standard set.mm has more connectives for
propositions than just implication and negation, some of these
statements have fully equivalent synonyms. </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that the truth of 𝛣 implies
the truth of 𝛢.</TD>
<TD><IMG SRC="_frege_jBimA.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment Beta implies Alpha"></TD>
<TD> ` |- ( ph -> ps ) `
<BR> ` |- ( ( _V \ B ) u. A ) = _V `
<BR> ` |- B C_ A ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that not both 𝛣 and 𝛢
hold true.</TD>
<TD><IMG SRC="_frege_jBimnA.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment Beta implies negated Alpha"></TD>
<TD> ` |- ( ph -> -. ps ) `
<BR> ` |- ( ph -/\ ps ) `
<BR> ` |- ( ( _V \ B ) u. ( _V \ A ) ) = _V `
<BR> ` |- ( _V \ ( B i^i A ) ) = _V `
<BR> ` |- ( B i^i A ) = (/) `
<BR> ` |- B C_ ( _V \ A ) ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that 𝛣 or 𝛢 (or
both) holds true.</TD>
<TD><IMG SRC="_frege_jBorA.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negated Beta implies Alpha"></TD>
<TD> ` |- ( -. ph -> ps ) `
<BR> ` |- ( ph \/ ps ) `
<BR> ` |- ( B u. A ) = _V `
<BR> ` |- ( _V \ B ) C_ A ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that both 𝛣 and 𝛢
hold true.</TD>
<TD><IMG SRC="_frege_jBandA.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negation of Beta implies negated Alpha"></TD>
<TD> ` |- -. ( ph -> -. ps ) `
<BR> ` |- -. ( ph -/\ ps ) `
<BR> ` |- ( ph /\ ps ) `
<BR> ` |- ( _V \ ( ( _V \ B ) u. ( _V \ A ) ) ) = _V `
<BR> ` |- ( _V \ ( _V \ ( B i^i A ) ) ) = _V `
<BR> ` |- ( B i^i A ) = _V ` </TD></TR>
<TR ALIGN=LEFT><TD ROWSPAN="2">The judgment that exactly one of
𝛣 and 𝛢 holds true.</TD>
<TD><IMG SRC="_frege_jBxor1A.svg" WIDTH="104" HEIGHT="92"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment that both negated Beta implies Alpha and Beta implies
negated Alpha"></TD>
<TD> ` |- -. ( ( -. ph -> ps ) -> -. ( ph -> -. ps ) ) `
<BR> ` |- ( ( -. ph -> ps ) /\ ( ph -> -. ps ) ) `
<BR> ` |- ( ph \/_ ps ) `
<BR> ` |- ( ( B u. A ) i^i ( _V \ ( B i^i A ) ) ) = _V `
<BR> ` |- ( _V \ B ) = A ` </TD></TR>
<TR ALIGN=LEFT>
<TD><IMG SRC="_frege_jBxor2A.svg" WIDTH="104" HEIGHT="92"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment that both Beta implies negated Alpha and negated Beta
implies Alpha"></TD>
<TD> ` |- -. ( ( ph -> -. ps ) -> -. ( -. ph -> ps ) ) `
<BR> ` |- ( ( ph -> -. ps ) /\ ( -. ph -> ps ) ) `
<BR> ` |- ( ph \/_ ps ) `
<BR> ` |- ( ( _V \ ( B i^i A ) ) i^i ( B u. A ) ) = _V `
<BR> ` |- B = ( _V \ A ) ` </TD></TR>
<TR ALIGN=LEFT><TD ROWSPAN="2">The judgment 𝛣 is true while
𝛢 is false.</TD>
<TD><IMG SRC="_frege_njBimA.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negation of Beta implies Alpha"></TD>
<TD> ` |- -. ( ph -> ps ) `
<BR> ` |- ( ph /\ -. ps ) `
<BR> ` |- ( _V \ ( ( _V \ B ) u. A ) ) = _V `
<BR> ` |- ( B i^i ( _V \ A ) ) = _V `
<BR> ` |- ( ( _V \ B ) u. A ) = (/) ` </TD></TR>
<TR ALIGN=LEFT>
<TD><IMG SRC="_frege_njnAimnB.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negation of negated Alpha implies negated Beta"></TD>
<TD> ` |- -. ( -. ps -> -. ph ) `
<BR> ` |- ( -. ps /\ ph ) `
<BR> ` |- ( _V \ ( A u. ( _V \ B ) ) ) = _V `
<BR> ` |- ( ( _V \ A ) i^i B ) = _V `
<BR> ` |- ( A u. ( _V \ B ) ) = (/) ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that neither 𝛢 nor 𝛣
is true.</TD>
<TD><IMG SRC="_frege_njnAimB.svg" WIDTH="80" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negation of negated Alpha implies Beta"></TD>
<TD> ` |- -. ( -. ps -> ph ) `
<BR> ` |- -. ( ps \/ ph ) `
<BR> ` |- ( _V \ ( A u. B ) ) = _V `
<BR> ` |- ( A u. B ) = (/) ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that the truth of both 𝛤
and 𝛣 implies the truth of 𝛢.</TD>
<TD><IMG SRC="_frege_jGandBimA.svg" WIDTH="104" HEIGHT="72"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment Gamma and Beta together imply Alpha"></TD>
<TD> ` |- ( ph -> ( ps -> ch ) ) `
<BR> ` |- ( ( ph /\ ps ) -> ch ) `
<BR> ` |- ( ( _V \ C ) u. ( ( _V \ B ) u. A ) ) = _V `
<BR> ` |- ( ( ( _V \ C ) u. ( _V \ B ) ) u. A ) = _V `
<BR> ` |- ( ( _V \ ( C i^i B ) ) u. A ) = _V `
<BR> ` |- ( C i^i B ) C_ A ` </TD>
<TD ROWSPAN=3> 𝛤 maps to ` ph ` or ` C ` .
<BR>𝛣 maps to ` ps ` or ` B ` .
<BR>𝛢 maps to ` ch ` or ` A ` .
<BR> Since Metamath's standard set.mm has more connectives for
propositions than just implication and negation, some of these
statements have fully equivalent synonyms. </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that 𝛤, 𝛣, or
𝛢 (or any combination) holds true.</TD>
<TD><IMG SRC="_frege_jnGandnBimA.svg" WIDTH="104" HEIGHT="72"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negated Gamma and negated Beta together imply Alpha"></TD>
<TD> ` |- ( -. ph -> ( -. ps -> ch ) ) `
<BR> ` |- ( ( -. ph /\ -. ps ) -> ch ) `
<BR> ` |- ( ph \/ ps \/ ch ) `
<BR> ` |- ( C u. ( B u. A ) ) = _V `
<BR> ` |- ( ( C u. B ) u. A ) = _V `
<BR> ` |- ( _V / ( C u. B ) ) C_ A ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that 𝛤, 𝛣, and
𝛢 all hold true.</TD>
<TD><IMG SRC="_frege_jGandBandA.svg" WIDTH="104" HEIGHT="72"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negation of Gamma and Beta together imply negated Alpha"></TD>
<TD> ` |- -. ( ph -> ( ps -> -. ch ) ) `
<BR> ` |- -. ( ( ph /\ ps ) -> -. ch ) `
<BR> ` |- ( ph /\ ps /\ ch ) `
<BR> ` |- ( _V \ ( ( _V \ C ) u. ( ( _V \ B ) u. ( _V \ A ) ) ) ) = _V `
<BR> ` |- ( C i^i ( B i^i A ) ) = _V `
<BR> ` |- ( ( C i^i B ) i^i A ) = _V ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that 𝛢 is equivalent to 𝛣.</TD>
<TD><IMG SRC="_frege_jAeqB.svg" WIDTH="118" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment Alpha is equivalent to Beta"></TD>
<TD> ` |- ( ps <-> ph ) `
<BR> ` |- { x | ps } = { x | ph } `
<BR> ` |- { <. x , y >. | ps } = { <. x , y >. | ph } `
<BR> ` |- ( ( ( _V \ A ) u. B ) i^i ( ( _V \ B ) u. A ) ) = _V `
<BR> ` |- ( ( _V \ ( A u. B ) ) u. ( A i^i B ) ) = _V `
<BR> ` |- ( A u. B ) C_ ( A i^i B ) `
<BR> ` |- A = B ` </TD>
<TD> Fundamentally equality of classes can be distinguished from
logical equivalence, the equality of propositions, since classes are equal
if and only if they contain the same sets and not every class is a set. So
we have ` |- -. ( _om C_ X <-> ( _om C_ X /\ X e. _V ) ) ` but
` |- { x | _om C_ x } = { x | ( _om C_ x /\ x e. _V ) } ` . Thus
the assumption of naive set theory is where Frege must break down.
Intermediate between the two is when the strong condition of
bi-implication implies the weaker equality of classes or relations
composed of sets which satisfy those propositions. With some
adaptation much can be salvaged by a forgiving translation.
<BR> 𝛢 maps to ` ps ` or ` A ` .
<BR>𝛣 maps to ` ph ` or ` B ` </TD></TR>
<TR ALIGN=LEFT><TD>The judgment that 𝛢 has the property
𝛷. (Which implies 𝛢 is a set.)</TD>
<TD><IMG SRC="_frege_jAinP.svg" WIDTH="118" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment Alpha has property Phi"></TD>
<TD> ` |- [. A / x ]. ph `
<BR> ` |- A e. P `
<BR> ` |- A e. { x | ph } ` </TD>
<TD ROWSPAN="4"> 𝛢 maps to ` A ` .
<BR>𝛣 maps to ` B ` .
<BR>𝛷 maps to ` ph ` or ` P ` or ` { x | ph } ` .
<BR>𝛹 maps to ` ps ` or ` R ` or ` { <. x , y >. | ps } ` .
<BR>𝔞 maps to ` a ` .
<BR> ` x ` and ` y ` are distinct set variables which presumably,
but not necessarily, appear in what is eventually substituted for
` ph ` or ` ps ` and which nowhere appear in ` A ` or ` B ` .</TD></TR>
<TR ALIGN=LEFT><TD>The judgment that 𝛣 stands in relation
𝛹 to 𝛢. (Which implies that 𝛢 and 𝛣
are sets.) </TD>
<TD><IMG SRC="_frege_jABinS.svg" WIDTH="118" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment Psi relates Alpha and Beta"></TD>
<TD> ` |- [. A / x ]. [. B / y ]. ps `
<BR> ` |- [. B / y ]. [. A / x ]. ps `
<BR> ` |- A R B `
<BR> ` |- B ``' R A `
<BR> ` |- A { <. x , y >. | ps } B `
<BR> ` |- A ``' { <. y , x >. | ps } B `
<BR> ` |- B { <. y , x >. | ps } A `
<BR> ` |- B ``' { <. x , y >. | ps } A `
<BR> ` |- B e. ( R " { A } ) `
<BR> ` |- A e. ( ``' R " { B } ) `
<BR> ` |- B e. ( { <. x , y >. | ps } " { A } ) `
<BR> ` |- B e. ( ``' { <. y , x >. | ps } " { A } ) `
<BR> ` |- A e. ( ``' { <. x , y >. | ps } " { B } ) `
<BR> ` |- A e. ( { <. y , x >. | ps } " { B } ) `
</TD></TR>
<TR ALIGN=LEFT><TD>The judgment that all 𝔞 have the property
𝛷.</TD>
<TD><IMG SRC="_frege_jalAinP.svg" WIDTH="118" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment all a have property Phi"></TD>
<TD> ` |- A. a [ a / x ] ph `
<BR> ` |- A. a a e. P `
<BR> ` |- A. a a e. { x | ph } ` </TD></TR>
<TR ALIGN=LEFT><TD>The negated judgment that no 𝔞 have the
property 𝛷.</TD>
<TD><IMG SRC="_frege_jexAinP.svg" WIDTH="118" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Judgment negation of all a do not have property Phi"></TD>
<TD> ` |- -. A. a -. [ a / x ] ph `
<BR> ` |- E. a [ a / x ] ph `
<BR> ` |- -. A. a -. a e. P `
<BR> ` |- E. a a e. P ` </TD></TR>
</TBODY>
</TABLE>
</TD></TR><TR><TD ALIGN=LEFT>
<FONT SIZE=-2 FACE=ARIAL>Colors of variables:
<FONT COLOR="#0000FF">wff</FONT> <FONT COLOR="#FF0000">set</FONT> <FONT
COLOR="#CC33CC">class</FONT></FONT>
</TD></TR></TABLE>
</CENTER>
<P><B><FONT COLOR="#006633">Additional
Notation</FONT></B> Having laid the foundations
of notation for propositions and classes that are sometimes required
to be sets, Frege invents additional notation to introduce definitions
and proceeds to define new arrangements of symbols.
Unlike left-to-right notation like ` x R y ` , Frege does not
privilege the ordering of the slots in a two-slot meta-notation
like 𝑓 (δ, α) as having fixed meaning
regarding the natural ordering such a relation indicates. Instead
Frege indicated the intended ordering of the slots with lowercase
Greek letters. Instead of having separate notation for the converse
of a relation, Frege would reverse the ordering of the lowercase
Greek letters relative to the vertically oriented marker which
introduces them.
<P><CENTER>
<TABLE BORDER=0 CELLSPACING=0 STYLE="max-width:90%"><TR><TD>
<TABLE BORDER CELLSPACING=0 BGCOLOR="#EEFFFA"
SUMMARY="Additional Frege Notation">
<CAPTION><B>Additional Frege Notation</B></CAPTION>
<COLGROUP>
<COL STYLE="width: 10em; max-width: 25em">
<COL STYLE="width: 110px">
<COL STYLE="width: 14em">
<COL STYLE="width: 15em; max-width: 25em">
</COLGROUP>
<THEAD>
<TR><TH WIDTH="10em">Statement
</TH><TH WIDTH="110px">Frege
</TH><TH WIDTH="14em">Metamath</TH><TH WIDTH="15em">Notes</TH></TR>
</THEAD>
<TBODY>
<TR ALIGN=LEFT><TD>Introducing a definition.</TD>
<TD><IMG SRC="_frege_dfAeqB.svg" WIDTH="88" HEIGHT="32"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Defintion: Alpha equivalent to Beta"></TD>
<TD> ` |- ( ph <-> ps ) `
<BR> ` |- A = B ` </TD>
<TD> 𝛢 maps to ` ph ` or ` A ` .
<BR> 𝛣 maps to ` ps ` or ` B ` .
<BR> While newly defined terms are introduced on the right by Frege,
set.mm follows the convention that newly defined terms appear on
the left with an expression in known symbols on the right.
<BR> This judgment is a definition in Metamath only if it is the
content of an <TT>$a</TT> statement as Metamath doesn't distinguish
between definitions and axioms. </TD></TR>
<TR ALIGN=LEFT><TD>The proposition that membership in class 𝐹
(a proposition schema with one slot) is hereditary in the sequence
generated by relation 𝑓 (which takes two slots where order
is distinguishable). </TD>
<TD><IMG SRC="_frege_fheF.svg" WIDTH="86" HEIGHT="72"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="F is hereditary in the f-sequence"></TD>
<TD> ` R hereditary A `
<BR> ` ( R " A ) C_ A `
<BR> ` A. x A. y ( ( x e. A /\ x R y ) -> y e. A ) ` </TD>
<TD ROWSPAN=2> 𝑓 maps to ` R ` .
<BR> 𝐹 maps to ` A ` .
<BR> α and δ are newly-introduced placeholders which do
not appear in any expression similar the the distinct bound variables
` x ` and ` y ` , provided that they don't appear in ` A ` or ` R
` .
<BR> The ` hereditary ` connective was introduced while translating
Frege to avoid the need to duplicate arbitrarily long expressions
for ` A ` .</TD></TR>
<TR ALIGN=LEFT><TD>The proposition that membership in class 𝐹
(a proposition schema with one slot) is hereditary in the sequence
generated by converse of the relation 𝑓. </TD>
<TD><IMG SRC="_frege_cfheF.svg" WIDTH="86" HEIGHT="72"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="F is hereditary in the converse of the f-sequence"></TD>
<TD> ` ``' R hereditary A `
<BR> ` ( ``' R " A ) C_ A `
<BR> ` A. x A. y ( ( x e. A /\ y R x ) -> y e. A ) ` </TD></TR>
<TR ALIGN=LEFT><TD> 𝑦 follows 𝑥 in the 𝑓-sequence </TD>
<TD><IMG SRC="_frege_yfollowsx.svg" WIDTH="86" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Definition: y follows x in the f-sequence"></TD>
<TD> ` Y e. |^| { p | ( R " ( p u. { X } ) ) C_ p } `
<BR> ` X ( t+ `` ``' ``' R ) Y ` </TD>
<TD ROWSPAN="4"> 𝑥 maps to ` X ` .
<BR> 𝑦 maps to ` Y ` .
<BR> 𝑓 maps to ` R ` .
<BR> ` p ` is a bound set variable, distinct from ` X ` , ` Y ` and
` R ` . Because ` p ` is a set variable, so the image of a set
under ` R ` (or ` ``' R ` ) must be a set. For the abbreviations,
we require the stronger condition that the relational content of ` R `
must be a set.
<BR> ` t+ ` maps to the transitive closure of a relation, while ` t* `
maps to the reflexive-transitive closure of a relation.
<BR> ` _I ` is the identity function which has a wider domain than
the reflexive-transitive closure of a relation.
<BR> Once again the lowercase Greek letters have no meaning but to
order the two slots of the relation, but now they are subscripts
of the concrete variables 𝑥 and 𝑦 which need not
be distinct.
<BR> This statement cannot be true unless both ` X ` and ` Y ` are
sets. </TD></TR>
<TR ALIGN=LEFT><TD> 𝑦 precedes 𝑥 in the 𝑓-sequence
</TD>
<TD><IMG SRC="_frege_yprecedsx.svg" WIDTH="86" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Definition: y precedes x in the f-sequence"></TD>
<TD> ` Y e. |^| { p | ( ``' R " ( p u. { X } ) ) C_ p } `
<BR> ` X ( t+ `` ``' R ) Y ` </TD></TR>
<TR ALIGN=LEFT><TD> 𝑦 belongs to the 𝑓-sequence
beginning with 𝑥</TD>
<TD><IMG SRC="_frege_yinfbegx.svg" WIDTH="86" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Definition: y belongs to the f-sequence beginning with x"></TD>
<TD> ` Y e. |^| { p | ( ( R u. _I ) " ( p u. { X } ) ) C_ p } `
<BR> ` X ( ( t+ `` ``' ``' R ) u. _I ) Y `
<BR> ` X ( ( t* `` ``' ``' R ) u. _I ) Y ` </TD></TR>
<TR ALIGN=LEFT><TD> 𝑦 belongs to the 𝑓-sequence
ending with 𝑥</TD>
<TD><IMG SRC="_frege_yinfendx.svg" WIDTH="86" HEIGHT="52"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="Definition: y belongs to the f-sequence ending with x"></TD>
<TD> ` Y e. |^| { p | ( ( ``' R u. _I ) " ( p u. { X } ) ) C_ p } `
<BR> ` X ( ( t+ `` ``' R ) u. _I ) Y `
<BR> ` X ( ( t* `` ``' R ) u. _I ) Y ` </TD></TR>
<TR ALIGN=LEFT><TD> 𝑓 is single-valued in the forward direction</TD>
<TD><IMG SRC="_frege_funf.svg" WIDTH="72" HEIGHT="64"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="f is a function"></TD>
<TD> ` A. x A. y A. z ( ( x R y /\ x R z ) -> y = z ) `
<BR> ` Fun ``' ``' R ` </TD>
<TD ROWSPAN="2"> 𝑓 maps to ` R ` . </TD></TR>
<TR ALIGN=LEFT><TD> 𝑓 is single-valued in the reverse direction </TD>
<TD><IMG SRC="_frege_funcf.svg" WIDTH="72" HEIGHT="64"
STYLE="margin-bottom:0px; vertical-align: top"
ALT="The converse of f is a function"></TD>
<TD> ` A. x A. y A. z ( ( y R x /\ z R x ) -> y = z ) `
<BR> ` Fun ``' R ` </TD></TR>
</TBODY>
</TABLE>
</TD></TR><TR><TD ALIGN=LEFT>
<FONT SIZE=-2 FACE=ARIAL>Colors of variables:
<FONT COLOR="#0000FF">wff</FONT> <FONT COLOR="#FF0000">set</FONT> <FONT
COLOR="#CC33CC">class</FONT></FONT>
</TD></TR></TABLE>
</CENTER>
<P><B><FONT COLOR="#006633">Section</FONT></B>
More text here.
<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 09-Nov-2020.</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="https://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>