This is the Proof Machine (FOL beta) in sandbox mode. See below for instructional video. The full FOL system now works: all quantifier and identity rules. Names and predicates must be short form, as in G(p) or AxR(x,a).
If you're looking for the Truth Machine, go here.
When the cursor is on a line:
Line Return or Control + "l" key: checks the line.
Subproof Backslash "\" key: adds subproof to line.
Subproof Shift + backslash "\" key: deletes subproof.
Row Control + "r" key: adds row below.
Row Control + "d" key: deletes current row.
Entire proof Control + "p" key: checks entire proof.
Proof Machine (FOL beta)
| 1. | |||
| 2. | |||
| 3. | |||
| 4. | |||
| 5. | |||
| 6. | |||
Messages
Instructions: How to use the Proof Machine
BOOL Problems
Level 1
- P&Q => Q&P
- ~~(~~P&Q)&~R => P
- P&(Q&R)&S => (RvT)&(RvU)
- ~~~~A => A
- ~~~P => (~Pv~Q)v(RvS)
- ~~Pv~~P => P
- {no prem} => ~(~~P&~P)
- Av(B&C) => CvA
- ~A => ~~~A
- ~B => ~(A&B)
- PvQ and ~Q => Pv~R
- ~~P&(~~Q&R)&S => TvQ
- {no prem} => ~(P&(~~~P&Q))
- (P&~P)v(Q&~Q)v(R&~R) => #
- P&Q&~~R => R&Q
- P&~~(Q&~~R) => QvS
- ~P and Q => ~(Pv~Q)
- A&B&C and ~C =>~A
- ~~~A&B => ~(A&C)
- {no prem} => ~(~~~~~P&P)
- {no prem} => ~~~(~~P&~~Q&~P)
- ~~(A&B)v(~~~C&D) => Bv~C
- Av~~~Bv# => Av~B
- {no prem} => ~(P&Q&#)
- ~~Av~~Bv~~C => AvBvC
- ~~~A&~~B => (~AvC)&(BvC)
- ~~Pv~~~Q => Pv~Q
- ~~~~~A => Bv~A
- ~~P&Q&~~R&S => RvT
- ~~P&Q&~~R&S => R&(Pv~~T)
- (A&B)&(C&D) => (D&C)&(B&A)
- A&B&C&D => B&(A&(D&C))
- (~~A&~B)&C => A&(~B&C)
- ~(~~A&~B) => ~Av~~B
- (P&Q)v~~P => P
- A&~B&# => C
Level 2
- ~(~CvD) => C&~D
- A&B and ~BvC => C
- {no prem} => Pv~P
- (P&Q)v(R&Q) and S => Q&S
- (P&Q)v(R&S) => QvR
- ~(~Av~B) => A&B
- ~(PvQv~~~R) => R
- ~(Pv~QvR) => ~P&Q&~R
- P&Q and RvS => (Q&R)vS
- Av(B&C) => (AvB)&(AvC)
- ~PvQ and ~PvR => ~Pv(Q&R)
- ~Pv(Q&R) => ~PvQ
- ~Pv(Q&R) => (~PvQ)&(~PvR)
- Pv~(QvR) => Pv~Q
- ~(~AvB)vC and ~C => A
- ~(~AvB)vC and ~C => A&~B
- PvQv~R and ~Q&R => P
- A&C and ~(AvB)v~CvD => D
- A&B and ~Bv~A => #
- {no prem} => ~~(~~Pv~P)
- {no prem} => ~(P&Q&(~Pv~Q))
- {no prem} => ~((~PvQ)&~~(P&~Q))
- {no prem} => ~((P&~P)v(Q&~Q))
- {no prem} => Pv~Qv~RvQ
- ~(B&A) => ~(A&B)
- ~(PvQ) => ~(QvP)
- ~(P&~~Q&v~R) => ~(Q&~~P&~R)
- ~(Pv~~Qv~R) => ~(Qv~~Pv~R)
- ~Pv(P&Q) => Qv~P
- ~(~~A&B) => ~(A&~~B)
- ~P => ~((PvQ)&~Q)
- (~~Av~B)vC => Av(~BvC)
- ~Av~~B => ~(~~A&~B)
- A&~~B => ~(~Av~B)
- (P&Q)v(R&S) => QvR
- ~~P&(QvR) => P&(Qv~~R)
- P&~~(Qv~~R) => ~~P&(QvR)
Level 3
- ~(~C&D) => Cv~D
- ~(P&Q&~R) => ~Pv~QvR
- (A&~~B)vB and ~(C&B) => ~C
- {no prem} => ~Pv~(Q&~(P&Q))
- ~PvQ, ~QvR, ~R => ~P
- {no prem} => ~Pv~(~Q&(~PvQ))
- (~PvQ)&(RvS), PvT, and ~T => Q
- (~AvB)&~C, ~EvA and ~(~EvB)vD => DvB
- P&Q&~R, ~PvRvS and ~SvR => #
- ~~A&(~BvC) => (A&~B)v(A&C)
- AvB and ~~AvC => Av(B&~~C)
- AvB and CvD => (A&C)v(A&D)v(B&C)v(B&D)
- (A&B)v(C&D) => (AvC)&(AvD)&(BvC)&(BvD)
- (AvC)&(AvD) and (BvC)&(BvD) => (A&B)v(C&D)
- (A&C)v(A&D)v(B&C)v(B&D) => (AvB)&(CvD)
- Pv~(Q&R) and R => Pv~Q
- Pv~(Q&R) => Pv~Qv~R
- ~(A&B)vC and ~C => ~Av~B
- PvQv~R and (~P&~Q)v(S&~Q&R) => Sv~R
- {no prem} => ~(A&B)v~(~A&C)
- ~(AvB)v~(~~AvC) => ~A
- ~(AvB)v~(~~AvC) => ~Bv~C
- ~(P&Q)vR and P&~R => ~Q
- ~(PvQ)vR and P&Q => R
- (P&Q)vR and ~Pv~Q => R
- {no prem} => ~Pv~Qv(P&Q)
- {no prem} => (P&~Q)v~Pv~~Q
- {no prem} => (~P&~~Q&~R)vPv~Qv~~R
- ~(PvQvR) => ~(QvR)
- ~((AvC)&B) => ~(~~A&(B&D))
- ~((PvQ)&(RvS)) => ~(P&S)
- ~(~~P&Q) => ~(P&~~Q&R)
- ~(QvR) and ~P => ~(PvQvR)
- {no prem} => ~((Pv~Q)&~P&Q)
- {no prem} => ~Pv((PvQ)&(PvR))
- PvQ, ~Qv~R and RvS => PvS
- Pv(Q&~R) and ~QvRvS => PvS
PROP Problems
Level 1
- (Q->P)&~~Q => P
- {no prem} => P->P
- ~P&Q => P->R
- {no prem} => ~~P->P
- P->Q and ~Q => ~P
- {no prem} => (~~P&Q)->(PvR)
- Pv~Q => ~P->~Q
- P<->~Q => (~~~Q&R)->PvS
- {no prem} => (P&~P)->Q
- {no prem} => (~P&Q&#)->P
- {no prem} => ~~(P&Q)->P
- {no prem} => P->(PvR)
- {no prem} => P->~~P
- {no prem} => (~P&R)->(~Q->~Q)
- {no prem} => P->(Q->Q)
- {no prem} => ~(Q->Q)->#
- P->Q, Q->R and R->S => P->S
- P->Q => P->(QvR)
- {no prem} => ~P<->~~~P
- P<->Q => (P->Q)&(Q->P)
- (P->Q)&(Q->P) => P<->Q
- (PvQ)->R and (RvS)->T => Q->T
- P->(Q&~R) and ~R->S => (P&T)->S
- (Pv~Q)->(~R&S) and (~RvT)->U => (~Q&M)->(UvN)
- P->Q and P->~Q => R->~P
- ~A->(B&C) and D->~C => D->A
- ~PvQ => (P&R)->Q
- P->(Q&R) => ~PvQ
- (PvQ)->R => ~PvR
- P->Q, (RvS)->P and S&T => P&Q
- P->Q, Q->R and P => R
- A<->B and B<->C => A<->C
- P<->Q => Q<->P
- Pv~Q, P->R and ~Q->R => R
- P and ~Q => ~(P->Q)
- Q->R and P->~R => ~(P&Q)
- PvQ, P->R and P->~R => Q
- (P&Q)->R and P&~R => ~Q
- P->(QvR) and ~Q&P => R
- (BvC)->(A->G), (BvE)->(G->D) and B&~H => A->D
Level 2
- (PvQ)->~R => R->~P
- {no prem} => ~P->((Q&R)->~P)
- P<->(~QvR) => R->~~P
- (~Q->~P)&(Q->P) => P<->Q
- ~(A&B) => A->~B
- {no prem} => P->(Q->(PvR))
- P->R, Q->R and PvQ => R
- {no prem} => (P&Q)->(R->Q)
- P->Q and P->R => P->(Q&R)
- (P->Q)v(P->R) => P->(QvR)
- {no prem} => Q->(P->P)
- (P&Q)<->R => ((P&Q)v(Q&P))<->R
- {no prem} => P->((Q&R)->P)
- {no prem} => ~P->((QvR)->~P)
- P->~Q => ~(P&Q)
- P->Q => ~PvQvR
- (P&S)vQ and Q->(R&S) => S
- {no prem} => (~P->Q)->((Q->P)->P)
- (A&B)->C => A->(~C->~B)
- {no prem} => (~P->Q)->((~P->~Q)->P)
- {no prem} => (P->~Q)->((P->Q)->~P)
- {no prem} => (P&Q)->(R->(P&Q&R))
- (~Q->~P)&(~P->~Q) => P<->Q
- {no prem} => (P&Q)->(R->((PvS)&(QvS)))
- {no prem} => ~(PvQvR)->~Q
- ~PvQ and ~QvP => P<->Q
- {no prem} => ((P&R)v~~Q)->(~R->Q)
- {no prem} => (PvQ)->(~Q->P)
- A->B => ~(BvC)->~A
- {no prem} => (P&Q)->(~P->R)
- P->(~Q->~R) and P&R => Q
- {no prem} => ~(P&Q)->(P->~Q)
- (P&Q)v(~P&~Q) => P<->Q
- (P&R)->Q and (PvS)->~Q => R->~P
- Q<->~Q => #
- {no prem} => (P->Q)<->(~Q->~P)
- ~P<->Q => P<->~Q
- ~P<->Q => ~(P<->Q)
- {no prem} => (P->Q)<->~(P&~Q)
- {no prem} => (P->Q)<->(~PvQ)
- {no prem} => (P->(Q->R))<->((P&Q)->R)
- PvQ, (P&R)->S and P->~S => ~Q->~R
- P<->(~Q<->~R) and P => Q->R
- (~PvQ)->(RvS), P->R and ~R => S
Level 3
- ~(A->B) => ~(~AvB)
- {no prem} => ((P&R)->Q)->((P->R)->(P->Q))
- ~(P->Q) => P&~Q
- ~P->Q and P->Q => Q
- P->(QvR) and ~(P->Q) => R
- P->(QvR) => (P->Q)v(P->R)
- (P&Q)<->R and P->Q => P<->R
- PvQ, ~QvR and ~RvS => PvS
- PvQ and ~QvR => PvR
- (P&T)vQ, ~QvR and ~Rv(S&T) => TvU
- (P&S)vQ and ~Qv(R&S) => S
- {no prem} => (P->(Q->R))->(~(P->R)->~(P->Q))
- {no prem} => (~(Q->R)->~P)->((P->Q)->(P->R))
- {no prem} => (P->(Q->R))->((P->Q)->(~R->~P))
- {no prem} => (P->(Q->R))->((P->R)->(P->Q))
- ~(P->Q) => ~(~~Qv~P)
- {no prem} => ((P&R)->Q)->((~R->~P)->(P->Q))
- {no prem} => ~(Pv(Q&~R))->((~R&Q)->T)
- {no prem} => ~(PvQvR)->((R&S)->T)
- ~(P->~Q) => ~~Q&P
- {no prem} => ((P&R)v~~Q)->~(~R&~Q)
- {no prem} => ~(P&Q)->(~Pv~Q)
- {no prem} => Q->(~Pv(P&Q))
- P&(Qv~~R) => ~(P&Q)->(P&R)
- ~(P&Q)->(P&R) => P&(Qv~~R)
- ~((P&Q)v~(~P->Q)) => ~P<->Q
- ~((P&Q)v~(~P->Q)) => ~(P<->Q)
- ~(~P->Q)v~(P->~Q) => P<->Q
- (P&Q)v~(P->~Q) => P<->Q
- P<->Q => (P&Q)v(~P&~Q)
- ~(P<->Q) => ~((P&Q)v(~P&~Q))
- ~((P&Q)v(~P&~Q)) => ~(P<->Q)
- ~((P->Q)&(Q->P)) => ~(P<->Q)
- ~((P&R)->(QvS)) => ~(~PvQ)
- ~(P<->Q) => ~P<->Q
- ~(~P<->Q) => ~(P<->~Q)
- {no prem} => ~(P->Q)<->(P&~Q)
FOL Problems
Level 1
- AxR(x,a) => ExR(x,a)
- Ax(P(x)&Q(x)) => AxQ(x)
- Ax(P(x)&Q(x)) and P(b)->R(b,a) => R(b,a)
- AxP(x) => AyP(y)
- ExP(x) => EzP(z)
- AxP(x), AxQ(x) and Ax((P(x)&Q(x))->R(x)) => AxR(x)
- Ax(P(x)vQ(x)) and Ax(P(x)->R(x)) => Ax(Q(x)vR(x))
- Ex(P(x)&~Q(x)) => Ex~(~P(x)vQ(x))
- P(a) and R(a,b) => ExP(x)&ExR(x,b)
- P(a) and R(a,b) => Ex(P(x)&R(x,b))
- Q(a,b,c) => ExEyQ(x,y,c)
- P(a)&AxQ(x) and Ax((P(x)&Q(x))->R(x)) => ExR(x)
- Ax(P(x)vQ(x)) and ~Q(b) => ExP(x)
- AxP(x)vAxQ(x) and ~Q(b) => P(b)
- AxP(x)vAxQ(x) and ~Q(b) => AxP(x)
- Ax~~P(x) => AxP(x)
- Ex~~P(x) => ExP(x)
- AxP(x) => Ax~~P(x)
- ExP(x) => Ex~~P(x)
- Ex~(~P(x)vQ(x)) => Ex(P(x)&~Q(x))
- Ax(P(x)&Q(x)) => Ax(Q(x)&P(x))
- Ex(P(x)&Q(x)) => Ex(Q(x)&P(x))
- Ax(P(x)vQ(x)) => Ax(Q(x)vP(x))
- Ex(P(x)vQ(x)) => Ex(Q(x)vP(x))
- Ax(P(x)->~Q(x)) and Q(a) => ~AxP(x)
- Ax(P(x)&(Q(x)vR(x))) => Ax((P(x)&Q(x))v(P(x)&R(x)))
- Ax((P(x)&Q(x))v(P(x)&R(x))) => Ax(P(x)&(Q(x)vR(x)))
- Ex(P(x)&(Q(x)vR(x))) => Ex((P(x)&Q(x))v(P(x)&R(x)))
- Ex((P(x)&Q(x))v(P(x)&R(x))) => Ex(P(x)&(Q(x)vR(x)))
- {no prem} => (a=b&b=c)->a=c
- a=b => b=a
- {no prem} => a=av~(a=a)
- {no prem} => a=bv~(a=b)
- {no prem} => a=bv~(b=a)
Level 2
- ~ExP(x) => Ax~P(x)
- Ax(P(x)->~Q(x)) => ~Ex(P(x)&Q(x))
- Ax(~P(x)vQ(x)) => ~Ex(P(x)&~Q(x))
- Ex(P(x)&~Q(x)) => ~Ax(P(x)->Q(x))
- Ax(P(x)->Q(x)) => ~Ex(P(x)&~Q(x))
- Ax~(P(x)->Q(x)) => Ax(P(x)&~Q(x))
- Ax(P(x)->Q(x)) => Ax~(P(x)&~Q(x))
- Ax(P(x)->Q(x)) => ~Ex~(~P(x)vQ(x))
- {no prem} => Ax(~P(x)v~(Q(x)&(~P(x)v~Q(x))))
- {no prem} => AxP(x)v~AyP(y)
- {no prem} => ExP(x)v~EyP(y)
- {no prem} => Ex(P(x)v~P(x))
- {no prem} => Ax(P(x)v~P(x))
- ~ExP(x) => ~EyP(y)
- ~AxP(x) => ~AyP(y)
- Ex(P(x)&Q(x)) => Ex(P(x)&EyQ(y))
- Ax(P(x)&Q(x)) => Ax(P(x)&AyQ(y))
- {no prem} => Ax((x=b&b=c)->x=c)
- Ex(~P(x)v~Q(x)) => ~Ax(P(x)&Q(x))
- Ax~(P(x)v~Q(x)) => AxQ(x)
- Ax~(P(x)v~Q(x)) => Ax(~P(x)&Q(x))
- Ax~(P(x)v~Q(x)) => Ax~P(x)&AxQ(x)
- ~Ex(P(x)v~Q(x)) => Ax~P(x)
- ~Ex(P(x)v~Q(x)) => Ax(~P(x)&Q(x))
- ~Ex(P(x)&Q(x)) => Ax(~P(x)v~Q(x))
Level 3
- ~AxP(x) => Ex~P(x)
- ~Ex(P(x)&~Q(x)) => Ax(P(x)->Q(x))
- ~Ex(P(x)&~Q(x)) => Ax(~P(x)vQ(x))
- ~Ax(P(x)->Q(x)) => Ex(P(x)&~Q(x))
- ~Ax~(P(x)->Q(x)) => ~Ax(P(x)&~Q(x))
- ~Ex~(~P(x)vQ(x)) => ~Ex(P(x)&~Q(x))
- ~Ax(P(x)->Q(x)) => Ex~(~P(x)vQ(x))
- {no prem} => Ex(P(x)->AyP(y)) Drunkard’s paradox
- ~Ax(P(x)&Q(x)) => Ex(~P(x)v~Q(x))
