Биусловное доказательство Fitch помогает?

Подсказка: всегда поднимайте контекст с тем, что нужно разрядить, чтобы вывести цель. Таким образом, стремясь ввести универсальный квантор, вам нужно начать поддоказательство, приняв произвольный термин . В данном случае дважды.

Предположим, что термины [a] и [b] произвольные, каким -то образом выведите бикондиционал (подсказка: будет задействовано несколько универсальных исключений), затем введите два универсальных.

|  Ɐx Ɐy (Indiff(x,y)→Indiff(y,x))        Premise
|_ :
|  :
|  |_ [a]                                 Assumption
|  |  |_ [b]                              Assumption
|  |  |  Ɐx Ɐy (Indiff(x,y)→Indiff(y,x))  Reiteration
|  |  |  :
|  |  |  Indiff(a,b)↔Indiff(b,a)          Biconditional Introduction
|  |  Ɐy (Indiff(a,y)↔Indiff(y,a))        Universal Introduction
|  Ɐx Ɐy (Indiff(x,y)↔Indiff(y,x))        Universal Introduction
■

Начинка в середине не должна быть слишком жесткой. Похоже, ваш чекер требует биусловного введения, чтобы выглядеть так:

h|  |_ X    Assumption
:|  |  :
k|  |  Y    Somehow derived
 |  +
n|  |_ Y    Assumption
:|  |  :
m|  |  X    Somehow derived
 |  X ↔ Y   Biconditional Introduction (h-k,n-m)

Я использую другое средство проверки корректуры, но, возможно, наблюдение за тем, как здесь достигается цель, может помочь сделать эту работу с помощью используемого вами средства проверки корректуры.

Это средство проверки доказательств имеет другой способ принятия правильно сформированных формул. Я заменил "Indiff" на "I".

Я также заметил, что целью было просто «∀x∀y(Ixy↔Iyx)», то есть «∀x∀y(Indiff(x,y) ↔ Indiff(y,x)», и у вас в качестве пятого посылка «∀x∀y(Ixy → Iyx)», то есть «∀x∀y(Indiff(x,y) → Indiff(y,x)». Мне нужно было использовать только эту посылку, поэтому я не включал другие.

Чтобы получить бикондиционал, мне пришлось запустить два условных поддоказательства. В первом я принял «Iab» в строке 2 и достиг цели этого поддоказательства, «Iba», в строке 5. Во втором подпроверке я пошел в противоположном направлении и принял «Iba» в строке 6 и достиг цели «Iab». " в строке 9. В каждом поддоказательстве я исключил универсальный квантификатор, но использовал имена для переменных "x" и "y", которые помогли мне прийти к заключению.

Когда я ввел бикондиционал в строке 10, это сняло предположения в строках 2 и 6.

Описание правил есть в forallx (ссылка ниже). Для универсального исключения (∀E) см. стр. 239-240. Условное исключение (→E) см. на стр. 103-104. Биусловное введение (↔I) см. на стр. 111-112. Универсальное введение (∀I) см. на стр. 243-246.

---

использованная литература

Редактор и средство проверки естественной дедукции Кевина Клемента на JavaScript/PHP в стиле Fitch http://proofs.openlogicproject.org/

PD Магнус, Тим Баттон с дополнениями Дж. Роберта Лофтиса, ремикшированный и отредактированный Аароном Томасом-Болдуком, Ричардом Заком, forallx Calgary Remix: An Introduction to Formal Logic, зима 2018 г. http://forallx.openlogicproject.org/