Re: FO logic without equality



David C. Ullrich wrote:

Exactly what part of that pdf do you think says that
it doesn't matter? That it doesn't matter _to_ _this_
_question_, not that it doesn't matter for some
_other_ purpose.

The papers say:

S u EQ_AX satisfiable iff S normal satisifiable

From this follows what I said:

T u EQ_AX |- A iff T |-_= A

Proof:

By (normal) completness:
S u EQ_AX satisfiable <=>
S u EQ_AX consistent <=>
S normal satisfiable <=>
S normal consistent

Further
T u EQ_AX |- A <=>
T u EQ_AX u ~A not consistent <=>
T u ~A not normal consistent <=>
T |-_= A

Bye
.

Loading