This is discussed at some length at
https://us.metamath.org/mpeuni/mmnatded.html and if you want something
shorter, "put everything in deduction form" would be my one sentence
summary.
On 1/23/25 04:43, jagra wrote:
Greetings,
Carnap book chapter 4 (https://carnap.io/book/4) talks about
Conditional Derivations. Was trying to come up with a way to do it in
metamath but am stuck.
An example is:
For the argument /P/ → /Q/, /Q/ → /R/ ⊢ /P/ → /R/, we can derive:
1. Show:P->R
2. P :AS
3. P->Q :PR
4. Q->R :PR
5. Q :MP 2,3
6. R :MP 4,5
7. :CD 6
It assumes (AS) P on step 2, introduces premises (PR), applies Modus
Ponens (MP) and concludes the proof of P -> R with a conditional
derivation.
All seems very similar to metamath way of doing things except (?) from
the :AS part. Is this translatable directly to metamath somehow?
Best regards,
JA
--
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/c710e4cd-093c-41af-ab90-542a4c125738n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/c710e4cd-093c-41af-ab90-542a4c125738n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/efde1c2f-db33-4149-94b9-29ad510b43f8%40panix.com.
