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$.

  1. $\vdash t=t$.

Axiom for equality.

  1. $\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,

  1. $\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.

  • 1
    $\begingroup$ Why not start from 2 and 3 then use $\land$-intro to get : $t=t \land \forall y (t=y \to y=t)$ and then conclude with $\exists$-intro ? $\endgroup$ – Mauro ALLEGRANZA Jan 29 '19 at 7:41
  • $\begingroup$ @MauroALLEGRANZA I was thinking about this as well. But then I would get $\exists !x(x=x)$, wouldn't I? $\endgroup$ – Daniels Krimans Jan 29 '19 at 16:47
  • 2
    $\begingroup$ @DanielsKrimans It is valid to convert only some of the t’s to quantified variables in an $\exists$ introduction. Not sure how this would be implemented in your system though. $\endgroup$ – spaceisdarkgreen Jan 29 '19 at 17:32
  • 2
    $\begingroup$ @DanielsKrimans Usually the rule is just from $\phi(t)$ infer $\exists x\phi(x)$ for any formula $\phi(x)$ which may have t’s floating around there already that aren’t the ones that are going to be substituted for $x.$ $\endgroup$ – spaceisdarkgreen Jan 29 '19 at 17:37
  • $\begingroup$ @spaceisdarkgreen thanks, I think I had some huge misconception about existence introduction rule $\endgroup$ – Daniels Krimans Jan 29 '19 at 18:19

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:

enter image description here

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

  • $\begingroup$ It looks very good, thanks $\endgroup$ – Daniels Krimans Jan 29 '19 at 18:18
  • 1
    $\begingroup$ @DanielsKrimans You're welcome .. I hope it's not too difficult to transform this into a Hilbert style proof ... I have never really worked with those ... they look like a real pain in the a**. Anyway, as you can see, no proof by contradiction needed! $\endgroup$ – Bram28 Jan 29 '19 at 18:25

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 _,_
        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.
  • $\begingroup$ Thank you - looks interesting even though I am not that comfortable with type theory yet. Is there any way to translate your proof into Hilbert-style system proof? $\endgroup$ – Daniels Krimans Jan 29 '19 at 16:49
  • 1
    $\begingroup$ Technically, it can be done in a mechanical way. It would essentially be a much more elaborate version of bracket abstraction. In this case it would be simpler to just create a Hilbert-style proof from scratch. I recommend switching to a natural deduction system. Even if you do have a strong reason to use a Hilbert-style system, I would still recommend getting familiar with writing natural deduction proofs instead and translating them into Hilbert-style. $\endgroup$ – Derek Elkins left SE Jan 29 '19 at 21:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.