Re: Need help with simple FOL proof -- without using existential quantifiers

In article <1169676603.136676.323530@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
"Dan Christensen" <dchris@xxxxxxxxx> wrote:

I want to prove

~Aa ~Ab R(a,b) -> Ab ~Aa ~R(a,b)

without making use of existential quantifiers.

Any help would be appreciated.

Dan

It would help to know your axioms and rules of inferences.

Here is a stab at a proof.

Ab R(a,b) -> R(a,b) -- note that last 'b' is not same as the other b's

~R(a,b) -> ~Ab R(a,b) -- contrapositive

[Aa ~R(a,b)] -> [Aa ~Ab R(a,b)] -- generalization

[~Aa ~Ab R(a,b)] -> [~Aa ~R(a,b)] -- contrapositive

Ab[~Aa ~Ab R(a,b)] -> Ab[~Aa ~R(a,b)] -- generalization

But b is not free in the hypothesis [~Aa ~Ab R(a,b)],
so it has no effect: ie,

[~Aa ~Ab R(a,b)] -> Ab[~Aa ~Ab R(a,b)] -- bound variable rule

Hence,

[~Aa ~Ab R(a,b)] -> Ab[~Aa ~R(a,b)] QED
.