1. trans=( r)(y)(Va)((R(, y)A R(y, a ))+R(a, a)), 2. sym=(Va)(Vy)(R(a, y)+ R(y, r)) 3. ref=(V)R(, a 20mtr20= (Va) y)(a, y) Then itrans, sym, nontriu ref Proof. We now prove that iT,S, N) R We have the following tableaux as Figure 1. It is a FVaR(c, c) FR(e, c), new c TVr=yR(, v) TR(e, d),new vrvy(R(x,y)→R(y,x) Ty(Rcy)→R(,c (R(cd)→R(d,c) y(R(xy)∧R2)→R(x2 Yy:(Rcy)∧R(,2)→R(c2 v:(R(c山)∧Ra2)→R(c2) TR(cd)∧R(ac)→R(cl PFR(cd∧R(dcl FR( d. c) (Rcd)→Ra R(cd⑦Ra,c Figure 1: The tableau proof tableau proof. It is pro1. trans = (∀x)(∀y)(∀z)((R(x, y) ∧ R(y, z)) → R(x, z)), 2. sym = (∀x)(∀y)(R(x, y) → R(y, x)), 3. ref = (∀x)R(x, x), 4. nontriv = (∀x)(∃y)R(x, y). Then {trans, sym, nontriv} |= ref. Proof. We now prove that {T, S, N} |= R.We have the following tableaux as Figure 1. It is a F∀xR(x, x) F R(c, c), new c T∀x∃yR(x, y) T∃yR(c, y) T R(c, d), new d T∀x∀y(R(x, y) → R(y, x)) T∀y(R(c, y) → R(y, c)) T(R(c, d) → R(d, c)) T∀x∀y∀z(R(x, y) ∧ R(y, z) → R(x, z)) T∀y∀z(R(c, y) ∧ R(y, z) → R(c, z)) T∀z(R(c, d) ∧ R(d, z) → R(c, z)) T R(c, d) ∧ R(d, c) → R(c, c) F R(c, d) ∧ R(d, c) F R(c, d) × F R(d, c) T(R(c, d) → R(d, c)) F R(c, d) × T R(d, c) × T R(c, c) × Figure 1: The tableau proof tableau proof. It is proved. 2