|
Zapiski Nauchnykh Seminarov LOMI, 1974, Volume 40, Pages 101–109
(Mi znsl2685)
|
|
|
|
Heytiag predicate calculus with $\varepsilon$-symbol
G. E. Mints
Abstract:
It is known that the introduction of $\varepsilon$-symbol with $\varepsilon$-axioms $A[t]\to A[\varepsilon x A]$ leads to non-conservative extension. For example $\exists x(\rceil P_x\to\rceil Pb\&\rceil Pa)$ becomes derivable. A conservative extension is obtained by treating $\varepsilon$-symbol like $\iota$-symbol: for every occurence $\varepsilon x A[x,\alpha_1\dots,\alpha_n]$ in a sequent from a deduction formula
$\forall\alpha_1\dots\forall\alpha_n\exists x A$ should occur in the antecedent of this sequent. Cut-elimination is proved for the resulting system $HPC^{\varepsilon}$. It is pointed out that the proof could be extended to $HPC$ with decidable equality and to Heyting arithmetic with free function variables and the principle of choice:
$$
\Gamma\to\forall x\exists y A;\quad\forall x A_y[f(x)],\quad\Gamma\to C\vdash\Gamma\to C.
$$
The extension to Heyting arithmetic with bound variables of higher types and corresponding choice principle requires new ideas.
Citation:
G. E. Mints, “Heytiag predicate calculus with $\varepsilon$-symbol”, Studies in constructive mathematics and mathematical logic. Part VI, Zap. Nauchn. Sem. LOMI, 40, "Nauka", Leningrad. Otdel., Leningrad, 1974, 101–109
Linking options:
https://www.mathnet.ru/eng/znsl2685 https://www.mathnet.ru/eng/znsl/v40/p101
|
Statistics & downloads: |
Abstract page: | 220 | Full-text PDF : | 70 |
|