some questions about wffs in set.mm

[Peter Dolland]

Is there any set of wffs?

Is there an equality (not equivalence) of wffs? So ` -. -. ph =/= ph ` .

Is a mapping of wffs into classes possible?

Clarification very appreciated!
Thank you!
Peter Dolland

[Jim Kingdon]

Not directly but you can achieve many of the things you'd want to with
constructions like { x | ph } or with using a subset of { (/) } as a way
of representing a truth value.

Many of the examples I can think of are in iset.mm, for example

* https://us.metamath.org/ileuni/df-exmid.html

* https://us.metamath.org/ileuni/nndc.html

* https://us.metamath.org/ileuni/mkvprop.html

[Peter Dolland]

I understand, that I can simulate wffs doing something like "Godelization". But I think, this is not what I want. So my questions are going in the direction, why I cannot define a set like { " ( ph \/ -. ph ) " } . Surely, I could define such sets using  the Word constructor <" "> , but it would be a laborious activity to reconstruct the whole wff syntax, and there will be still the challenge to define the semantics.

At the moment the only way to continue my reasoning about integrating algebraic combinatorics I see to examine whether I really need sets of wffs or which possibilities are to avoid them.

In my understanding so far, intuitionistic logic restricts the possibilities of reasoning compared to conventional logic. I do not expect to be able to express facts in it that I cannot express in conventional logic.

[Richard Penner]

Godelization is not being discussed above. Equivalence of wffs is done with the biimplication operator, ( ph <-> ps ). Definitions for new wff syntax are typically introduced with a biimplication, example:

df-an ⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) { A and B ) is equivalent to the negation of ( A implies not B ). This is is the introduction of the and symbol's meaning, so metamath counts it as an axiom, just like it counts the syntax statement wa as an axiom.

You can't define a set from every wff, but you can define a class. { x | ph } defines a class such that 

sbc8g ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))  {when A is an element of any class, ph with A properly substituted for x is true if-and-only-if A is an element of { x | ph } )

Many, but not all classes are sets, but only sets can be elements of sets. The distinction between wffs., classes and sets became important at the begining of the 20th century when by playing games with the language of wffs, irreconcilable problems arose with the historical practice of treating wffs, classes and sets the same. A famous example is Russell's paradox and the class R = {𝑥 ∣ 𝑥 ∉ 𝑥} ;
If R is a set, then either R is a member of itself, and therefore it can't be a member of itself OR R is not a member of itself and therefore must be a member of itself. 

See https://us.metamath.org/mpeuni/ru.html for the then-revolutionary conclusion that R is not a set.

Classes that are not sets are called proper classes, with examples including the class of all sets, {𝑥 ∣ ⊤}, and the class of all sets which have the property that every proper subset which is transitively ordered is also a member {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} , commonly called the ordinal numbers.

So you can't have a set, or even a class, of all the wffs. If you want to count all possible wffs, your main problem is that anyone can define a new syntax at any time and your work becomes obsolete. Better to count something more abstract like the number of trees with j types of terminal nodes, k types of single-child nodes, m-types of two-child nodes, n-types of three-child nodes, etc. Then you could extend that work to include nodes which are not wffs but also classes and set variables. Abstraction is wonderful as Eugenia Cheng named her book "The Joy of Abstraction" in part as a play on a famous 1972 book and Keith Devlin's 1993 textbook.