# Tagged Questions

39 views

### Proof on Dyadic Trees [Smullyan: First-Order Logic, chapter 1, section 0]

I'm having difficult with a proof from Smullyan's First-Order Logic, Chapter 1 Section 0 (Reprint, Dover 1968, p. 4): Prove: In a dyadic tree, define x to be to the left of y if there is a ...
27 views

### Can a non-cyclic infinite proof tree with always-reachable provable nodes be used to construct a proof?

Suppose that I have a finite number of basic elements x,y,z ... and a finite number of operators +, * ... Terms X,Y,Z ... are created by combining basic elements and operators. For example, x+y, and ...
75 views

### Are the structure of logical expression based on formative constructions like sequences or trees ?

Recently, I get confused when reading the book Principles of Mathematical Logic written by D. Hilbert. How to define the term 'logical expression'? I just envisage that it might be defined as anyone ...
293 views

### Is there a “tree-like” proof of compactness theorem in the case of uncountably many variables?

I like proofs using trees and König's lemma, since they are very visual. One of the applications of König's lemma you can show to students is proving compactness theorem for propositional calculus, ...
214 views

### Ordinal interpretation of Friedman's $n$?

I heard that Kruskal's tree theorem can be turned into a finite form that creates an extremely fast growing function because ordinals could be encoded into trees. On this wiki page it mentions that ...
82 views

### Natural order of rational trees?

What would be a natural order of rational trees? Rational trees arise naturally from free algebras if we view a term as a finite tree. For example the term f(a,g(b,c)) could be viewed as the ...
459 views

### How to make a parse tree for the following propositional logic formula?

I have a formula $\neg (( q \rightarrow \neg q) \vee p \vee ( \neg q \rightarrow ( r \wedge p)))$. As it contains 3 subformulas between the $\vee$'s, how can I put it into a parse tree. Would it be ...
Lets work with the following inductive definition of a decision tree: 1) $\bot$, $\top$ are decision trees. 2) If $x_i$ is a variable and $T_0$, $T_1$ are decision trees then \$(\lnot x_i \land T_0) ...