<p>I'm just getting into model theory for type theory. I would like to know:</p>
<ol>
<li><p>How to properly define notions Compactness in type theory?</p>
</li>
<li><p>Is There Completeness, Compactness and downward Löwenheim–Skolem theorem hold in <code>MLTT</code>/<code>pCIC</code>?</p>
</li>
</ol>

CC BY-SA 4.0
2024-06-03T18:54:22.023Z
Please ask only one question per post.  If you have multiple questions, each one can be posted separately.  Please ask only about questions you are seriously thinking about, and show what progress you've made and what resources you've found so far.  See our [help/on-topic], especially "Questions should be based on..."  Please [edit] your question to make it suitable here.
D.W.
CC BY-SA 4.0
2024-06-03T19:39:46.857Z
@D.W. Interestingly the question I posed can indeed be seen as **a question**, since the three properties Completeness, Compactness and downward LST can be deduced from each other in `FOL`, and the question itself is whether these properties of `FOL` also hold in `MLTT`/`pCIC`.
Ember Edison
<lo.logic><type-theory><model-theory>
Completeness, Compactness and LST in Type Theory
Ember Edison
# Completeness, Compactness and LST in Type Theory

(Asked by: username_0 on 2024-06-03)

I'm just getting into model theory for type theory. I would like to know:

1. How to properly define notions Compactness in type theory?
2. Is There Completeness, Compactness and downward Löwenheim–Skolem theorem hold in `MLTT`/`pCIC`?

**Tags:** lo.logic, type-theory, model-theory
> **Comments:**
> **username_1**: Please ask only one question per post.  If you have multiple questions, each one can be posted separately.  Please ask only about questions you are seriously thinking about, and show what progress you've made and what resources you've found so far.  See our [help/on-topic], especially "Questions should be based on..."  Please [edit] your question to make it suitable here.  
> **username_0**: @D.W. Interestingly the question I posed can indeed be seen as **a question**, since the three properties Completeness, Compactness and downward LST can be deduced from each other in `FOL`, and the question itself is whether these properties of `FOL` also hold in `MLTT`/`pCIC`.  

---

## 0 answers

