Metamath Proof Explorer


Table of Contents - 21.38.6. Propositions from _Begriffsschrift_

In 1879, Frege introduced notation for documenting formal reasoning about propositions (and classes) which covered elements of propositional logic, predicate calculus and reasoning about relations. However, due to the pitfalls of naive set theory, adapting this work for inclusion in set.mm required dividing statements about propositions from those about classes and identifying when a restriction to sets is required. For an overview comparing the details of Frege's two-dimensional notation and that used in set.mm, see mmfrege.html. See ru for discussion of an example of a class that is not a set.

Numbered propositions from [Frege1879]. ax-frege1, ax-frege2, ax-frege8, ax-frege28, ax-frege31, ax-frege41, frege52 (see ax-frege52a, frege52b, and ax-frege52c for translations), frege54 (see ax-frege54a, frege54b and ax-frege54c for translations) and frege58 (see ax-frege58a, ax-frege58b and frege58c for translations) are considered "core" or axioms. However, at least ax-frege8 can be derived from ax-frege1 and ax-frege2, see axfrege8.

Frege introduced implication, negation and the universal quantifier as primitives and did not in the numbered propositions use other logical connectives other than equivalence introduced in ax-frege52a, frege52b, and ax-frege52c. In dffrege69, Frege introduced to say that relation , when restricted to operate on elements of class , will only have elements of class in its domain; see df-he for a definition in terms of image and subset. In dffrege76, Frege introduced notation for the concept of two sets related by the transitive closure of a relation, for which we write , which requires to also be a set. In dffrege99, Frege introduced notation for the concept of two sets either identical or related by the transitive closure of a relation, for which we write , which is a superclass of sets related by the reflexive-transitive relation . Finally, in dffrege115, Frege introduced notation for the concept of a relation having the property elements in its domain pair up with only one element each in its range, for which we write (to ignore any non-relational content of the class ). Frege did this without the expressing concept of a relation (or its transitive closure) as a class, and needed to invent conventions for discussing indeterminate propositions with two slots free and how to recognize which of the slots was domain and which was range. See mmfrege.html for details.

English translations for specific propositions lifted in part from a translation by Stefan Bauer-Mengelberg as reprinted in From Frege to Goedel: A Source Book in Mathematical Logic, 1879-1931. An attempt to align these propositions in the larger set.mm database has also been made. See frege77d for an example.

  1. _Begriffsschrift_ Chapter I
    1. dfxor4
    2. dfxor5
    3. df3or2
    4. df3an2
    5. nev
    6. 0pssin
  2. _Begriffsschrift_ Notation hints
    1. whe
    2. df-he
    3. dfhe2
    4. dfhe3
    5. heeq12
    6. heeq1
    7. heeq2
    8. sbcheg
    9. hess
    10. xphe
    11. 0he
    12. 0heALT
    13. he0
    14. unhe1
    15. snhesn
    16. idhe
    17. psshepw
    18. sshepw
  3. _Begriffsschrift_ Chapter II Implication
    1. ax-frege1
    2. ax-frege2
    3. rp-simp2-frege
    4. rp-simp2
    5. rp-frege3g
    6. frege3
    7. rp-misc1-frege
    8. rp-frege24
    9. rp-frege4g
    10. frege4
    11. frege5
    12. rp-7frege
    13. rp-4frege
    14. rp-6frege
    15. rp-8frege
    16. rp-frege25
    17. frege6
    18. axfrege8
    19. frege7
    20. ax-frege8
    21. frege26
    22. frege27
    23. frege9
    24. frege12
    25. frege11
    26. frege24
    27. frege16
    28. frege25
    29. frege18
    30. frege22
    31. frege10
    32. frege17
    33. frege13
    34. frege14
    35. frege19
    36. frege23
    37. frege15
    38. frege21
    39. frege20
  4. _Begriffsschrift_ Chapter II Implication and Negation
    1. axfrege28
    2. ax-frege28
    3. frege29
    4. frege30
    5. axfrege31
    6. ax-frege31
    7. frege32
    8. frege33
    9. frege34
    10. frege35
    11. frege36
    12. frege37
    13. frege38
    14. frege39
    15. frege40
    16. axfrege41
    17. ax-frege41
    18. frege42
    19. frege43
    20. frege44
    21. frege45
    22. frege46
    23. frege47
    24. frege48
    25. frege49
    26. frege50
    27. frege51
  5. _Begriffsschrift_ Chapter II with logical equivalence
    1. axfrege52a
    2. ax-frege52a
    3. frege52aid
    4. frege53aid
    5. frege53a
    6. axfrege54a
    7. ax-frege54a
    8. frege54cor0a
    9. frege54cor1a
    10. frege55aid
    11. frege55lem1a
    12. frege55lem2a
    13. frege55a
    14. frege55cor1a
    15. frege56aid
    16. frege56a
    17. frege57aid
    18. frege57a
    19. axfrege58a
    20. ax-frege58a
    21. frege58acor
    22. frege59a
    23. frege60a
    24. frege61a
    25. frege62a
    26. frege63a
    27. frege64a
    28. frege65a
    29. frege66a
    30. frege67a
    31. frege68a
  6. _Begriffsschrift_ Chapter II with equivalence of sets
    1. axfrege52c
    2. ax-frege52c
    3. frege52b
    4. frege53b
    5. axfrege54c
    6. ax-frege54c
    7. frege54b
    8. frege54cor1b
    9. frege55lem1b
    10. frege55lem2b
    11. frege55b
    12. frege56b
    13. frege57b
    14. axfrege58b
    15. ax-frege58b
    16. frege58bid
    17. frege58bcor
    18. frege59b
    19. frege60b
    20. frege61b
    21. frege62b
    22. frege63b
    23. frege64b
    24. frege65b
    25. frege66b
    26. frege67b
    27. frege68b
  7. _Begriffsschrift_ Chapter II with equivalence of classes
    1. frege53c
    2. frege54cor1c
    3. frege55lem1c
    4. frege55lem2c
    5. frege55c
    6. frege56c
    7. frege57c
    8. frege58c
    9. frege59c
    10. frege60c
    11. frege61c
    12. frege62c
    13. frege63c
    14. frege64c
    15. frege65c
    16. frege66c
    17. frege67c
    18. frege68c
  8. _Begriffsschrift_ Chapter III Properties hereditary in a sequence
    1. dffrege69
    2. frege70
    3. frege71
    4. frege72
    5. frege73
    6. frege74
    7. frege75
  9. _Begriffsschrift_ Chapter III Following in a sequence
    1. dffrege76
    2. frege77
    3. frege78
    4. frege79
    5. frege80
    6. frege81
    7. frege82
    8. frege83
    9. frege84
    10. frege85
    11. frege86
    12. frege87
    13. frege88
    14. frege89
    15. frege90
    16. frege91
    17. frege92
    18. frege93
    19. frege94
    20. frege95
    21. frege96
    22. frege97
    23. frege98
  10. _Begriffsschrift_ Chapter III Member of sequence
    1. dffrege99
    2. frege100
    3. frege101
    4. frege102
    5. frege103
    6. frege104
    7. frege105
    8. frege106
    9. frege107
    10. frege108
    11. frege109
    12. frege110
    13. frege111
    14. frege112
    15. frege113
    16. frege114
  11. _Begriffsschrift_ Chapter III Single-valued procedures
    1. dffrege115
    2. frege116
    3. frege117
    4. frege118
    5. frege119
    6. frege120
    7. frege121
    8. frege122
    9. frege123
    10. frege124
    11. frege125
    12. frege126
    13. frege127
    14. frege128
    15. frege129
    16. frege130
    17. frege131
    18. frege132
    19. frege133