Fitch Biconditional Proof Help?

Question

Hi, I'm starting to learn formal proofs using Fitch, but I'm having a bit of trouble figuring out my arguments. I've generally mapped out the subproofs I was considering to use, but I'm unsure how to proceed from this point.

Answer 1

Hint: Always raise a context with what needs to be discharged to deduce the target. Thusly, when aiming to introduce an universal quantifier, you need to begin the subproof by assuming an arbitrary term. In this case, twice.

Assume the arbitrary terms, [a], and [b], somehow derive the biconditional (hint: several universal eliminations will be involved), then introduce two universals.

|  Ɐ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
■

Filling in the middle should not be too hard. It looks like your checker requires biconditional introduction to look thus:

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

Answer 2

I am using a different proof checker, but perhaps seeing how the goal is reached here may help to make this work with the proof checker you are using.

This proof checker has a different way of accepting well-formed formulas. I replaced "Indiff" with "I".

I also noticed that the goal was simply "∀x∀y(Ixy↔Iyx)", that is, "∀x∀y(Indiff(x,y) ↔ Indiff(y,x)", and you had as the fifth premise "∀x∀y(Ixy → Iyx)", that is, "∀x∀y(Indiff(x,y) → Indiff(y,x)". I only needed to use that premise and so I did not include the others.

To get a biconditional I had to start two conditional subproofs. The first one I assumed "Iab" on line 2 and reached the goal of that subproof, "Iba", on line 5. The second subproof I went in the opposite direction and assumed "Iba" on line 6 and reached the goal "Iab" on line 9. Within each subproof I eliminated the universal quantifier, but using names for the "x" and "y" variables that helped me reach the conclusion.

When I introduced the biconditional on line 10 this discharged the assumptions on lines 2 and 6.

A description of the rules are in forallx (link below). For universal elimination (∀E) see pages 239-240. For conditional elimination (→E) see pages 103-104. For biconditional introduction (↔I) see pages 111-112. For universal introduction (∀I) see pages 243-246.

---

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/