Navelgazer · Logic Linter
Documentation
Found a Bug?
Source Code
Gaurav Manek
Click here or hit Ctrl+Enter to build and test.
// Premise "A person will be respected by anyone who admires someone the person teaches.": [1] (1) (∀x)(∀y)((∃z)(Txz ∧ Ayz) → Ryx) P // Premise "Everyone admires logic students.": [2] (2) (∀x)(∀y)(Lx → Ayx) P [3] (3) (∃y)(Ly ∧ Txy) P [3][4] (4) (La ∧ Txa) (3)aEII [2] (5) (La → Aya) (2) UI [2][3][4] (6) (Txa ∧ Aya) (4)(5) TF [2][3][4] (7) (∃z)(Txz ∧ Ayz) (6) EG [2][3] (8) (∃z)(Txz ∧ Ayz) [4](7) EIE [1] (9) ((∃z)(Txz ∧ Ayz) → Ryx) (1) UI [1][2][3] (10) Ryx (8)(9) TF [1][2][3] (11) (∀z)Rzx (10) UG [1][2] (12) ((∃y)(Ly ∧ Txy) → (∀z)Rzx) [3](11) D [1][2] (13) (∀x)((∃y)(Ly ∧ Txy) → (∀z)Rzx) (12) UG // Conclusion "A person who teaches a logic student is admired by all." // Example adapted from Warren Goldfarb's "Deductive Logic" (p. 197-198)