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/02f1f42c-9002-477e-8bac-96c7bda13e91%40gmx.de.
