Skip to main content
11 votes
Accepted

Standard reference for basic model theory definitions

Here is one possibility, but other people might use different words. I will use first-order logic as a running example. Language The language is a collection of expressions, which are syntactic ...
Andrej Bauer's user avatar
  • 29.2k
7 votes

Are MSO formulae expressible as existential SO formulae over arbitrary structures?

In MSO one can say that a graph is not $3$-colorable: $$\forall C_1 \forall C_2 \forall C_3 (``\text{$C_1,C_2,C_3$ are disjoint sets that cover the graph''} \to \exists x \exists y (E(x,y) \land \...
Reijo Jaakkola's user avatar
5 votes

What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

Your description of an idealized computer is a nescient form of realizability, and there are very simple realizability models of parametric polymorphism. Take a model of computatation (an "...
Andrej Bauer's user avatar
  • 29.2k
5 votes

Descriptive model theory classification of Counting hierarchy

This is only a partial answer (to the $PSPACE$ characterization), but I don't have the reputation to comment. $PSPACE$ has the following (equivalent) descriptive characterizations: $FO[2^{n^{O(1)}}]...
Sam McGuire's user avatar
4 votes
Accepted

Proof that the theory of rationals is convex

The key idea here is that for any conjunction of equations $F\equiv u_1=v_1\wedge\ldots\wedge u_k=v_k$, the set $S_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S_F$, all points ...
Klaus Draeger's user avatar
4 votes
Accepted

Is there a way to define dependent types without explicit substitutions internally within agda?

The thing is, the definition is "too" dependent. In order to define the type of substitution or renaming, you need to something like ...
Trebor's user avatar
  • 345
4 votes

Are MSO formulae expressible as existential SO formulae over arbitrary structures?

An SO formula quantifying over $k$-ary relations can be expressed as an MSO formula over a larger structure that includes the $k$th cartesian power of the original structure. Thus, up to a polynomial-...
Emil Jeřábek's user avatar
3 votes

In logic programming, what would a language with second-order model theory gain?

An actual second-order logic programming language would allow you to use second-order quantifiers in a computationally meaningful way. Second-order logic without quantifiers ranging over second-order ...
Andrej Bauer's user avatar
  • 29.2k
3 votes

Are MSO formulae on graphs expressible with bounded quantifier alternation?

No, for the same reason as in the linked question: an SO sentence over a given class of structures can be translated to an MSO sentence over structures augmented with their Cartesian powers, which can ...
Emil Jeřábek's user avatar
3 votes
Accepted

Exposition of categorical models of type theory from type-theoretic perspective

For simple type theories, there's a very simple dictionary. Type Theory Category Theory Judgement Category Type Object Context (Monoidal) Product Term Morphism However, interpreting dependent ...
Neel Krishnaswami's user avatar
2 votes
Accepted

What kind of computational model is the brain?

This is pretty much an open problem and subject to active research. There are a few proposals available. Here are some of the latest ones: Brain computation by assemblies of neurons Christos H. ...
Mahdi Cheraghchi's user avatar
1 vote

How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

The question is about dependent type theory, but, if the type you are trying to show non-inhabited can be expressed as a first-order formula, you can also use classical logic. You either prove ...
Danko Ilik's user avatar

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