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.
On Saturday, January 4, 2025 at 8:19:04 AM UTC-8 Peter Dolland wrote:
> 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.
> Am 03.01.2025 um 16:50 schrieb 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
>
> On 1/3/25 07:10, 'Peter Dolland' via Metamath wrote:
>
> 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
>
>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/00afab6b-50ba-4862-9179-c028a313f18an%40googlegroups.com.
