21

($=$ is a logical symbol, hence I will not write it as part of the signature.) The satisfiability problem is decidable, as $\gcd$ has both a universal and an existential definition in terms of $|$, $+$, and $\le$: $$\begin{align*} \gcd(a,b)=c&\iff c\ge0\land c\mid a\land c\mid b\land\forall d\:(d\mid a\land d\mid b\to d\mid c)\\ &\iff c\ge0\land c\...


9

A something that might be too long for a comment, based on the previous answer by Emil. In the case you are interested in the complexity of such a logic, consider reading LICS'2015 paper by Joël Ouaknine, Antonia Lechner and Ben Worrell. A preprint is available here: https://www.cs.ox.ac.uk/people/james.worrell/LICS-main.pdf According to the authors, the ...


9

Maybe the keyword you are looking for is "Implicit Complexity". It is more general than Curry-Howard correspondence, but several lines of research investigate along the axis you are interested in. You can check for instance the publications of Patrick Baillot for many references and pointers. For a little self-promotion, here are for instance two ...


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


8

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


5

Ryan O'Donnell (professor at Carnegie Mellon) has a wonderful undergraduate complexity theory series that goes through the fundamentals quite well, and he's an engaging lecturer. He also has a similar graduate lecture series that mostly picks up where the undergrad series left off. (Note that this series does not cover logic, and I'm not aware of any videos ...


5

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that every propositions is equal (equivalent) to itself, but it could not be used to show that ever number equals itself.


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


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


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


3

I stumbled upon this question now, many years later. In the interim the following paper has appeared: https://dl.acm.org/doi/10.1145/3278158 https://arxiv.org/abs/1704.08705 There the authors do precisely what Kaveh asks for in his question 2: they give a (uniform) TC0 algorithm for balancing, hence obtaining an alternative proof of the main result in Buss '...


3

Q1: Yes, every LTS is bisimilar to its unfolding, which is a tree. Q2: No, by a cardinality argument. For instance take infinite binary trees with $L=\{a,b\}$. Each tree has countable set of states and is finitely-branching, but you have uncountably many such trees, even up to bisimilarity. However you have only countably many $\mu$-calculus formulas, so ...


3

For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\mu$-calculus, only the fragment called Hennessy-Milner Logic to distinguish non-bisimilar structures [HM85]. This is known as the Hennessy-Milner Theorem. ...


3

I tried to address the questions you raise in "Five stages of accepting constructive mathematics". And here are some textbooks: Constructive analysis by D. Bridges and E. Bishop is the "bible" of constructive mathematics. Varieties of constructive mathematics by D. Bridges and F. Richman considers several varieties of constructive ...


2

$(x< y) \land (y < z) \land (z < x)$


2

I can't give you a (easily translatable) answer to the question regarding Haskell and the types, but the following might help you since you already mentioned ZFC: Take the axioms of ZFC and let's assume that ZFC is consistent. By the Löwenheim-Skolem Theorem Downwards (as a corollary to the Completeness Theorem for First-Order Predicate Logic) there is a ...


2

This can take exponentially many steps, as Laakeri explained. You can build a system that cycles with period $p$. In particular, the update rule is $x_i = x_{i-1 \bmod p}$ for all $i$, with variables $x_0,\dots,x_{p-1}$. Let $p_1,\dots,p_k$ be the first $k$ primes. Concatenate $k$ disjoint systems, each of which cycles with period $p_i$. Then the period ...


2

Prof. Tim Roughgarden (Stanford University) Lectures on algorithms and more are also great. He is one of the best lecturers out there... https://www.youtube.com/channel/UCcH4Ga14Y4ELFKrEYM1vXCg/playlists


1

After re-reading Barrington et al., it seems that the case of $CC^0$ can be handled by using "group quantifiers", which allow for quantifiers to act over finite groups (i.e. $\mathbb{Z}/m\mathbb{Z}$) directly, while still using a binary representation under the hood so that the original definition of $DLOGTIME$-uniformity can still be used. With ...


1

Not good with proofs but can answer number 2. First of all it isn't necessary to use a complicated compilation scheme, you can just use PHOAS or a tagless final style directly. class Category k => Terminal k where bang :: k a () class Terminal k => Kappa k where kappa :: (k () a -> k b c) -> k (a, b) c lift :: k () a -> k b (a, ...


Only top voted, non community-wiki answers of a minimum length are eligible