Two relations are not likely to give you what you want in this scenario.
For example, if the first system has a rule for conjunction introduction:
Thm1 p /\ Thm1 q ==> Thm1 (p AND q)
then this rule requires Thm1 hypotheses. If you add
Thm1 p ==> Thm2 p
you don’t get to use Thm2 hypotheses to prove conjunctions using the first rule.
If you’re committed to this notion of systems of rules that can be extended in
the way you want, I think there’s probably a bit of work required I’m afraid,
and it may not really win you much. I agree though that having to repeat rules
for things like conjunction introduction feels annoying.
Michael
From: Alexander Cox
Date: Friday, 4 January 2019 at 09:11
To: hol-info
Subject: [Hol-info] Relations which build upon each other
Hello,
I’m doing a project on proof theory, and I’m trying to define the proof rules
with Hol_reln. I am defining multiple proof systems which build upon each
other, i.e. intuitionistic logic then classical logic. It seems natural to have
something like:
var (Sys1_rules, …,…) = Hol_reln `…`;
var (Sys2_rules,…,…) = Hol_reln `!x. Sys1 x ==> Sys2 x /\ …`
But when I go to prove something which needs to use Sys2 rules then Sys1 rules,
I don’t know how to get it to work, since the Sys1 rules don’t know mention
Sys2 (nor should they). For example:
`Sys2 x` by metis_tac[Sys2_rules]
`Sys2 y` by metis_tac[Sys1_rules,Sys2_rules] (* Sys1 has no rules for Sys2, so
this fails! *)
The obvious solution is to just keep them independent and have all the rules in
each of them, but I thought I might be missing some elegant way of achieving
this. Please let me know if there is such a trick.
Thank you,
Alex
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
