Questions tagged [model-theory]
The model-theory tag has no usage guidance.
27
questions
1
vote
1
answer
122
views
Are Turing Machines Models?
I am wondering whether it is correct to say that Turing machines are models of, say, the lambda calculus, in the model theoretical sense. Lambda calculus and Turing machines are equivalent ...
- 21
4
votes
0
answers
120
views
Completeness, Compactness and LST in Type Theory
I'm just getting into model theory for type theory. I would like to know:
How to properly define notions Compactness in type theory?
Is There Completeness, Compactness and downward Löwenheim–Skolem ...
- 201
0
votes
1
answer
162
views
What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?
In what books or papers is it explained how the type constructions of a functional programming language correspond to category theory, and what are the models (a rigorous semantics) of programs of ...
- 552
8
votes
1
answer
367
views
In logic programming, what would a language with second-order model theory gain?
HiLog is described as a logic programming language with higher-order syntax, but first-order model theory.
For example, it allows you to define a map over lists:
...
- 259
2
votes
0
answers
89
views
Is there a text that contains all 4 Büchi-Elgot-Trakhtenbrot-style theorems?
There are several natural Büchi-Elgot-Trakhtenbrot-style theorems:
The equivalence of various finite automata on finite words and the weak monadic second order theory of 1 successor
The equivalence ...
- 519
5
votes
0
answers
177
views
Can a positive elementary inductive definition refer to its own stage comparison relation?
Moschovakis' stage comparison theorem says that the stage comparison relation associated with any positive elementary induction is itself definable by (another) positive elementary induction. But what ...
- 851
2
votes
1
answer
106
views
Are MSO formulae on graphs expressible with bounded quantifier alternation?
Is there some $k$ such that, given any formula $\varphi$ in the monadic second order theory of graphs (this question applies for either MSO with sets of vertices and edges or just MSO with sets of ...
- 519
4
votes
2
answers
273
views
Are MSO formulae expressible as existential SO formulae over arbitrary structures?
Given an MSO formulae φ, which may contain arbitrary quantifier alternation, is there always an ESO formula ψ, such that φ and ψ have the same (finite) models?
(This statement holds when the models we ...
3
votes
1
answer
178
views
Exposition of categorical models of type theory from type-theoretic perspective
Are there any formalizations or expositions of categorical models from type theoretic point-of-view? What I have in mind to get a better grasp of categorical models of dependent types, treating ...
- 920
6
votes
1
answer
217
views
Is there a way to define dependent types without explicit substitutions internally within agda?
I am playing around the Programming Language Foundations in Agda exercises and wondering if we can achieve the same level of theories with dependent types. With simple types, the definition usually ...
- 163
1
vote
1
answer
178
views
What kind of computational model is the brain? [duplicate]
I was wondering what kind of computational model is the human brain (as it seems superior to a Turing machine).
Another thing that should be a separate question, What would be a perfect computer model ...
- 133
4
votes
0
answers
106
views
Logic of learning
Does Robust logic (Leslie Valiant), Default logic (Raymond Reiter) and Circumscription logic (John McCarthy) have any relation?
I was Mathematician and Computer Science (dual degree undergraduate) ...
8
votes
0
answers
75
views
Relationship between lambda-definability, specification and definability in model theory
I am new to lambda calculus and definability theory, and I am trying to clarify my understanding of the relationship among the following concepts:
An element $a$ in the domain of a type $A_\sigma$ is ...
- 243
3
votes
1
answer
179
views
Descriptive model theory classification of Counting hierarchy
Descriptive model theory uses logic to characterize complexity classes
How to model
Counting Hierarchy
PSPACE
in descriptive model theory?
- 13.1k
2
votes
0
answers
123
views
Applications of the monoidal closed structure in LTL?
A simple model of temporal logic is via time-indexed truth
functions. This lets us model the Boolean connectives, as well as the
next-step operator and modal always operator:
$$
\begin{array}{lclll}
...
- 32.8k
4
votes
0
answers
280
views
Modeling union types using sum types
It is trivial to model sum types using only union types and product types: simply add a discriminant. $A + B \cong (0 \times A) \cup (1 \times B)$.
What I am wondering is whether or not there is a ...
5
votes
1
answer
539
views
Proof that the theory of rationals is convex
In Example 10.12 of the book The calculus of computation by Bradley and Manna, it is said
The theory of rationals is convex, as it is convex in a geometric sense.
How does the geometric sense of ...
- 153
6
votes
1
answer
357
views
Standard reference for basic model theory definitions
I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...
- 203
2
votes
0
answers
75
views
applications of institution-independent model theory
To quote wikipedia,
The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970s in order to deal with the "population explosion among the logical systems used in ...
- 523
4
votes
1
answer
281
views
Is it decidable that a computable analytic function over $\mathbb{R,C} ,$ equals $0$
Is it decidable whether a computable analytic function $f(x_1,x_2,\dots,x_n)$ over $\mathbb{R}$, $\mathbb{C}$ in a semi-algebraic or semi-analytic domain is identically zero? Is there any algorithm?
...
- 1,071
16
votes
1
answer
1k
views
To what extent can the mathematics of Reals be applied to Computable Reals?
Is there a general theorem that would state, with proper sanitization,
that most known results regarding the use of real numbers can actually
be used when considering only computable reals? Or is ...
- 1,542
3
votes
1
answer
247
views
Decidability of first-order theory of real closed fields with functions
By a famous theorem of Tarski, the first-order theory of real closed fields is decidable, as it admits quantifier elimination. Can this result be extended so that propositions can be quantified over ...
- 11.2k
9
votes
1
answer
1k
views
What is the axiomatic (set theory) context of the P vs NP and NP=EXPTIME conjectures?
When the conjecture $\mathbf{P} = \mathbf{NP}$ or $\mathbf{P} \neq \mathbf{NP}$ is set (e.g. by the Clay Mathematical Institute by S. Cook, see here) what mathematical axiomatic system is assumed?
In ...
5
votes
0
answers
268
views
Is there a Galois correspondence between a Haskell class hierarchy and its instance hierarchy?
Can we consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)? In the example below the specification of the class ...
- 179
16
votes
2
answers
468
views
How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?
For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, ...
- 2,611
1
vote
2
answers
292
views
Any Graph is a Model (! or ?)
I know this could be considered a pointless question. However despite I am quite convinced that any possible model (i.e. UML, SysML, natural language, math, etc.) can be defined by means of a graph I ...
- 123
8
votes
1
answer
165
views
Time/Space Requirements of Verifying or Falsifying a First-Order Statement
Though L.Berman proved that the problem of verifying or falsifying any first-order statement about real numbers that uses addition and comparison but not multiplication is in EXPSPACE. Has it been ...
- 457