This is fixed mode of the Proof Machine for the PL, where the conclusion and toolbox mode is set for you.
To return to sandbox mode go here.
For atomic sentences, use P, Q, R, etc.
For premises, use "Premise" or "P" for citation.
For axioms, use "PL1", "PL2" or "PL3" for citation.
For modus ponens, use "MP;1,2" (e.g.) for 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 (fixed)
1. | |||
2. | |||
3. | |||
4. | |||
5. | |||
6. | |||
Messages
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