Доказательство теоремы из первых принципов с использованием SML с правилами вывода HOL - PullRequest
Новая
       10

Доказательство теоремы из первых принципов с использованием SML с правилами вывода HOL

0 голосов
/ 01 мая 2018

Я пытаюсь доказать теорему [] |- p /\ q <=> q /\ p :thm, используя SML с правилами вывода HOL. Вот код SML: 

val thm1 = ASSUME ``p:bool /\ q:bool``;
val thm2 = ASSUME ``p:bool``;
val thm3 = ASSUME ``q:bool``;
val thm4 = CONJ thm2 thm3;
val thm5 = CONJ thm3 thm2;
val thm6 = DISCH ``(q:bool/\p:bool)`` thm4;
val thm7 = DISCH ``(p:bool/\q:bool)`` thm5;
val thm8 = IMP_ANTISYM_RULE thm6 thm7;

Результат приведенного выше кода дает: 

val thm8 =  [(p :bool), (q :bool)] |- (q :bool) /\ (p :bool) <=> p /\ q: thm

Что я делаю не так?

1 Ответ

0 голосов
/ 03 мая 2018

Проблема с вашей окончательной теоремой состоит в том, что у вас все еще есть p и q в качестве предположений, введенных через thm2 и thm3, тогда как вы можете и должны получить их из thm1.

Первая нужная вам теорема - это что-то вроде p /\ q ==> p. Я нашел соответствующее правило, просматривая описание (с. 2.3.24). Это называется CONJUNCT1.

Используя его, мы можем получить p в качестве теоремы из thm1: 

val thmp = CONJUNCT1 thm1;

Та же идея работает для получения q в качестве теоремы от thm1: 

val thmq = CONJUNCT2 thm1;

И тогда вы можете применить свою идею для thm5: 

val thm5 = CONJ thmq thmp;

Важная вещь в том, что мы не используем p, полученные из p (thm2) и q, полученные из q (thm3), а точнее p, полученный из p /\ q и q, полученный из p /\ q (настройка show_assumes := true; может помочь увидеть это больше ясно).

Наконец, мы применим вашу идею для thm7: 

val thm7 = DISCH ``p /\ q`` thm5;

для получения первой половины желаемого результата, но без посторонних предположений.

Вторая половина получается аналогично: 

val thm9 = ASSUME (``q /\ p``);
val thmp2 = CONJUNCT2 thm9;
val thmq2 = CONJUNCT1 thm9;
val thm6 =  DISCH ``q /\ p`` (CONJ thmp2 thmq2);

И тогда ваша идея для thm8 отлично работает: 

val thm8 = IMP_ANTISYM_RULE thm7 thm6;
...