Looking for a formal proof that x=x isn't a contingency

Question

EDIT - My original question was answered, but not to my satisfaction. What I really want is a formal proof α = α isn't a contingency, using the modal logic version of Hao Wang's axiom of Identity. I said 'preferably' because I know how to prove it's a tautology by knowing it isn't a contingency.

To be crystal clear I want a proof that

⊢ ∀x[x=x] ∨ ⊢ ~∀x[x=x]

Then I can prove

Theorem 2: ∀z[z=z]

Let y be a specific constant.

1. ⊢ ~∀x[x=x] [OSC1]
2. ⊢ ∃x[~(x=x)] [1;QN]
3. ⊢ ~(y=y) [2;EI]
4. ⊢ ☐~(y=y) [3;NEC]
5. ⊢ ~◊~~(y=y) [4; Df]
6. ⊢ ~◊y=y [5; DN]
7. ⊢ ◊y=y [Th.1]
8. ⊢ ◊y=y ∧ ~◊y=y [7,6; conj]
9. (⊢ ~∀x[x=x]) → contradiction [1-8; CSC1]
10. ~ ⊢ ~∀x[x=x] [9;UG]

At this point if I know ∀x[x=x] isn't a contingency, I can use disjunctive syllogism to conclude ⊢ ∀x[x=x]

---

It's clear that the proposition denoted by x=x isn't a contingency, but I want to prove this formally. Does anyone know how I could do this?

You can use Hao Wang's axiom of Identity.

Hao Wang's Axiom of Identity

• ∀y[Φ(y) iff ∃x[x=y ∧ Φ(x)]]

Or preferably you could use

Modal Logic Version of Hao Wang's axiom of Identity

• ∀y[Φ(y) iff ∃x[◊x=y ∧ Φ(x)]]

The system I've been working in is SQML, but any system is fine.

Answer 1

How to prove that the proposition denoted by x=x isn't a contingency, using Hao Wang's Axiom of Identity.

We have to use the formula ¬(z=y) as Φ(z). Thus, Φ(y) is ¬(y=y) and Φ(x) is ¬(x=y).

The relevant instance of the axiom-schema will be:

¬(y=y) ↔ ∃x[x=y ∧ ¬(x=y)].

But the right-hand side is a contradiction, and thus ¬(y=y) is equivalent to a contradiction, that means that (y=y) is always true.

By Generalization, we have ∀x (x=x).

Also the substitution property of equality follows from the axiom schema:

(x=y ∧ Φ(x)) → Φ(y).

Having reflexivity and substitution, the remaing laws of equality, like simmetry and transitivity, can be proved.

Answer 2

Let me provide a complementary answer to @Mauro.

Classically we attribute contingency to sentences. While we can change our deductive system to allow proofs of formulas with free variables (see Alex Krukman's lecture notes on model theory), a more standard route is to show that P:= "Vx, x=x" is necessary.

Then, P is a theorem of classical logic (use soundness). Then necessarily P (use necessitation). so we only need a very weak modal logic to do this (say K)

Answer 3

A follow-up proof outline

1. ∃x(¬x = x) [Assume for reductio ad absurdum]
2. ⊥
   Ergo,
3. ¬∃x(¬x = x) [1 to 2, RAA]
4. ∀x(x = x) [3 QN]
   QED

Note: Since The Law of Identity is not contigent, it's necessary. The negation of a necessary truth is a contradiction (hence my proof by contradiction)

Answer 4

I am unable to prove it formally, but I can use the metalanguage English, and a meta-axiom to prove it. Perhaps someone else can improve on this.

Metalanguage: English

Undefined binary relations: is-currently, can-become

Meta-axiom: Meaning is constant in time, truth value can vary.

Definitions

A tautology is a statement that denotes a proposition whose truth value is constant in time and is currently true.

Thus a tautology is always currently true. That means if the statement is compound, and the truth value of the proposition it denotes is true in every row of its truth table it's a tautology.

A contradiction is a statement that denotes a proposition whose truth value is constant in time and is currently false.

Thus a contradiction is always currently false. That means if a statement is compound, and the truth value of the proposition it denotes is false in every row of its truth table, it's a contradiction.

A contingency is a statement that is neither a tautology nor a contradiction.

We have simple statements, of the form a=b. The only way a simple statement can be a contingency is if the truth value of the proposition it denotes can vary in time (edit: or place or in some other sense. Re: Aristotle's definition of a contradiction as to state that something is and is not ... in the same sense and at the same time)

Using the metalanguage of English we may say

The expression 'a=b' means the thing symbolized by a is-currently the thing symbolized by b. Let's say the things symbols symbolize are their meanings.

Suppose 'a=b' is currently true. Then the meaning of a is the meaning of b. Suppose it can become false. Then the meaning of a would be different than the meaning of b. Thus, the meaning of a or the meaning of b would have to vary in time, which is impossible.

Therefore if 'a=b' is currently true, it cannot become false.

Similarly, if 'a=b' is currently false, it cannot become true.

By the law of the excluded middle, a=b is currently true or currently false. Therefore by constructive dilemma, 'a=b' cannot become true and cannot become false. Therefore, it isn't a contingency.

Let α be an arbitrary constant, and consider the statement α=α. By the preceding discussion, it's either a tautology or a contradiction. This alone doesn't tell you

⊢ ∀x[x=x] ∨ ⊢ ~∀x[x=x]

You need to to specify that your system with equality '=', is to be complete. Thus, all tautologies besides the axioms are theorems.

Now, suppose α=α is a tautology. Then ⊢ α=α, so by UG ⊢ ∀x[x=x]. IF it's a contradiction then ⊢ ~∀x[x=x]. Since α=α is either a tautology or a contradiction, we have

⊢ ∀x[x=x] ∨ ⊢ ~∀x[x=x]

I wanted something better, but perhaps someone else can find a formal proof using modal binary logic, or temporal modal binary logic.