2
$\begingroup$

There is those one Q5 to Q7 in https://en.wikipedia.org/wiki/Hilbert_system#Formal_deductions

But I know the axioms of Boolean algebra were simplified to this https://en.wikipedia.org/wiki/Wolfram_axiom

I was wondering if similar researchs have been done on quantifiers?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

There is The Epsilon Calculus developed by David Hilbert during the 20s.

It is based on the $ε$ symbol :

if $A$ is a formula and $x$ is a variable, $εx \ A$ is a term

with the axiom (Hilbert's “transfinite axiom”) :

$A(x) → A(εx A)$.

The intended interpretation is that $εx \ A$ denotes some $x$ satisfying $A$, if there is one.

Quantifiers can be defined as follows:

$∃x A(x) ≡ A(εx A)$

$∀x A(x) ≡ A(εx (¬A)).$

See the use of epsilon notation in Nicolas Bourbaki, Elements of Mathematics : Theory of sets (1968 - French ed. 1958), page 20 and page 36 [with $\tau_x$ in place of $εx$].

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks for answering. Yeah I've read about that, but there is this weird thing about "replacing the occurences of x by squares" and "linking to" the tau. And the fact that the axiom of choice is kind of embedded into the system... which makes it not very elegant according to me. $\endgroup$
    – Alexandre Khoury
    Commented Dec 26, 2015 at 22:45
  • 1
    $\begingroup$ @Mageek - I agree; and this is way Hilbert's proposal is not usually adopted. In addition, in the classical context, due to the interdefinibility of the quantifiers, a single axiom, like : $A(t) \to \exists x A(x)$, plus a rule of inference, like : "from $A \to B$, derive $\exists x A \to B$, provided that $x$ is not free in $B$" are enough for the quantificational part. Thus, there is very little "space" for further improvements... $\endgroup$
    – Mauro ALLEGRANZA
    Commented Dec 27, 2015 at 8:01

Not the answer you're looking for? Browse other questions tagged .