The Stack Overflow podcast is back! Listen to an interview with our new CEO.

 3 added 132 characters in body edited Nov 20 '18 at 9:55 Graham Kemp 1,40422 silver badges1212 bronze badges 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) `````` 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. 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) `````` 2 added 132 characters in body edited Nov 20 '18 at 9:49 Graham Kemp 1,40422 silver badges1212 bronze badges Hint: Always raise a subproofcontext with what needs to be discharged to derivededuce the target. For an universal statement Thusly, when aiming to introduce an universal quantifier, you need to raisebegin the subproof by assuming an arbitrary termarbitrary term. In this case, twice. Assume the arbitrary terms, [a], and [b], somehowsomehow 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. Hint: Always raise a subproof with what needs to be discharged to derive the target. For an universal statement, you need to raise an arbitrary term 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 ■ `````` 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. 1 answered Nov 20 '18 at 9:43 Graham Kemp 1,40422 silver badges1212 bronze badges Hint: Always raise a subproof with what needs to be discharged to derive the target. For an universal statement, you need to raise an arbitrary term 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 ■ ``````