New answers tagged lo.logic
3
Yes, backtracking in focused proof search may be necessary due to a wrong choice of focus formula. Consider the provable sequent
$$\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot.$$
Choosing to focus on $p\otimes q$ leads to a dead end, because however you "split" the context you end up with an atom ($p$ or $q$) without matching ...
4
Yes. Just employ the formula $\forall{x}\forall{y} \; R(x,y) \leftrightarrow (x=y)$ (for a fresh binary predicate $R$), which allows you to "hide" the equality inside the $\forall\forall$-part of the Scott normal form. Then you proceed as usual.
EDIT: I've noticed that you wrote that $\alpha$ in $\forall{x}\forall{y} \; \alpha$ is a binary ...
4
I believe that the formula with the quantifier prefix you want to achieve are strictly less expressive than the two-variable logic with counting quantifiers. So there is no hope that you can translate any C2 formuale into such a form.
Similar types of Scott-normal forms were obtained in:
Bartosz Bednarczyk, Witold Charatonik: Modulo Counting on Words and ...
8
It seems to me there isn't an agreement about what "HOL" means. The OP indicates in their question that they are thinking of the formalization of higher-order logic within the formalism of the simply-typed $\lambda$-calculus. To give the question some clarity, allow me to spell out my understanding of what such a formalism comprises.
Recall the ...
7
The structure you want is due to Andy Pitts, and is called a tripos. It extends the notion of hyperdoctrine, which gives a categorical model for first-order logic, with enough structure to model higher-order logic.
However, much more of the work in this part of categorical logic focuses on toposes instead of triposes, which are just a little bit more ...
8
If recollection serves the answer is yes, although it is definitely not easy (so far as I know). The question was first posed by Shoenfield in the final paragraph of his paper Degrees of unsolvability associated with classes of formalized theories. I believe it was first answered by Peretyat'kin, who has proved a number of deep results about the model- and ...
Top 50 recent answers are included
