first-order logic of the following sequence

Question

“There is a barber in Atlantis who shaves exactly those citizens of Atlantis who do not shave

themselves. Therefore, there is a barber in Atlantis who is not a citizen of Atlantis.”

Parameters: ∀; B, C (1-place predicate symbols); S (2-place predicate symbol). Bx: ‘x is a barber

in Atlantis’; Cx: ‘x is a citizen of Atlantis’; Sxy: ‘x shaves y’. You may use any sentential connective

and also the existential quantifier that is definable in terms of ∀.

Answer 1

∃x(Bx & ∀y((Cy & ~Syy) <-> Sxy)) ∴ ∃x(Bx & ~Cx)

1. ∃x(Bx & ∀y((Cy & ~Syy) <-> Sxy)) premise

2. ~∃x(Bx & ~Cx) Assume for Reductio/Negation Elimination

3. ∀x~(Bx & ~Cx) 2, Quantifier Negation

4. Ba & ∀y((Cy & ~Syy) <-> Say) 1, Existential Elimination/Instantiation

5. Ba 4, Simplification/Conjunction Elimination

6. ∀y((Cy & ~Syy) <-> Say) 4, Simplification/Conjunction Elimination

7. ~(Ba & ~Ca) 3, Universal Elimination/Instantiation

8. ~Ba v ~~Ca 7, DeMorgan's Law

9. ~Ba v Ca 8, Double Negation Elimination

10. ~~Ba 5, Double Negation Introduction

11. Ca 9, 10 DisjunctiveSyllogism/DisjunctionElimination

12. (Ca & ~Saa) <-> Saa 6, Universal Elimination/Instantiation

13. Ca -> (~Saa <-> Saa) 12, Exportation

14. ~Saa <-> Saa 11, 13, Modus Ponens/Conditional Introduction

15. ~(~Saa v Saa) Assume for Reductio/Negation Elimination

16. ~~Saa & ~Saa 15, DeMorgan's Law

17. ~Saa v Saa 15-16, Reduction/Negation Elimination

18. ~Saa -> Saa 14, Biconditional Elimination

19. Saa -> ~Saa 14, Biconditional Elimination

20. ~Saa Assume for Conditional Proof/Introduction

21. Saa 18, 20, Modus Ponens/Conditional Introduction

22. ~Saa & Saa 20, 21, Conjunction Introduction

23. ~Saa -> (~Saa & Saa) 20-22, Conditional Proof/Introduction

24. Saa Assume for Conditional Proof/Introduction

25. ~Saa 19, 24, Modus Ponens/Conditional Introduction

26. ~Saa & Saa 24, 25, Conjunction Introduction

27. Saa -> (~Saa & Saa) 24-26, Conditional Proof/Introduction

28. ~Saa & Saa 17, 23, 27, Constructive Dilemma

29. ∃x(Bx & ~Cx) 2-28, Reductio/Negation Elimination

Let me know if you'd like a session with me! I'd be happy to help you with first-order logic