Quantifiers: Atomic Tableaux AFavp(v)+ for some ground term t, AFp(t) 7(彐x)y( T( for a new constant c
Quantifiers: Atomic Tableaux A |= ∃vϕ(v ) ⇔ for some ground term t, A |= ϕ(t). T(∃x)ϕ(x) Tϕ(c) for a new constant c Yi Li (Fudan University) Discrete Mathematics June 5, 2012 6 / 25
Quantifiers: Atomic Tableaux AVp(v)+ for all ground term t, AFp(t) T(Vxp( for any ground term t of cc
Quantifiers: Atomic Tableaux A |= ∀vϕ(v ) ⇔ for all ground term t, A |= ϕ(t). T(∀x)ϕ(x) Tϕ(t) for any ground term t of LC Yi Li (Fudan University) Discrete Mathematics June 5, 2012 7 / 25
Quantifiers: Atomic Tableaux F(xp(x) F(彐x)y(x) for a new constant c for any ground term t of lc
Quantifiers: Atomic Tableaux F(∀x)ϕ(x) Fϕ(c) for a new constant c F(∃x)ϕ(x) Fϕ(t) for any ground term t of LC Yi Li (Fudan University) Discrete Mathematics June 5, 2012 8 / 25