<p>I couldn't find any source speaking about the consistency of [Weak] Monadic Second Order Logic over Binary Trees (or over graphs with finite tree/clique width). I did find decidability results, and it all looks to me like a finite amount of "interleaved Presburger arithmetics" with monadic second order quantification, roughly speaking. But I cannot find proofs or discussions about the topic. Can someone please enlighten me with a reference or an argument?</p>

CC BY-SA 3.0
2016-06-30T14:23:07.793Z
If it would be inconsistent, the algorithm for membership in the theory would always answer "true", which is not the case.
Denis
CC BY-SA 3.0
2016-07-01T00:21:43.057Z
can you elaborate please?
Troy McClure
CC BY-SA 3.0
2016-07-01T11:22:37.533Z
Any inconsistent theory is decidable because all sentences are derivable from the axioms, hence any statement is "true" in the theory. So the algorithm that always answers "true" decides membership in the theory. For MSO on infinite trees, the algorithm is nontrivial and can answer "false", hence the theory is consistent.
Denis
<lo.logic>
Consistency of MSOL over trees
Troy McClure
# Consistency of MSOL over trees

(Asked by: username_0 on 2016-06-30)

I couldn't find any source speaking about the consistency of [Weak] Monadic Second Order Logic over Binary Trees (or over graphs with finite tree/clique width). I did find decidability results, and it all looks to me like a finite amount of "interleaved Presburger arithmetics" with monadic second order quantification, roughly speaking. But I cannot find proofs or discussions about the topic. Can someone please enlighten me with a reference or an argument?

**Tags:** lo.logic
> **Comments:**
> **username_1**: If it would be inconsistent, the algorithm for membership in the theory would always answer "true", which is not the case.  
> **username_0**: can you elaborate please?  
> **username_1**: Any inconsistent theory is decidable because all sentences are derivable from the axioms, hence any statement is "true" in the theory. So the algorithm that always answers "true" decides membership in the theory. For MSO on infinite trees, the algorithm is nontrivial and can answer "false", hence the theory is consistent.  

---

## 0 answers

