|
ALLx (Fx IMP Gx), ⊢ NOTSOMEx (Fx AND NOTGx)
|
SH {Sample tableau 1}
ST {ALL x (Fx IMP Gx) ⊢ NOT SOME x (Fx AND NOT Gx)}
TL {t} {ALL x (Fx IMP Gx)}
TL {f} {NOT SOME x (Fx AND NOT Gx)}
SN
TL {t} {SOME x (Fx AND NOT Gx)}
SN
TL {t} {Fa AND NOT Ga}
SN
TL {t} {Fa}
TL {t} {NOT Ga}
SN
TL {f} {Ga}
SN
TL {t} {Fa IMP Ga}
SN
TL {f} {Fa}
EN
SN
TL {t} {Ga}
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
NOTSOMEx (Fx AND NOTGx) ⊢ ALLx (Fx IMP Gx)
|
SH {Sample tableau 2}
ST {NOT SOME x (Fx AND NOT Gx) ⊢ ALL x (Fx IMP Gx)}
TL {t} {NOT SOME x (Fx AND NOT Gx)}
TL {f} {ALL x (Fx IMP Gx)}
SN
TL {f} {SOME x (Fx AND NOT Gx)}
SN
TL {f} {Fa IMP Ga}
SN
TL {t} {Fa}
TL {f} {Ga}
SN
TL {f} {Fa AND NOT Ga}
SN
TL {f} {Fa}
EN
SN
TL {f} {NOT Ga}
SN
TL {t} {Ga}
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLx (Fx IMP Gx), SOMEx (Gx AND Hx) ⊢ SOMEx (Fx AND Hx)
|
SH {Sample tableau 3}
ST {ALL x (Fx IMP Gx), SOME x (Gx AND Hx) ⊢ SOME x (Fx AND Hx)}
TL {t} {ALL x (Fx IMP Gx)}
TL {t} {SOME x (Gx AND Hx)}
TL {f} {SOME x (Fx AND Hx)}
SN
TL {t} {Ga AND Ha}
SN
TL {t} {Ga}
TL {t} {Ha}
SN
TL {t} {Fa IMP Ga}
SN
TL {f} {Fa AND Ha}
SN
TL {f} {Fa}
EN
SN
TL {f} {Ha}
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLx (Fx IMP Gx), ALLx (Gx IMP Hx) ⊢ ALLx (Fx IMP Hx)
|
SH {Sample tableau 4}
ST {ALL x (Fx IMP Gx), ALL x (Gx IMP Hx) ⊢ ALL x (Fx IMP Hx)}
TL {t} {ALL x (Fx IMP Gx)}
TL {t} {ALL x (Gx IMP Hx)}
TL {f} {ALL x (Fx IMP Hx)}
SN
TL {f} {Fa IMP Ha}
SN
TL {t} {Fa IMP Ga}
SN
TL {t} {Ga IMP Ha}
SN
TL {t} {Fa}
TL {f} {Ha}
SN
TL {f} {Fa}
EN
SN
TL {t} {Ga}
SN
TL {f} {Ga}
EN
SN
TL {t} {Ha}
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLx (Fx IMP Gx), SOMEx (Hx AND NOTGx) ⊢ SOMExNOT(Fx OR NOTHx)
|
SH {Sample tableau 5}
ST {ALL x (Fx IMP Gx), SOME x (Hx AND NOT Gx) ⊢ SOME x NOT (Fx OR NOT Hx)}
TL {t} {ALL x (Fx IMP Gx)}
TL {t} {SOME x (Hx AND NOT Gx)}
TL {f} {SOME x NOT (Fx OR NOT Hx)}
SN
TL {t} {Ha AND NOT Ga}
SN
TL {t} {Ha}
TL {t} {NOT Ga}
SN
TL {f} {Ga}
SN
TL {t} {Fa IMP Ga}
SN
TL {f} {Fa}
SN
TL {f} {NOT(Fa OR NOT Ha)}
SN
TL {t} {Fa OR NOT Ha}
SN
TL {t} {Fa}
EN
SN
TL {t} {NOT Ha}
SN
TL {f} {Ha}
EN
EN
EN
EN
EN
SN
TL {t} {Ga}
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLx (Fx IMP Hx), ALLx (Gx IMP Hx) ⊢ SOMEx (Fx OR Gx)
|
SH {Sample tableau 6}
ST {ALL x (Fx IMP Hx), ALL x (Gx IMP Hx) ⊢ SOME x (Fx OR Gx)}
TL {t} {ALL x (Fx IMP Hx)}
TL {t} {ALL x (Gx IMP Hx)}
TL {f} {SOME x (Fx OR Gx)}
SN
TL {t} {Fa IMP Ha}
SN
TL {t} {Ga IMP Ha}
SN
TL {f} {Fa OR Ga}
SN
TL {f} {Fa}
TL {f} {Ga}
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
SOMExNOTFx OR SOMExGx ⊢ SOMEx (Fx IMP Gx)
|
SH {Sample tableau 7}
ST {SOME x NOT Fx OR SOME x Gx ⊢ SOME x (Fx IMP Gx)}
TL {t} {SOME x NOT Fx OR SOME x Gx}
TL {f} {SOME x (Fx IMP Gx)}
SN
TL {t} {SOME x NOT Fx}
SN
TL {t} {NOT Fa}
SN
TL {f} {Fa}
SN
TL {f} {Fa IMP Ga}
SN
TL {t} {Fa}
TL {f} {Ga}
EN
EN
EN
EN
EN
SN
TL {t} {SOME x Gx}
SN
TL {t} {Ga}
SN
TL {f} {Fa IMP Ga}
SN
TL {t} {Fa}
TL {f} {Ga}
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLx (Fx OR Gx) ⊢ ALLxFx OR SOMExGx
|
SH {Sample tableau 8}
ST {ALL x (Fx OR Gx) ⊢ ALL x Fx OR SOME x Gx}
TL {t} {ALL x (Fx OR Gx)}
TL {f} {ALL x Fx OR SOME x Gx}
SN
TL {f} {ALLxFx}
TL {f} {SOME x Gx}
SN
TL {f} {Fa}
SN
TL {f} {Ga}
SN
TL {t} {Fa OR Ga}
SN
TL {t} {Fa}
EN
SN
TL {t} {Ga}
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
SOMExFx AND SOMExGx ⊢ SOMEx (Fx AND Gx)
|
SH {Sample tableau 9}
ST {SOME x Fx AND SOME x Gx ⊢ SOME x (Fx AND Gx)}
TL {t} {SOME x Fx AND SOME x Gx}
TL {f} {SOME x (Fx AND Gx)}
SN
TL {t} {SOME x Fx}
TL {t} {SOME x Gx}
SN
TL {t} {Fa}
SN
TL {f} {Fa AND Ga}
SN
TL {f} {Fa}
EN
SN
TL {f} {Ga}
SN
TL {t} {Gb}
SN
TL {f} {Fb AND Gb}
SN
TL {f} {Fb}
EN
SN
TL {f} {Gb}
EN
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLxSOMEy Rxy ⊢ SOMExALLy (Rxy OR Ryx)
|
SH {Sample tableau 10}
ST {ALL x SOME y Rxy ⊢ SOME x ALL y (Rxy OR Ryx)}
TL {t} {ALL x SOME y Rxy}
TL {f} {SOME x ALL y (Rxy OR Ryx)}
SN
TL {t} {SOME y Ray}
SN
TL {f} {ALL y (Ray OR Rya)}
SN
TL {t} {Raa}
SN
TL {f} {Rab OR Rba}
SN
TL {f} {Rab}
TL {f} {Rba}
SN
TL {t} {SOME y Rby}
SN
TL {t} {Rbb}
SN
TL {f} {ALL y (Rby OR Ryb)}
SN
TL {f} {Rba OR Rab}
EN
EN
EN
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLx(Fx OR Gx), ALLx(Gx IMP Hx) ⊢ ALLx(NOTHx IMP Fx)
|
SH {Sample tableau 11}
ST {ALL x (Fx OR Gx), ALL x (Gx IMP Hx) ⊢ ALL x (NOT Hx IMP Fx)}
TL {t} {ALL x (Fx OR Gx)}
TL {f} {ALL x (Gx IMP Hx)}
SN
TL {f} {NOT Ha IMP Fa}
SN
TL {t} {NOT Ha}
TL {f} {Fa}
SN
TL {f} {Ha}
SN
TL {t} {Fa OR Ga}
SN
TL {t} {Fa}
EN
SN
TL {t} {Ga}
SN
TL {t} {Ga IMP Ha}
SN
TL {f} {Ga}
EN
SN
TL {t} {Ha}
EN
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLxSOMEy Rxy ⊢ SOMExSOMEy (Rxy AND Ryx)
|
SH {Sample tableau 12}
ST {ALL x SOME y Rxy ⊢ SOME x SOME y (Rxy AND Ryx)}
TL {t} {ALL x SOME y Rxy}
TL {f} {SOME x SOME y (Rxy AND Ryx)}
SN
TL {t} {SOME y Ray}
SN
TL {f} {SOME y (Ray AND Rya)}
SN
TL {f} {Raa AND Raa}
SN
TL {f} {Raa}
SN
TL {t} {Rab}
SN
TL {t} {SOME y Rby}
SN
TL {f} {SOME y (Rby AND Ryb)}
SN
TL {f} {Rab AND Rba}
SN
TL {f} {Rab}
EN
SN
TL {f} {Rba}
SN
TL {f} {Rba AND Rab}
SN
TL {f} {Rbb AND Rbb}
SN
TL {f} {Rbb}
SN
TL {t} {Rbc}
SN
TL {t} {SOME y Rcy}
SN
TL {f} {SOME y (Rcy AND Ryc)}
SN
TL {f} {Rbc AND Rcb}
SN
TL {f} {Rbc}
EN
SN
TL {f} {Rcb}
SN
TL {f} {Rcb AND Rbc}
SN
TL {f} {Rcc AND Rcc}
SN
TL {f} {Rcc}
SN
TL {t} {Rca}
SN
TL {f} {Rac AND Rca}
SN
TL {f} {Rac}
SN
TL {f} {Rca AND Rac}
EN
EN
SN
TL {f} {Rca}
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLxALLyALLz((Rxy AND Ryz) IMP Rxz), ALLxALLy(Rxy IMP Ryx), ALLxSOMEy Ryx ⊢ ALLx Rxx
|
SH {Sample tableau 13}
ST {ALL x ALL y ALL z ((Rxy AND Ryz) IMP Rxz), ALL x ALL y (Rxy IMP Ryx), ALL x SOME y Ryx ⊢ ALL x Rxx}
TL {t} {ALL x ALL y ALL z ((Rxy AND Ryz) IMP Rxz)}
TL {t} {ALL x ALL y (Rxy IMP Ryx)}
TL {t} {ALL x SOME y Ryx}
TL {f} {ALL x Rxx}
SN
TL {f} {Raa}
SN
TL {t} {SOME y Rya}
SN
TL {t} {Rba}
SN
TL {t} {ALL y (Rby IMP Ryb)}
SN
TL {t} {Rba IMP Rab}
SN
TL {f} {Rba}
EN
SN
TL {t} {Rab}
SN
TL {t} {ALL y ALL z ((Ray AND Ryz) IMP Raz)}
SN
TL {t} {ALL z ((Rab AND Rbz) IMP Raz)}
SN
TL {t} {(Rab AND Rba) IMP Raa}
SN
TL {f} {Rab AND Rba}
SN
TL {f} {Rab}
EN
SN
TL {f} {Rba}
EN
EN
SN
TL {t} {Raa}
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|
|
ALLxALLy(Rxy IMP >Sxy), ALLxALLy(Sxy IMP Syx) ⊢ ALLxALLy(Rxy IMP Ryx)
|
SH {Sample tableau 14}
ST {ALL x ALL y (Rxy IMP Sxy), ALL x ALL y (Sxy IMP Syx) ⊢ ALL x ALL y (Rxy IMP Ryx)}
TL {t} {ALL x ALL y (Rxy IMP Sxy)}
TL {t} {ALL x ALL y (Sxy IMP Syx)}
TL {f} {ALL x ALL y (Rxy IMP Ryx)}
SN
TL {f} {ALL y (Ray IMP Rya)}
SN
TL {f} {Rab IMP Rba}
SN
TL {t} {Rab}
TL {f} {Rba}
SN
TL {t} {ALL y (Ray IMP Say)}
SN
TL {t} {ALL y (Rby IMP Sby)}
SN
TL {t} {ALL y (Say IMP Sya)}
SN
TL {t} {ALL y (Sby IMP Syb)}
SN
TL {t} {Rab IMP Sab}
SN
TL {f} {Rab}
EN
SN
TL {t} {Sab}
SN
TL {t} {Sab IMP Sba}
SN
TL {f} {Sab}
EN
SN
TL {t} {Sba}
SN
TL {t} {Sba IMP Sab}
SN
TL {t} {Rba IMP Sba}
SN
TL {t} {Raa IMP Saa}
SN
TL {t} {Rbb IMP Sbb}
SN
TL {t} {Saa IMP Saa}
SN
TL {t} {Sbb IMP Sbb}
SN
TL {f} {Raa}
EN
SN
TL {t} {Saa}
SN
TL {f} {Rbb}
EN
SN
TL {t} {Sbb}
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
EN
ET
EH
|
Try it
|
|
Answer
|