Does the fact
$\lnot {Spouse}({George},{Laura})$ follow from the facts
${Jim}\neq {George}$ and ${Spouse}({Jim},{Laura})$? If so,
give a proof; if not, supply additional axioms as needed. What happens
if we use ${Spouse}$ as a unary function symbol instead of a binary
predicate?
Does the fact $\lnot {Spouse}({George},{Laura})$ follow from the facts ${Jim}\neq {George}$ and ${Spouse}({Jim},{Laura})$? If so, give a proof; if not, supply additional axioms as needed. What happens if we use ${Spouse}$ as a unary function symbol instead of a binary predicate?