Proving $\exists ! x (t = x)$ constructively without double negation axiom

Question

I am wondering how one would go about this. I am using Hilbert style proof system as described in Kleene's "Introduction to Metamathematics" or "Mathematical logic". I am pretty sure that if you can give the proof in your preferred system then I will be able to translate it (hopefully). I am using predicate calculus with equality. Also, I hope that it is clear from the context which symbol is variable, term, formula, held free, held fixed, and so forth. If not, please let me know. $\exists !x (A(x))$ stands for $\exists x (A(x) \land \forall y (A(y) \implies y=x))$.

1. $ \lnot \exists x (t=x \land \forall y (t=y \implies y=x)) \vdash \forall x(\lnot(t=x \land \forall y (t=y \implies y=x))) \vdash \lnot(t=t \land \forall y (t=y \implies y=t))$.

By negation of existential quantifier and by $\forall$- elimination where $t$ is free for $x$.

2. $\vdash t=t$.

Axiom for equality.

3. $\vdash t = y \implies y = t$, so $\vdash \forall y(t=y \implies y=t)$.

By property of equality and $\forall$-introduction where $y$ is free for $y$.

Combining three results we obtain a contradiction, so, by skipping some steps,

4. $\vdash \lnot \lnot \exists x (t=x \land \forall y (t=y \implies y=x)) \vdash \exists x (t=x \land \forall y (t=y \implies y=x))$

By $\lnot$-introduction and $\lnot$-elimination.

Answer 1

I see that you are trying a proof by contradiction, which was my first inclination as well, but there is probably no need for it. Or at least, here is a direct proof done in my preferred system, Fitch:

Please note that the software implementation of this system treats $t$ as a variable, so I had to use $c$ instead of $t$

Answer 2

Here's a complete, formal proof written in Agda, a constructive dependent type theory.

data _≡_ {A : Set} (a : A) : A → Set where
    Refl : a ≡ a

record Σ (A : Set) (F : A → Set) : Set where
    constructor _,_
    field
        fst : A
        snd : F fst

_∧_ : Set → Set → Set
A ∧ B = Σ A (λ _ → B)

thm : {A : Set} → (t : A) → Σ A (λ x → (t ≡ x) ∧ ((y : A) → t ≡ y → x ≡ y))
thm t = t , (Refl , λ y prf → prf)

All that happens is the existential is instantiated with the term $t$, and the rest follows just as readily. In fact, it follows so readily that you can just ask Agda to automatically fill in the proof, e.g. from thm t = ?, Agda can fill in the ? completely automatically.

There's a few reasons why you may be having difficulty.

1. You are using a Hilbert-style system. These are extremely non-ergonomic.
2. You are using a system for classical logic but just avoiding the use of LEM. Many Hilbert-style systems are designed to be minimal. This makes the axioms highly interdependent. Indeed, in these systems many definitions and basic reasoning steps require the use of LEM even though the result is constructive. Hilbert-style systems for constructive logic are much more verbose than typical Hilbert-style systems for classical logic.