Frege Notation - Metamath Proof Explorer

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	Metamath	Notes
The proposition, an idea which may be judged true or false, 𝛢.	Alpha	𝜑    𝐴	𝛢 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.	Judgment Alpha	⊢ 𝜑 ⊢ (Ⅎ𝑥𝐴 ∧ ∀𝑥𝑥 ∈ 𝐴) ⊢ 𝐴 = V
The negation of proposition 𝛢.	negated Alpha	¬ 𝜑    (V ∖ 𝐴)
Proposition 𝛢 holds false.	Judgment negated Alpha	⊢ ¬ 𝜑 ⊢ (V ∖ 𝐴) = V ⊢ 𝐴 = ∅
The idea that 𝛣 implies 𝛢.	Beta implies Alpha	(𝜑 → 𝜓)    ((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 𝛢.	Judgment Beta implies Alpha	⊢ (𝜑 → 𝜓) ⊢ ((V ∖ 𝐵) ∪ 𝐴) = V ⊢ 𝐵 ⊆ 𝐴
The judgment that not both 𝛣 and 𝛢 hold true.	Judgment Beta implies negated Alpha	⊢ (𝜑 → ¬ 𝜓) ⊢ (𝜑 ⊼ 𝜓) ⊢ ((V ∖ 𝐵) ∪ (V ∖ 𝐴)) = V ⊢ (V ∖ (𝐵 ∩ 𝐴)) = V ⊢ (𝐵 ∩ 𝐴) = ∅ ⊢ 𝐵 ⊆ (V ∖ 𝐴)
The judgment that 𝛣 or 𝛢 (or both) holds true.	Judgment negated Beta implies Alpha	⊢ (¬ 𝜑 → 𝜓) ⊢ (𝜑 ∨ 𝜓) ⊢ (𝐵 ∪ 𝐴) = V ⊢ (V ∖ 𝐵) ⊆ 𝐴
The judgment that both 𝛣 and 𝛢 hold true.	Judgment negation of Beta implies negated Alpha	⊢ ¬ (𝜑 → ¬ 𝜓) ⊢ ¬ (𝜑 ⊼ 𝜓) ⊢ (𝜑 ∧ 𝜓) ⊢ (V ∖ ((V ∖ 𝐵) ∪ (V ∖ 𝐴))) = V ⊢ (V ∖ (V ∖ (𝐵 ∩ 𝐴))) = V ⊢ (𝐵 ∩ 𝐴) = V
The judgment that exactly one of 𝛣 and 𝛢 holds true.	Judgment that both negated Beta implies Alpha and Beta implies negated Alpha	⊢ ¬ ((¬ 𝜑 → 𝜓) → ¬ (𝜑 → ¬ 𝜓)) ⊢ ((¬ 𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ⊢ (𝜑 ⊻ 𝜓) ⊢ ((𝐵 ∪ 𝐴) ∩ (V ∖ (𝐵 ∩ 𝐴))) = V ⊢ (V ∖ 𝐵) = 𝐴
	Judgment that both Beta implies negated Alpha and negated Beta implies Alpha	⊢ ¬ ((𝜑 → ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓)) ⊢ ((𝜑 → ¬ 𝜓) ∧ (¬ 𝜑 → 𝜓)) ⊢ (𝜑 ⊻ 𝜓) ⊢ ((V ∖ (𝐵 ∩ 𝐴)) ∩ (𝐵 ∪ 𝐴)) = V ⊢ 𝐵 = (V ∖ 𝐴)
The judgment 𝛣 is true while 𝛢 is false.	Judgment negation of Beta implies Alpha	⊢ ¬ (𝜑 → 𝜓) ⊢ (𝜑 ∧ ¬ 𝜓) ⊢ (V ∖ ((V ∖ 𝐵) ∪ 𝐴)) = V ⊢ (𝐵 ∩ (V ∖ 𝐴)) = V ⊢ ((V ∖ 𝐵) ∪ 𝐴) = ∅
	Judgment negation of negated Alpha implies negated Beta	⊢ ¬ (¬ 𝜓 → ¬ 𝜑) ⊢ (¬ 𝜓 ∧ 𝜑) ⊢ (V ∖ (𝐴 ∪ (V ∖ 𝐵))) = V ⊢ ((V ∖ 𝐴) ∩ 𝐵) = V ⊢ (𝐴 ∪ (V ∖ 𝐵)) = ∅
The judgment that neither 𝛢 nor 𝛣 is true.	Judgment negation of negated Alpha implies Beta	⊢ ¬ (¬ 𝜓 → 𝜑) ⊢ ¬ (𝜓 ∨ 𝜑) ⊢ (V ∖ (𝐴 ∪ 𝐵)) = V ⊢ (𝐴 ∪ 𝐵) = ∅
The judgment that the truth of both 𝛤 and 𝛣 implies the truth of 𝛢.	Judgment Gamma and Beta together imply Alpha	⊢ (𝜑 → (𝜓 → 𝜒)) ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⊢ ((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.	Judgment negated Gamma and negated Beta together imply Alpha	⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) ⊢ (𝐶 ∪ (𝐵 ∪ 𝐴)) = V ⊢ ((𝐶 ∪ 𝐵) ∪ 𝐴) = V ⊢ (V / (𝐶 ∪ 𝐵)) ⊆ 𝐴
The judgment that 𝛤, 𝛣, and 𝛢 all hold true.	Judgment negation of Gamma and Beta together imply negated Alpha	⊢ ¬ (𝜑 → (𝜓 → ¬ 𝜒)) ⊢ ¬ ((𝜑 ∧ 𝜓) → ¬ 𝜒) ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⊢ (V ∖ ((V ∖ 𝐶) ∪ ((V ∖ 𝐵) ∪ (V ∖ 𝐴)))) = V ⊢ (𝐶 ∩ (𝐵 ∩ 𝐴)) = V ⊢ ((𝐶 ∩ 𝐵) ∩ 𝐴) = V
The judgment that 𝛢 is equivalent to 𝛣.	Judgment Alpha is equivalent to Beta	⊢ (𝜓 ↔ 𝜑) ⊢ {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜑} ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜓} = {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊢ (((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.)	Judgment Alpha has property Phi	⊢ [𝐴 / 𝑥]𝜑 ⊢ 𝐴 ∈ 𝑃 ⊢ 𝐴 ∈ {𝑥 ∣ 𝜑}	𝛢 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.)	Judgment Psi relates Alpha and Beta	⊢ [𝐴 / 𝑥][𝐵 / 𝑦]𝜓 ⊢ [𝐵 / 𝑦][𝐴 / 𝑥]𝜓 ⊢ 𝐴𝑅𝐵 ⊢ 𝐵◡𝑅𝐴 ⊢ 𝐴{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝐵 ⊢ 𝐴◡{⟨𝑦, 𝑥⟩ ∣ 𝜓}𝐵 ⊢ 𝐵{⟨𝑦, 𝑥⟩ ∣ 𝜓}𝐴 ⊢ 𝐵◡{⟨𝑥, 𝑦⟩ ∣ 𝜓}𝐴 ⊢ 𝐵 ∈ (𝑅 “ {𝐴}) ⊢ 𝐴 ∈ (◡𝑅 “ {𝐵}) ⊢ 𝐵 ∈ ({⟨𝑥, 𝑦⟩ ∣ 𝜓} “ {𝐴}) ⊢ 𝐵 ∈ (◡{⟨𝑦, 𝑥⟩ ∣ 𝜓} “ {𝐴}) ⊢ 𝐴 ∈ (◡{⟨𝑥, 𝑦⟩ ∣ 𝜓} “ {𝐵}) ⊢ 𝐴 ∈ ({⟨𝑦, 𝑥⟩ ∣ 𝜓} “ {𝐵})
The judgment that all 𝔞 have the property 𝛷.	Judgment all a have property Phi	⊢ ∀𝑎[𝑎 / 𝑥]𝜑 ⊢ ∀𝑎𝑎 ∈ 𝑃 ⊢ ∀𝑎𝑎 ∈ {𝑥 ∣ 𝜑}
The negated judgment that no 𝔞 have the property 𝛷.	Judgment negation of all a do not have property Phi	⊢ ¬ ∀𝑎¬ [𝑎 / 𝑥]𝜑 ⊢ ∃𝑎[𝑎 / 𝑥]𝜑 ⊢ ¬ ∀𝑎¬ 𝑎 ∈ 𝑃 ⊢ ∃𝑎𝑎 ∈ 𝑃

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.

Additional Frege Notation

Statement	Frege	Metamath	Notes
Introducing a definition.	Defintion: Alpha equivalent to Beta	⊢ (𝜑 ↔ 𝜓) ⊢ 𝐴 = 𝐵	𝛢 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).	F is hereditary in the f-sequence	𝑅 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 𝑓.	F is hereditary in the converse of the f-sequence	◡𝑅 hereditary 𝐴 (◡𝑅 “ 𝐴) ⊆ 𝐴 ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦𝑅𝑥) → 𝑦 ∈ 𝐴)
𝑦 follows 𝑥 in the 𝑓-sequence	Definition: y follows x in the f-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	Definition: y precedes x in the f-sequence	𝑌 ∈ ∩ {𝑝 ∣ (◡𝑅 “ (𝑝 ∪ {𝑋})) ⊆ 𝑝} 𝑋(t+‘◡𝑅)𝑌
𝑦 belongs to the 𝑓-sequence beginning with 𝑥	Definition: y belongs to the f-sequence beginning with x	𝑌 ∈ ∩ {𝑝 ∣ ((𝑅 ∪ I ) “ (𝑝 ∪ {𝑋})) ⊆ 𝑝} 𝑋((t+‘◡◡𝑅) ∪ I )𝑌 𝑋((t*‘◡◡𝑅) ∪ I )𝑌
𝑦 belongs to the 𝑓-sequence ending with 𝑥	Definition: y belongs to the f-sequence ending with x	𝑌 ∈ ∩ {𝑝 ∣ ((◡𝑅 ∪ I ) “ (𝑝 ∪ {𝑋})) ⊆ 𝑝} 𝑋((t+‘◡𝑅) ∪ I )𝑌 𝑋((t*‘◡𝑅) ∪ I )𝑌
𝑓 is single-valued in the forward direction	f is a function	∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑥𝑅𝑧) → 𝑦 = 𝑧) Fun ◡◡𝑅	𝑓 maps to 𝑅.
𝑓 is single-valued in the reverse direction	The converse of f is a function	∀𝑥∀𝑦∀𝑧((𝑦𝑅𝑥 ∧ 𝑧𝑅𝑥) → 𝑦 = 𝑧) Fun ◡𝑅

Section    More text here.