Textbook Content

Expand All
1 of 2
Proof Machine
Proof
Toggle Machines
1.
2.
3.
4.
5.
6.

BOOL Level 1

  • P&~Q and (RvS)&~T => ~T&P
  • ~~(~~P&Q)&~R => P
  • P&(Q&R)&S => (RvT)&(RvU)
  • ~~~P => (~Pv~Q)v(RvS)
  • ~~~~A => A
  • P&Q => Q&P
  • ~~Pv~~P => P
  • Av(B&C) => CvA
  • {no prem} => ~(~~P&~P)
  • ~~~A => ~A
  • ~A => ~~~A
  • ~B => ~(A&B)
  • PvQ and ~Q => Pv~R
  • ~~P&(~~Q&R)&S => TvQ
  • (P&~P)v(Q&~Q)v(R&~R) => #
  • ~P and Q => ~(Pv~Q)
  • {no prem} => ~(P&(~~~P&Q))
  • P&Q&~~R => R&Q
  • P&~~(Q&~~R) => QvS
  • 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)
  • (P&Q)v~~P => P
  • A&~B&# => C
  • ~(AvB) => ~A
  • ~(A&B) and A => ~B

BOOL Level 2

  • ~(~CvD) => C&~D
  • ~(~~Pv~~~Q) => ~P&Q
  • 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&~R) => ~(Q&~~P&~R)
  • ~(Pv~~Qv~R) => ~(Qv~~Pv~R)
  • ~Pv(P&Q) => Qv~P
  • ~(~~A&B) => ~(A&~~B)
  • ~(~~A&~B) => ~Av~~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)

BOOL Level 3

  • {no prem} => ~Pv~(Q&~(P&Q))
  • ~(~C&D) => Cv~D
  • ~(P&Q&~R) => ~Pv~QvR
  • (A&~~B)vB and ~(C&B) => ~C
  • ~PvQ, ~QvR, ~R => ~P
  • {no prem} => ~Pv~(~Q&(~PvQ))
  • (~PvQ)&(RvS), PvT, ~T => Q
  • (~AvB)&~C, ~EvA, ~(~EvB)vD => DvB
  • P&Q&~R, ~PvRvS, ~SvR => #
  • ~~A&(~BvC) => (A&~B)v(A&C)
  • AvB, ~~AvC => Av(B&~~C)
  • AvB, CvD => (A&C)v(A&D)v(B&C)v(B&D)
  • (A&B)v(C&D) => (AvC)&(AvD)&(BvC)&(BvD)
  • (AvC)&(AvD), (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, (~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 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, 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), (~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, 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, ~Q->R => R
  • P and ~Q => ~(P->Q)
  • Q->R and P->~R => ~(P&Q)
  • PvQ, P->R, P->~R => Q
  • (P&Q)->R and P&~R => ~Q
  • P->(QvR) and ~Q&P => R
  • (BvC)->(A->G), (BvE)->(G->D), B&~H => A->D
  • {no prem} => ~(BvA)->~(AvB)
  • {no prem} => ~(B&A)->~(A&B)
  • {no prem} => ~(B&A)<->(~Av~B)

PROP Level 2

  • (PvQ)->~R => R->~P
  • ~(A&B) => A->~B
  • {no prem} => ~P->((Q&R)->~P)
  • P<->(~QvR) => R->~~P
  • (~Q->~P)&(Q->P) => P<->Q
  • {no prem} => P->(Q->(PvR))
  • P->R, Q->R, 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, 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, (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, P->~S => ~Q->~R
  • P<->(~Q<->~R), P => Q->R
  • (~PvQ)->(RvS), P->R, ~R => S
  • ~(A->B) => ~B
  • ~(~A->B) => ~A

PROP Level 3

  • {no prem} => ((P&R)->Q)->((P->R)->(P->Q))
  • ~(A->B) => ~(~AvB)
  • ~(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, ~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 Level 1

  • Ax(P(x)->R(x,a)) and P(a) => ExR(x,x)
  • Ax(R(a,x)&S(x,x)) => ExR(x,b)
  • AxP(x)&AxR(b,x) => ExR(x,x)
  • P(a) => Ax(P(x)->Q(x))->Ex(P(x)&Q(x))
  • AxR(x,a) => ExR(x,a)
  • Ax(P(x)&Q(x)) => AxQ(x)
  • Ax(P(x)&Q(x)), P(b)->R(b,a) => R(b,a)
  • AxP(x) => AyP(y)
  • ExP(x) => EzP(z)
  • AxP(x), AxQ(x), Ax((P(x)&Q(x))->R(x)) => AxR(x)
  • Ax(P(x)vQ(x)), 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), Ax((P(x)&Q(x))->R(x)) => ExR(x)
  • Ax(P(x)vQ(x)), ~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)))
  • e=d, L(a,b,c,d), a=f => L(f,b,c,e)
  • {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)
  • Ax~(P(x)&Q(x)) and AxP(x) => Ax~Q(x)
  • Ax~(P(x)&Q(x)) => Ax(~P(x)v~Q(x))
  • {no prem} => Ax(~(P(x)->P(x))->#)
  • ~ExP(x) => ~P(b)
  • ~ExP(x) => ~(P(b)&Q(a))

FOL Level 2

  • {no prem} => Ax((P(x)&Q(x))->Q(x))
  • Ax~Q(x), Ax(Q(x)vR(x)) => AxR(x)
  • Ax~Q(x) => Ax~(Q(x)&R(x))
  • Ex(~~P(x)&~~Q(x)) => Ex(Q(x)&P(x))
  • Ax(P(x)->Q(x)), Ex~Q(x) => Ex~P(x)
  • Ex~(P(x)->Q(x)) => ExP(x)
  • Ax((P(x)vQ(x))->R(x)), Ax~R(x) => ~ExP(x)
  • Ax~R(x,x), R(b,a) => ~(a=b)
  • {no prem} => (a=b&P(a))->(P(b)vP(c))
  • 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)
  • 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))
  • {no prem} => Ax~(P(x)&Q(x))<->Ax~(Q(x)&P(x))
  • {no prem} => Ax~(P(x)&Q(x))<->Ax(~P(x)v~Q(x))

FOL Level 3

  • Ax((P(x)vQ(x))->#) => ~ExQ(x)
  • ~Ex(P(x)vQ(x)vR(x)) => Ax~(R(x)&S(x))
  • ~AxP(x) => Ex(~P(x)vQ(x)vR(x))
  • ~ExP(x) => Ax~P(x)
  • (a=b)v(c=d), ~(d=c)v(a=b) => b=a
  • ~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))
  • {no prem} => Ax~(P(x)&Q(x))<->Ax~(Q(x)&(P(x)vR(x))
  • {no prem} => ~Ax~(P(x)&Q(x))<->~Ax~(Q(x)&P(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 paradox
  • ~Ax(P(x)&Q(x)) => Ex(~P(x)v~Q(x))
  • ~Ax(P(x)vQ(x)) => Ex(~P(x)&~Q(x))
  • ~Ax(P(x)->Q(x)) => Ex(P(x)&~Q(x))
Messages

Tutorials

Videos coming soon.

Videos coming soon.