Extension of Natural Deduction (). Formulas
Where is a propositional variable.
NM_2 = NM+\frac{{M:A[Y\mapsto X]}}{\forall X.A}+\frac{\forall X.A}{A[X\mapsto B]} $$Where $B$ may be arbitrarily complex, including where it's more complex than $A$. Note that this second $\forall E$ rule in [[impredicative]]. Note that $Y$ must be fresh.\begin{aligned} \bot &:= \forall X. X\ \neg A&:= A\to \bot \ A\vee B&:= \forall X.(A\to X)\to (B\to X)\to X\ A\wedge B&:=\forall X.(A\to B\to X)\to X\ \exists X.A&:=\forall Y. (\forall X.(A\to Y))\to Y\ \end{aligned}
\begin{aligned} (\exists E)\quad &\forall Y. (\forall X.(A\to Y))\to Y\ &A[X\mapsto Z] \to W\ &-------\ (\forall E)\quad &(\forall X.(A\to W))\to W\ (\forall E)\quad &((A[X\mapsto Z]\to W))\to W\ (\to E)\quad & W\ \end{aligned}
### Numerals\begin{aligned} \lceil n \rceil f y =f^n y \quad \forall n\in \mathbb{N} \ N := \forall A.(A\to A)\to (A \to A) \end{aligned}
Simple type structures Given $\eta:\mathcal{V}\to \mathrm{Set}$\begin{aligned} X^\eta = \eta (X)\ (A\to B)^\eta := {f:A^\eta\to B^\eta} \end{aligned}
*This does not extend to a model of [[system F]] as it doesn't have recursion.* ### [[Jean-Yves Girard]]'s Term Model Candidate is a set $\alpha$ of terms such that SN = [[Strongly Normalizing]]\begin{aligned} \alpha \subset S N\ \alpha\text{ closed under }\to_\beta \ M\text{ not an abstraction }\implies \forall M’\leftarrow_\beta M. M’\in\alpha \implies M\in \alpha \end{aligned}
\begin{aligned} C_\alpha &=\alpha \ C_{A\to B} &= {M:\forall N\in C_A.MN\in C_B}\ C_{\forall x.A(x)}&=\bigcap_\alpha C_{A(\alpha)} \end{aligned}
\frac{\exists’ X.A(X)\qquad [A(X)]…B}{B}
\frac{A[X\mapsto B]}{\exists’ X.A}
#### Thm: This $\exists'$ is equivalent to $\exists$NM_2+\exists’ \vdash \exists X.A(X) \iff\exists’ X.A(X)
The $\exists$ gives us enough to define and reason about coalgebras such as streams and co-naturals. ### Coinduction\mu X A(X)=\forall X. (A(X)\to X) \to X
\nu XA(X)=\exists X.(X\to A(X))\to X
### Knaster-Tarski Thm (sp?) See: https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem Let $L$ be a [[complete lattice]]. Let f : L -> L be [[monotone]]. Then the set of fixed points of f in L forms a [[complete lattice]]. ### Church style\frac{s:B}{\lambda x:A.~s:A\to B}
\frac{s:A(Y)}{\Lambda X.s:\forall X.A(X)}
\frac{s:\forall X.A(X)}{s B.A(B)}
### The set of strongly normalizing terms is recursively enumerable Proof: [[Kőnig's lemma]] ### Intersection Types:A;~s:B\vdash s:A\cap B
s:A\cap B\vdash A
# Duplicate Content 1 ## Idea Second-order logic constitutes an extension of classical [[First-Order Logic (Classical)|first-order logic]] allowing quantification over sets of domain elements (predicates) or functions, rather than solely over individual elements. While strictly more expressive than first-order logic, it lacks properties such as [[completeness]] and [[compactness]] under standard semantics. ## Definition *Second-order logic* is a [[formal system]] extending first-order logic by introducing variables that range over relations (or subsets) and [[functions]] on the [[domain of discourse]], along with quantifiers binding these variables. Formally, the language includes: - Individual variables: $x, y, z, \dots$ - Relation variables (of various arities): $X, Y, Z, \dots$ or $P, Q, \dots$ - Function variables: $f, g, \dots$ - Second-order quantifiers: $\forall X, \exists X, \forall f, \exists f$. ## Syntax A formula involving second-order quantification is well-formed if it adheres to standard recursive rules. For example, the principle of [[mathematical induction]] is expressible as a single axiom in SOL: $$\forall P \, [ (P(0) \land \forall x (P(x) \to P(S(x)))) \to \forall n \, P(n) ]$$ Here, $P$ is a variable ranging over all properties (unary relations) of the domain. ## Semantics We distinguish between two primary semantics for SOL, yielding different metatheoretic properties. ### Standard Semantics The domain of relation variables $X$ of arity $k$ is the full power set $\mathcal{P}(D^k)$, where $D$ is the domain of individuals. Under standard semantics: 1. We gain high expressive power (e.g., $\mathbb{N}$ and $\mathbb{R}$ are characterizing up to isomorphism). 2. We lose the [[Completeness]] Theorem (Gödel). 3. We lose the [[Compactness]] Theorem and the [[Löwenheim-Skolem]] property. ### [[Henkin Semantics]] Models include a specific domain of relations $\mathcal{D}_k \subseteq \mathcal{P}(D^k)$ for each arity, subject to [[Axiom of Comprehension|comprehension axioms]] ensuring definable relations exist. - Under this interpretation, SOL is essentially a many-sorted first-order logic. - We recover Completeness, Compactness, and Löwenheim-Skolem properties. - We lose the ability to categorically characterize structures like the [[Natural Number|natural numbers]]. ## Expressivity SOL can define concepts inexpressible in [[First-Order Logic]]: 1. **Finiteness:** A domain is finite if and only if every surjective function from the domain to itself is injective ([[Dedekind finiteness]]). 2. **Countability:** We can assert the existence of an ordering isomorphic to $\omega$. 3. **Graph Properties:** Connectivity and 3-colorability are definable. ## Relation to Type Theory In the context of [[type theory]], SOL corresponds to polymorphic lambda calculi (like [[System F]]) via the [[Curry-Howard correspondence]], where second-order quantification $\forall X$ corresponds to polymorphism over types. ## References [[shapiro1991-second-order-foundations]]