This is the Proof Machine for the PL system in Ted Sider's Logic for Philosophy Ch. 2. See below for instructional video and practice problems.
If you're looking for them, the regular Proof Machine is here and the Truth Machine is here.
For atomic sentences, use P, Q, R, etc.
For premises, use "Premise" or "P" as citation.
For axioms, use "PL1", "PL2" or "PL3" as citation.
For modus ponens, use "MP;1,2" (e.g.) as citation.
Line Return or Control + "l" key: checks the line.
Row Control + "r" key: adds row below.
Row Control + "d" key: deletes current row.
Entire proof Control + "p" key: checks entire proof.
Toolbox: Allow spaces:
PL Proof Machine
1. | |||
2. | |||
3. | |||
4. | |||
5. | |||
6. | |||
Messages
Instructions: How to use the PL Proof Machine
PL Practice Problems
Level 2
- Exercise 2.4a (“Identity Principle”): {no prem} => P->P
- IP practice: {no prem} => ~Q->~Q
- Exercise 2.4b: {no prem} => (~P->P)->P
- “Contraposition 1”: ~P->~Q => Q->P
- “Contraposition 2”: P->Q => ~Q->~P
- Exercise 2.11a: {no prem} => P->((P->Q)->Q)
- Exercise 2.11b: {no prem} => (P->(Q->R))->(Q->(P->R))
- Exercise 2.11c (“DN elimination”): {no prem} => ~~P->P
- Exercise 2.11d (“DN intro”, full toolkit): {no prem} => P->~~P
Level 3
- Exercise 2.4c: ~~P => P
- “Ex falso”: P and ~P => Q
- “Negated Conditional 1”: ~(P->Q) => P
- “Negated Conditional 2”: ~(P->Q) => ~Q
- “Excluded Middle MP”: P->Q and ~P->Q => Q
- “Contraposition 2” with only DT: P->Q => ~Q->~P
- Exercise 2.11c with only DT: {no prem} => ~~P->P
- Exercise 2.11d with only DT: {no prem} => P->~~P