# Tagged Questions

In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics. (Def: http://en.m.wikipedia.org/wiki/Higher-order_logic)

32 views

### What's a good introduction to Second Order Logic

I'm looking for a good introduction to second order logic. Any recommendations?
82 views

### The monadic second order theory with $<$ and Presburger arithmetic

Consider the monadic second order logic over the natural numbers with $<$ as a predicate, i.e. the second order logic over $(\mathbb N, 1, <)$, where we can quantify over sets and individual ...
47 views

82 views

### What is the difference between logical and iterative set

Saphiro in his "foundations without foundationalism: a case for second-order logic" defends second-order logic by claiming that talking about subsets of domain is not problematic in case of SOL. He ...
145 views

### Logic question in Real Analysis

I thought about posting some minor insecurities and some main doubts i have on a particular topic. Let R with the usual metric be a metric space, $A \subseteq R$ , $f:A\to R$ and p is a limit ...
138 views

### Are higher order logics substantially stronger than second order

Do we get much by using logics of order higher that 2? Does each transition to next level provides much power?
121 views

### Proving property for all predicates in first order logic

Let's consider language with predicate $P$ and following derivation $${{{[P[a/x]]^1} \over {P[a/x] \rightarrow P[a/x]}}\rightarrow I^1 \over {\forall_x (P(x) \rightarrow P(x))}}\forall I$$ Doesn't ...
110 views

### Completness in higher order logic and Interpretations

It´s known that for first order theories, it holds $\mathbf{ZFC} \vdash T \vdash \varphi \leftrightarrow T \models \varphi$. Why does this not hold in the higher order case (any simple example?)? ...
In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows:  \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to Y))...