Substitutionless first-order logic w/ identity

[techmologist]

I have been trying to familiarize myself with a particular system of first-order logic with identity, in which the process of substitution is achieved by replacing, one at a time, one occurrence of a variable with a term. (see axiom schemes 6) and 7)). I want to use these axioms to prove the properties of equality (identity), namely reflexivity, symmetry, and transitivity. In particular, I'd like to show that they hold for terms, not just variables. A term could be a variable, a constant or some arithmetic composition of variables and constants. But I'm having trouble doing that. First, some preliminaries:

Axiom schemes: each axiom scheme stands for infinitely many individual axioms.

F, G, and H stand for any formulas. x stands for any variable. t stands for any term.\exists x is here taken to be an abbreviation for \neg\forall x \neg.

Propositional calculus:
1)F \supset(G \supset F)
2)(F \supset (G \supset H)) \supset ((F \supset G) \supset (F \supset H))
3)(\neg F \supset \neg G) \supset (G \supset F)

Predicate calculus:
4)\forall x(F \supset G) \supset (\forall x F \supset \forall x G)
5)F \supset \forall x F provided x does not occur in F
6)\exists x (x = t) provided x does not occur in the term t
7)x = t \supset (Y_1 \supset Y_2) where Y₂ is obtained from atomic formula Y₁ by replacing any one occurrence of x with t. An atomic formula is a formula of the form t₁ = t₂, where t₁ and t₂ are terms.


Rules of inference: Modus Ponens and Universal Generalization, i.e. from theorem F infer \forall x F. Here it doesn't matter whether or not x occurs in F.

There are also the axiom schemes for arithmetic and mathematical induction, but I'm leaving them out because I don't think they are important here. I might be wrong about that, though. But it is because of the inclusion of arithmetic that I need to consider terms and not just variables.

I am having trouble proving the usual properties of equality using these axioms. Reflexivity is easy enough:

From 7), we get x=t \supset (x=t \supset t=t).

This is equivalent to

x=t \supset t=t

And from this we can infer

\exists x(x=t) \supset t=t, which gives us the theorem t = t for any term t. I can show a limited form of symmetry:

x=t \supset (x=x \supset t=x)
x=x \supset (x=t \supset t=x)
x=t \supset t=x

But I haven't figured out how to show t=x \supset x=t, much less t_1 = t_2 \supset t_2 = t_1.

Axiom scheme 7) itself gives a limited form of transitivity, i.e.

x=t_1 \supset (x = t_2 \supset t_1=t_2)

But I don't know how to show x=t_1 \supset (t_1=t_2 \supset x = t_2), which I assume is valid. Note that symmetry and transitivity are easily proved when we restrict t to being a variable. But I'm pretty sure these properties of equality are supposed to hold for more general terms. It seems they would have to, or else this method of replacement would not achieve the same results as the more normal method of substitution. Any suggestions on how to prove these? Thanks.

edit: with my old browser, I can't tell, but it looks like the tildes don't show up in LaTeX, so I guess I'll change them to \neg

 

[Preno]

Symmetry:

x=t_1 \rightarrow (x \neq t_2 \rightarrow t_1 \neq t_2), i.e. x=t_1 \rightarrow (t_1=t_2 \rightarrow x=t_2)
x=t_2 \rightarrow (x = t_1 \rightarrow t_2 = t_1), i.e. x=t_1 \rightarrow (x=t_2 \rightarrow t_2 = t_1), therefore
(x=t_1) \rightarrow (t_1=t_2 \rightarrow t_2=t_1), so
\forall x (x=t_1 \rightarrow (t_1=t_2 \rightarrow t_2=t_1)), i.e. (assuming we've chosen x so that x is not free in t_1 or t_2) \exists x (x=t_1) \rightarrow (t_1 = t_2 \rightarrow t_2 = t_1), but
\exists x (x=t_1), therefore
t_1 = t_2 \rightarrow t_2 = t_1

Transitivity is easier:

x=t_1 \rightarrow (t_1 = t_2 \rightarrow x=t_2)
x=t_2 \rightarrow (t_2 = t_3 \rightarrow x=t_3)
(t_1 = t_2) \rightarrow (t_2 = t_3 \rightarrow (x=t_1 \rightarrow x=t_3))
\forall x ((t_1 = t_2) \rightarrow (t_2 = t_3 \rightarrow (x=t_1 \rightarrow x=t_3)))
t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow (t_1=t_1 \rightarrow t_1 = t_3)), but we already know that t_1 = t_1, so:
t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow t_1 = t_3)

Hope I didn't make any blunders there.

 

[techmologist]

Preno, thanks for your reply.

Symmetry:

x=t_1 \rightarrow (x \neq t_2 \rightarrow t_1 \neq t_2), i.e. x=t_1 \rightarrow (t_1=t_2 \rightarrow x=t_2)
x=t_2 \rightarrow (x = t_1 \rightarrow t_2 = t_1), i.e. x=t_1 \rightarrow (x=t_2 \rightarrow t_2 = t_1), therefore
(x=t_1) \rightarrow (t_1=t_2 \rightarrow t_2=t_1), so
\forall x (x=t_1 \rightarrow (t_1=t_2 \rightarrow t_2=t_1)), i.e. (assuming we've chosen x so that x is not free in t_1 or t_2) \exists x (x=t_1) \rightarrow (t_1 = t_2 \rightarrow t_2 = t_1), but
\exists x (x=t_1), therefore
t_1 = t_2 \rightarrow t_2 = t_1

I see what you're doing in the proof of symmetry...I think it is the right idea. But since x \neq t_2 is not an atomic formula, the first line is not an instance of axiom scheme 7). So that line would need to be proved first. Maybe that part is easy and I'm just missing something.

Transitivity is easier:

x=t_1 \rightarrow (t_1 = t_2 \rightarrow x=t_2)
x=t_2 \rightarrow (t_2 = t_3 \rightarrow x=t_3)
(t_1 = t_2) \rightarrow (t_2 = t_3 \rightarrow (x=t_1 \rightarrow x=t_3))
\forall x ((t_1 = t_2) \rightarrow (t_2 = t_3 \rightarrow (x=t_1 \rightarrow x=t_3)))
t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow (t_1=t_1 \rightarrow t_1 = t_3)), but we already know that t_1 = t_1, so:
t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow t_1 = t_3)

In going from the 4th line to the 5th line, it looks like you made use of \forall xF(x) \rightarrow F(t_1). But that is a theorem I haven't been able to prove yet. In fact, I think it depends on the identities we are trying to prove now. However, I can prove

\forall xF(x) \rightarrow F(y) where y is also a variable. It's really inconvenient not having substitution (of terms for variables) as a rule of inference, but apparently it is helpful for theoretical reasons.

 

[Preno]

I see what you're doing in the proof of symmetry...I think it is the right idea. But since x \neq t_2 is not an atomic formula, the first line is not an instance of axiom scheme 7). So that line would need to be proved first. Maybe that part is easy and I'm just missing something.

Ah, you're right.

In going from the 4th line to the 5th line, it looks like you made use of \forall xF(x) \rightarrow F(t_1). But that is a theorem I haven't been able to prove yet. In fact, I think it depends on the identities we are trying to prove now. However, I can prove

\forall xF(x) \rightarrow F(y) where y is also a variable. It's really inconvenient not having substitution (of terms for variables) as a rule of inference, but apparently it is helpful for theoretical reasons.

Well, it is a theorem of classical predicate logic (without identity), and I was assuming that we already know that the system includes classical predicate logic and that identity is the problematic bit. But I see I was mistaken, we do have to use the equality axioms to prove it in this system.

The best I could do is (\sigma \equiv (t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow t_1 = t_3))):

...
t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow (x=t_1 \rightarrow x=t_3))
x=t_1 \rightarrow \sigma (7 + propositional logic)
\forall x (\neg\sigma \rightarrow x \neq t_1)
\forall x (\neg\sigma \rightarrow x \neq t_1) \rightarrow (\neg\forall x x\neq t_1 \rightarrow \neg \forall x \neg \sigma) (axiom 4)
\neg\forall x x \neq t_1 (axiom 6)
\exists x \sigma (where \sigma obviously doesn't include x)

This is a curious system you've got there, I'll have to think about it some more.

[Edit]: ah, I got it:

\neg\forall x \neg \sigma
\neg\sigma\rightarrow \forall x \neg\sigma (axiom 5)
\sigma (propositional logic)

The same trick works for \forall x F(x) \rightarrow F(t):
...
\forall x F(x) \rightarrow F(y) (y not in F except when substituted for x)
y=t \rightarrow (\forall x F(x) \rightarrow F(t)) (axiom 7 + prop. logic)
and you use the same method, this time setting \sigma \equiv \forall x F(x) \rightarrow F(t).

This also proves symmetry, as you already know that x=t_2 \rightarrow t_2=x and can in effect substitute t_1 for x.

edit: out of curiosity, where did you come across this system / who proposed it?

 

[techmologist]

Ah, you're right.
Well, it is a theorem of classical predicate logic (without identity), and I was assuming that we already know that the system includes classical predicate logic and that identity is the problematic bit. But I see I was mistaken, we do have to use the equality axioms to prove it in this system.

Yes, this system is supposed to do all that classical predicate logic does without using substitution as a rule of inference. I am new to all this, but my understanding is that substitution is hard to arithmetize. In other words, find arithmetic statements which state this formula can be derived from that formula(s). The formulas are referenced by their Godel numbers.

The best I could do is (\sigma \equiv (t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow t_1 = t_3))):

...
t_1 = t_2 \rightarrow (t_2 = t_3 \rightarrow (x=t_1 \rightarrow x=t_3))
x=t_1 \rightarrow \sigma (7 + propositional logic)
\forall x (\neg\sigma \rightarrow x \neq t_1)
\forall x (\neg\sigma \rightarrow x \neq t_1) \rightarrow (\neg\forall x x\neq t_1 \rightarrow \neg \forall x \neg \sigma) (axiom 4)
\neg\forall x x \neq t_1 (axiom 6)
\exists x \sigma (where \sigma obviously doesn't include x)

I follow this proof, but doesn't the first line depend on your earlier assumption that
x=t_1 \rightarrow (x \neq t_2 \rightarrow t_1 \neq t_2), which is still in doubt?

This is a curious system you've got there, I'll have to think about it some more.

[Edit]: ah, I got it:

\neg\forall x \neg \sigma
\neg\sigma\rightarrow \forall x \neg\sigma (axiom 5)
\sigma (propositional logic)

Yes.

The same trick works for \forall x F(x) \rightarrow F(t):
...
\forall x F(x) \rightarrow F(y) (y not in F except when substituted for x)
y=t \rightarrow (\forall x F(x) \rightarrow F(t)) (axiom 7 + prop. logic)...

I'm not sure about this part. I have only been able to show that

x=y \rightarrow (F(x) \rightarrow F(y))

When I try to show this with a term t instead of a variable y, I run into trouble when the formula involves negations.

edit: out of curiosity, where did you come across this system / who proposed it?

It is an improvement by Richard Montague and Donald Kalish on an idea of Alfred Tarski's. I came across it in Raymond Smullyan's book, https://www.amazon.com/dp/0195046722/?tag=pfamazon01-20

Here is the abstract of the paper:

http://www.springerlink.com/content/t51u21nk217u581l/

Too bad I don't have free institutional access to the full paper. It's like $34 to buy a copy of it

 

[techmologist]

It seems that

x=t_1 \rightarrow (t_1 = t_2 \rightarrow x = t_2)

is the crucial formula that needs to be proved. Everything else falls in place after that, and we get the same results as classical predicate logic. I can show that it follows from

y=t_1 \rightarrow(x=y \rightarrow (t_1 = t_2 \rightarrow x = t_2)).

Of course, I can't prove this formula (call it \psi) either, but I can show

y=t_2 \rightarrow \psi.

So if it could be shown that y \neq t_2 \rightarrow \psi also holds, that would provide a proof by contradiction. Just trying to lay out some possible lines of attack. This really has me stumped.

 

[techmologist]

It seems that

x=t_1 \rightarrow (t_1 = t_2 \rightarrow x = t_2)

is the crucial formula that needs to be proved. Everything else falls in place after that, and we get the same results as classical predicate logic.

I spoke to soon here. What I really need is another identity formula like axiom scheme 7), but with negations, i.e.

x=t \rightarrow (\neg Y_1 \rightarrow \neg Y_2) where Y₂ is obtained from atomic formula Y₁ by replacing one occurrence of x with t. Whether this can be proved or has to be taken as another axiom, I don't know. But using this formula and 7), I can show

x=t \rightarrow (Y(x) \rightarrow Y(t)) and
x=t \rightarrow (Y(t) \rightarrow Y(x))

for any atomic formula Y(x) by induction on the number of times the variable x occurs in Y(x). Using this result as a base case, I can further show that

x=t \rightarrow (F(x) \rightarrow F(t)) (*) and
x=t \rightarrow (F(t) \rightarrow F(x)) (**)

for any formula F(x) (where x occurs only as a free variable) by induction on the degree of F(x). The degree of a formula is the number of occurrences of the symbols \neg, \forall, and \rightarrow in the formula (in unabbreviated form). An atomic formula obviously has degree zero. A formula F(x) of degree n has one of the following three forms:

i) \neg G where G is of degree n-1
ii) \forall y G where G is of degree n-1
iii) G \rightarrow H where the degrees of G and H add to n-1

For cases i) and ii), the induction step is very easy. Case iii) goes like this:

x=t \rightarrow (H(x) \rightarrow H(t))
x=t \rightarrow (G(t) \rightarrow G(x)) by hypothesis since both G and H are of degree less than n.

From the first we get:
x=t \rightarrow ((G(t) \rightarrow H(x)) \rightarrow (G(t) \rightarrow H(t)))
(x=t \rightarrow (G(t) \rightarrow H(x))) \rightarrow (x=t \rightarrow (G(t) \rightarrow H(t)))

from the second:
x=t \rightarrow ((G(x) \rightarrow H(x)) \rightarrow (G(t) \rightarrow H(x)))
(G(x) \rightarrow H(x)) \rightarrow (x=t \rightarrow (G(t) \rightarrow H(x)))

and finally

(G(x) \rightarrow H(x)) \rightarrow (x=t \rightarrow (G(t) \rightarrow H(t)))
x=t \rightarrow ((G(x) \rightarrow H(x)) \rightarrow (G(t) \rightarrow H(t)))

as hoped for. Of course, x=t \rightarrow ((G(t) \rightarrow H(t)) \rightarrow (G(x) \rightarrow H(x))) is proved the same way with x and t switched throughout.

 

[techmologist]

With that out of the way, one can prove some useful theorems.

T1) \exists x F \rightarrow F provided x does not occur in F

proof:
\neg F \rightarrow \forall x \neg F axiom 5)
\neg \forall x \neg F \rightarrow F

T2) \forall x F \rightarrow \exists xF provided x does not occur in F
(and therefore \forall x F \rightarrow F under those conditions)

proof:
\neg F \rightarrow (F \rightarrow x \neq t) prop. calc.
\forall x(\neg F) \rightarrow (\forall x F \rightarrow \forall x (x \neq t)) Generalization and axiom 4)
\forall x F \rightarrow (\forall x(\neg F) \rightarrow \forall x (x \neq t))
\forall x F \rightarrow (\exists x(x = t) \rightarrow \exists x F)
\exists x(x = t) \rightarrow (\forall x F \rightarrow \exists x F)

T3) \forall x F(x) \rightarrow F(t)

proof:
from (*) above,
x=t \rightarrow (F(x) \rightarrow F(t))
F(x) \rightarrow (x=t \rightarrow F(t))
F(x) \rightarrow (\neg F(t) \rightarrow x \neq t)
\forall xF(x) \rightarrow (\forall x \neg F(t) \rightarrow \forall x(x \neq t))
\forall xF(x) \rightarrow (\exists x (x=t) \rightarrow \exists xF(t))
\exists x(x=t) \rightarrow (\forall x F(x) \rightarrow \exists xF(t))
\forall x F(x) \rightarrow \exists xF(t), and then use T1) to get T3)

T4) F(t) \rightarrow \exists x F(x)
T5) \forall x F(x) \rightarrow \exists x F(x)

T6) \forall x F(x) \rightarrow \forall y F(y)

proof:
as a special case of T3)
\forall x F(x) \rightarrow F(y)
\forall y \forall x F(x) \rightarrow \forall yF(y) generalization and axiom 4)
\forall x F(x) \rightarrow \forall y F(y) axiom 5)

Similarly, \exists x F(x) \rightarrow \exists y F(y)

This result allows the relaxation of the earlier requirement that x not occur bound in formulas in which it is also free. Now if it occurs bound also, the formula is equivalent to one in which it doesn't. I normally avoid formulas in which the same variable occurs bound and free, but their possibility has to be allowed for.

T7) F(t) \rightarrow \forall x(x=t \rightarrow F(x))

proof:
from (**)
x=t \rightarrow (F(t) \rightarrow F(x))
F(t) \rightarrow (x=t \rightarrow F(x))
\forall x F(t) \rightarrow \forall x(x=t \rightarrow F(x)) , and T7) comes from applying axiom 5)

T8) \forall x(x=t \rightarrow F(x)) \rightarrow F(t)

proof:
x=t \rightarrow (F(x) \rightarrow F(t))
(x=t \rightarrow F(x)) \rightarrow (x=t \rightarrow F(t))
(x=t \rightarrow F(x)) \rightarrow (\neg F(t) \rightarrow x \neq t)
\neg F(t) \rightarrow ((x=t \rightarrow F(x)) \rightarrow x \neq t)
\neg F(t) \rightarrow (\forall x(x=t \rightarrow F(x)) \rightarrow \forall x (x \neq t))
\forall x(x=t \rightarrow F(x)) \rightarrow (\neg F(t) \rightarrow \forall x (x \neq t))
\forall x(x=t \rightarrow F(x)) \rightarrow (\exists x(x=t) \rightarrow F(t))
\exists x(x=t) \rightarrow (\forall x(x=t \rightarrow F(x)) \rightarrow F(t))

Taken together, T7) and T8) allow you to obtain a formula equivalent to the result of substituting t for all free occurrences of x in F(x), without appealing to substitution as a rule of inference.