- #1
techmologist
- 306
- 12
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.[tex]\exists x[/tex] is here taken to be an abbreviation for [tex]\neg\forall x \neg[/tex].
Propositional calculus:
1)[tex]F \supset(G \supset F)[/tex]
2)[tex](F \supset (G \supset H)) \supset ((F \supset G) \supset (F \supset H))[/tex]
3)[tex](\neg F \supset \neg G) \supset (G \supset F)[/tex]
Predicate calculus:
4)[tex]\forall x(F \supset G) \supset (\forall x F \supset \forall x G)[/tex]
5)[tex]F \supset \forall x F[/tex] provided x does not occur in F
6)[tex]\exists x (x = t)[/tex] provided x does not occur in the term t
7)[tex]x = t \supset (Y_1 \supset Y_2)[/tex] where Y2 is obtained from atomic formula Y1 by replacing any one occurrence of x with t. An atomic formula is a formula of the form t1 = t2, where t1 and t2 are terms.
Rules of inference: Modus Ponens and Universal Generalization, i.e. from theorem F infer [tex]\forall x F[/tex]. 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 [tex]x=t \supset (x=t \supset t=t)[/tex].
This is equivalent to
[tex]x=t \supset t=t[/tex]
And from this we can infer
[tex]\exists x(x=t) \supset t=t[/tex], which gives us the theorem t = t for any term t. I can show a limited form of symmetry:
[tex]x=t \supset (x=x \supset t=x)[/tex]
[tex]x=x \supset (x=t \supset t=x)[/tex]
[tex]x=t \supset t=x[/tex]
But I haven't figured out how to show [tex]t=x \supset x=t[/tex], much less [tex]t_1 = t_2 \supset t_2 = t_1[/tex].
Axiom scheme 7) itself gives a limited form of transitivity, i.e.
[tex]x=t_1 \supset (x = t_2 \supset t_1=t_2)[/tex]
But I don't know how to show [tex]x=t_1 \supset (t_1=t_2 \supset x = t_2)[/tex], 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
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.[tex]\exists x[/tex] is here taken to be an abbreviation for [tex]\neg\forall x \neg[/tex].
Propositional calculus:
1)[tex]F \supset(G \supset F)[/tex]
2)[tex](F \supset (G \supset H)) \supset ((F \supset G) \supset (F \supset H))[/tex]
3)[tex](\neg F \supset \neg G) \supset (G \supset F)[/tex]
Predicate calculus:
4)[tex]\forall x(F \supset G) \supset (\forall x F \supset \forall x G)[/tex]
5)[tex]F \supset \forall x F[/tex] provided x does not occur in F
6)[tex]\exists x (x = t)[/tex] provided x does not occur in the term t
7)[tex]x = t \supset (Y_1 \supset Y_2)[/tex] where Y2 is obtained from atomic formula Y1 by replacing any one occurrence of x with t. An atomic formula is a formula of the form t1 = t2, where t1 and t2 are terms.
Rules of inference: Modus Ponens and Universal Generalization, i.e. from theorem F infer [tex]\forall x F[/tex]. 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 [tex]x=t \supset (x=t \supset t=t)[/tex].
This is equivalent to
[tex]x=t \supset t=t[/tex]
And from this we can infer
[tex]\exists x(x=t) \supset t=t[/tex], which gives us the theorem t = t for any term t. I can show a limited form of symmetry:
[tex]x=t \supset (x=x \supset t=x)[/tex]
[tex]x=x \supset (x=t \supset t=x)[/tex]
[tex]x=t \supset t=x[/tex]
But I haven't figured out how to show [tex]t=x \supset x=t[/tex], much less [tex]t_1 = t_2 \supset t_2 = t_1[/tex].
Axiom scheme 7) itself gives a limited form of transitivity, i.e.
[tex]x=t_1 \supset (x = t_2 \supset t_1=t_2)[/tex]
But I don't know how to show [tex]x=t_1 \supset (t_1=t_2 \supset x = t_2)[/tex], 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
Last edited: