 Metamath Proof Explorer Frege Notation Mirrors  >  Home  >  MPE Home  >  Frege Notation

Frege Notation and Metamath    While Frege, in his 1879 work Begriffsschrift, 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.

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.

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 𝑦.

Guide to Frege Notation
Statement Frege MetamathNotes
The proposition, an idea which may be judged true or false, 𝛢. 𝜑
𝐴
𝛢 maps to proposition 𝜑 or class 𝐴.
V is the universal class of all sets.
is the empty class.
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.
Proposition 𝛢 holds true. 𝜑
(𝑥𝐴 ∧ ∀𝑥𝑥𝐴)
𝐴 = V
The negation of proposition 𝛢. ¬ 𝜑
(V ∖ 𝐴)
Proposition 𝛢 holds false. ¬ 𝜑
(V ∖ 𝐴) = V
𝐴 = ∅
The idea that 𝛣 implies 𝛢. (𝜑𝜓)
((V ∖ 𝐵) ∪ 𝐴)
𝛣 maps to 𝜑 or 𝐵.
𝛢 maps to 𝜓 or 𝐴.
Since Metamath's standard set.mm has more connectives for propositions than just implication and negation, some of these statements have fully equivalent synonyms.
The judgment that the truth of 𝛣 implies the truth of 𝛢. (𝜑𝜓)
((V ∖ 𝐵) ∪ 𝐴) = V
𝐵𝐴
The judgment that not both 𝛣 and 𝛢 hold true. (𝜑 → ¬ 𝜓)
(𝜑𝜓)
((V ∖ 𝐵) ∪ (V ∖ 𝐴)) = V
(V ∖ (𝐵𝐴)) = V
(𝐵𝐴) = ∅
𝐵 ⊆ (V ∖ 𝐴)
The judgment that 𝛣 or 𝛢 (or both) holds true. 𝜑𝜓)
(𝜑𝜓)
(𝐵𝐴) = V
(V ∖ 𝐵) ⊆ 𝐴
The judgment that both 𝛣 and 𝛢 hold true. ¬ (𝜑 → ¬ 𝜓)
¬ (𝜑𝜓)
(𝜑𝜓)
(V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐴))) = V
(V ∖ (V ∖ (𝐵𝐴))) = V
(𝐵𝐴) = V
The judgment that exactly one of 𝛣 and 𝛢 holds true. ¬ ((¬ 𝜑𝜓) → ¬ (𝜑 → ¬ 𝜓))
((¬ 𝜑𝜓) ∧ (𝜑 → ¬ 𝜓))
(𝜑𝜓)
((𝐵𝐴) ∩ (V ∖ (𝐵𝐴))) = V
(V ∖ 𝐵) = 𝐴 ¬ ((𝜑 → ¬ 𝜓) → ¬ (¬ 𝜑𝜓))
((𝜑 → ¬ 𝜓) ∧ (¬ 𝜑𝜓))
(𝜑𝜓)
((V ∖ (𝐵𝐴)) ∩ (𝐵𝐴)) = V
𝐵 = (V ∖ 𝐴)
The judgment 𝛣 is true while 𝛢 is false. ¬ (𝜑𝜓)
(𝜑 ∧ ¬ 𝜓)
(V ∖ ((V ∖ 𝐵) ∪ 𝐴)) = V
(𝐵 ∩ (V ∖ 𝐴)) = V
((V ∖ 𝐵) ∪ 𝐴) = ∅ ¬ (¬ 𝜓 → ¬ 𝜑)
𝜓𝜑)
(V ∖ (𝐴 ∪ (V ∖ 𝐵))) = V
((V ∖ 𝐴) ∩ 𝐵) = V
(𝐴 ∪ (V ∖ 𝐵)) = ∅
The judgment that neither 𝛢 nor 𝛣 is true. ¬ (¬ 𝜓𝜑)
¬ (𝜓𝜑)
(V ∖ (𝐴𝐵)) = V
(𝐴𝐵) = ∅
The judgment that the truth of both 𝛤 and 𝛣 implies the truth of 𝛢. (𝜑 → (𝜓𝜒))
((𝜑𝜓) → 𝜒)
((V ∖ 𝐶) ∪ ((V ∖ 𝐵) ∪ 𝐴)) = V
(((V ∖ 𝐶) ∪ (V ∖ 𝐵)) ∪ 𝐴) = V
((V ∖ (𝐶𝐵)) ∪ 𝐴) = V
(𝐶𝐵) ⊆ 𝐴
𝛤 maps to 𝜑 or 𝐶.
𝛣 maps to 𝜓 or 𝐵.
𝛢 maps to 𝜒 or 𝐴.
Since Metamath's standard set.mm has more connectives for propositions than just implication and negation, some of these statements have fully equivalent synonyms.
The judgment that 𝛤, 𝛣, or 𝛢 (or any combination) holds true. 𝜑 → (¬ 𝜓𝜒))
((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒)
(𝜑𝜓𝜒)
(𝐶 ∪ (𝐵𝐴)) = V
((𝐶𝐵) ∪ 𝐴) = V
(V / (𝐶𝐵)) ⊆ 𝐴
The judgment that 𝛤, 𝛣, and 𝛢 all hold true. ¬ (𝜑 → (𝜓 → ¬ 𝜒))
¬ ((𝜑𝜓) → ¬ 𝜒)
(𝜑𝜓𝜒)
(V ∖ ((V ∖ 𝐶) ∪ ((V ∖ 𝐵) ∪ (V ∖ 𝐴)))) = V
(𝐶 ∩ (𝐵𝐴)) = V
((𝐶𝐵) ∩ 𝐴) = V
The judgment that 𝛢 is equivalent to 𝛣. (𝜓𝜑)
{𝑥𝜓} = {𝑥𝜑}
{⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
(((V ∖ 𝐴) ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐴)) = V
((V ∖ (𝐴𝐵)) ∪ (𝐴𝐵)) = V
(𝐴𝐵) ⊆ (𝐴𝐵)
𝐴 = 𝐵
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 ¬ (ω ⊆ 𝑋 ↔ (ω ⊆ 𝑋𝑋 ∈ V)) but {𝑥 ∣ ω ⊆ 𝑥} = {𝑥 ∣ (ω ⊆ 𝑥𝑥 ∈ 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.
𝛢 maps to 𝜓 or 𝐴.
𝛣 maps to 𝜑 or 𝐵
The judgment that 𝛢 has the property 𝛷. (Which implies 𝛢 is a set.) [𝐴 / 𝑥]𝜑
𝐴𝑃
𝐴 ∈ {𝑥𝜑}
𝛢 maps to 𝐴.
𝛣 maps to 𝐵.
𝛷 maps to 𝜑 or 𝑃 or {𝑥𝜑}.
𝛹 maps to 𝜓 or 𝑅 or {⟨𝑥, 𝑦⟩ ∣ 𝜓}.
𝔞 maps to 𝑎.
𝑥 and 𝑦 are distinct set variables which presumably, but not necessarily, appear in what is eventually substituted for 𝜑 or 𝜓 and which nowhere appear in 𝐴 or 𝐵.
The judgment that 𝛣 stands in relation 𝛹 to 𝛢. (Which implies that 𝛢 and 𝛣 are sets.) [𝐴 / 𝑥][𝐵 / 𝑦]𝜓
[𝐵 / 𝑦][𝐴 / 𝑥]𝜓
𝐴𝑅𝐵
𝐵𝑅𝐴
𝐴{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝐵
𝐴{⟨𝑦, 𝑥⟩ ∣ 𝜓}𝐵
𝐵{⟨𝑦, 𝑥⟩ ∣ 𝜓}𝐴
𝐵{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝐴
𝐵 ∈ (𝑅 “ {𝐴})
𝐴 ∈ (𝑅 “ {𝐵})
𝐵 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} “ {𝐴})
𝐵 ∈ ({⟨𝑦, 𝑥⟩ ∣ 𝜓} “ {𝐴})
𝐴 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} “ {𝐵})
𝐴 ∈ ({⟨𝑦, 𝑥⟩ ∣ 𝜓} “ {𝐵})
The judgment that all 𝔞 have the property 𝛷. 𝑎[𝑎 / 𝑥]𝜑
𝑎𝑎𝑃
𝑎𝑎 ∈ {𝑥𝜑}
The negated judgment that no 𝔞 have the property 𝛷. ¬ ∀𝑎¬ [𝑎 / 𝑥]𝜑
𝑎[𝑎 / 𝑥]𝜑
¬ ∀𝑎¬ 𝑎𝑃
𝑎𝑎𝑃
Colors of variables: wff set class

Additional Notation    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 𝑥𝑅𝑦, 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.

Statement Frege MetamathNotes
Introducing a definition. (𝜑𝜓)
𝐴 = 𝐵
𝛢 maps to 𝜑 or 𝐴.
𝛣 maps to 𝜓 or 𝐵.
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.
This judgment is a definition in Metamath only if it is the content of an \$a statement as Metamath doesn't distinguish between definitions and axioms.
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). 𝑅 hereditary 𝐴
(𝑅𝐴) ⊆ 𝐴
𝑥𝑦((𝑥𝐴𝑥𝑅𝑦) → 𝑦𝐴)
𝑓 maps to 𝑅.
𝐹 maps to 𝐴.
α and δ are newly-introduced placeholders which do not appear in any expression similar the the distinct bound variables 𝑥 and 𝑦, provided that they don't appear in 𝐴 or 𝑅.
The hereditary connective was introduced while translating Frege to avoid the need to duplicate arbitrarily long expressions for 𝐴.
The proposition that membership in class 𝐹 (a proposition schema with one slot) is hereditary in the sequence generated by converse of the relation 𝑓. 𝑅 hereditary 𝐴
(𝑅𝐴) ⊆ 𝐴
𝑥𝑦((𝑥𝐴𝑦𝑅𝑥) → 𝑦𝐴)
𝑦 follows 𝑥 in the 𝑓-sequence 𝑌 {𝑝 ∣ (𝑅 “ (𝑝 ∪ {𝑋})) ⊆ 𝑝}
𝑋(t+‘𝑅)𝑌
𝑥 maps to 𝑋.
𝑦 maps to 𝑌.
𝑓 maps to 𝑅.
𝑝 is a bound set variable, distinct from 𝑋, 𝑌 and 𝑅. Because 𝑝 is a set variable, so the image of a set under 𝑅 (or 𝑅) must be a set. For the abbreviations, we require the stronger condition that the relational content of 𝑅 must be a set.
t+ maps to the transitive closure of a relation, while t* maps to the reflexive-transitive closure of a relation.
I is the identity function which has a wider domain than the reflexive-transitive closure of a relation.
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.
This statement cannot be true unless both 𝑋 and 𝑌 are sets.
𝑦 precedes 𝑥 in the 𝑓-sequence 𝑌 {𝑝 ∣ (𝑅 “ (𝑝 ∪ {𝑋})) ⊆ 𝑝}
𝑋(t+‘𝑅)𝑌
𝑦 belongs to the 𝑓-sequence beginning with 𝑥 𝑌 {𝑝 ∣ ((𝑅 ∪ I ) “ (𝑝 ∪ {𝑋})) ⊆ 𝑝}
𝑋((t+‘𝑅) ∪ I )𝑌
𝑋((t*‘𝑅) ∪ I )𝑌
𝑦 belongs to the 𝑓-sequence ending with 𝑥 𝑌 {𝑝 ∣ ((𝑅 ∪ I ) “ (𝑝 ∪ {𝑋})) ⊆ 𝑝}
𝑋((t+‘𝑅) ∪ I )𝑌
𝑋((t*‘𝑅) ∪ I )𝑌
𝑓 is single-valued in the forward direction 𝑥𝑦𝑧((𝑥𝑅𝑦𝑥𝑅𝑧) → 𝑦 = 𝑧)
Fun 𝑅
𝑓 maps to 𝑅.
𝑓 is single-valued in the reverse direction 𝑥𝑦𝑧((𝑦𝑅𝑥𝑧𝑅𝑥) → 𝑦 = 𝑧)
Fun 𝑅
Colors of variables: wff set class

Section    More text here.