# Questions tagged [second-order-logic]

The tag has no usage guidance.

173 questions
Filter by
Sorted by
Tagged with
88 views

31 views

### In RCA0, Prove that for all n, fⁿ(i) exists

I wanted to prove in RCA0 that: If f:A→A be a function and i∈A, then for all n, fⁿ(i) exists. To reach that, I proved another theorem. I wrote my proof but I'm not sure it's rigorous. If you read it, ...
51 views

### Does Z₂ Prove the iteration theorem?

iteration theorem: Let (ℕ,0,S) be the structure of natural numbers. And let W be an arbitrary set and c be an arbitrary member of W and g be a function from W into W. Then, there is a unique function ...
1 vote
40 views

### What is the importance of Peano categoricity?

We know that Dedekind in 1888 proved that second order peano arithmetic(PA2) is categorical. My question is, why is it important? Does it have any mathematical, philosophical or foundamental ...
1 vote
29 views

### Peano categoricity is equivalent to weak konig lemma

Peano categoricity (PC) says that: Every model for second order peano system is isomorphic to standard model. i.e PC says that every peano system such as (A, f, i) is isomorphic to (N, S, 0). Simpson ...
53 views

### Is there such a thing as the second-order theory of a structure?

Given a structure, say for example, $(\mathbb{R};+,*,0,1,<)$, I know the definition of the first-order theory of that structure. But is there such a thing as the second-order theory of a structure, ...
• 16.8k
1 vote
57 views

### Are there expressive compact fragments of universal second order logic?

Question 1: I'm interested in fragments of universal second-order logic (USO) that are known to be compact. Are there any that, for example, include negation or first-order existential quantification? ...
• 9,228
42 views

• 239
1 vote
72 views

### Proofs that monadic second order logic is not compact

I was reading this comment by Simone on this answer to this question. The comment is reproduced below, emphasis mine. Well, It's not an extension that uses the notation you use, but all axioms remain ...
• 9,228
259 views

### Why is ZFC incapable of interpreting second-order logic?

Why is ZFC incapable of interpreting second-order logic? Also, when we say this, are we talking about ZFC as a background theory or using ZFC in some different way? I am interested in this answer ...
• 9,228
50 views

Are smt-solvers (like z3) theoretically able to (always correctly) check consistency of any 1.-order logic formula? How does smt-solver algorithm work in details? Are there any algorithms that could ...
• 109
25 views

### Strength and conservativity of $\Sigma^1_n \textrm{-DC}_0$

How strong is $\Sigma^1_n \textrm{-DC}_0$ in terms of consistency strength? I know it is conservative to $\Pi^1_n \textrm{-TI}_0$, but I don't know its relation to other subsystems. Are there any ...
• 263
40 views

### Logic with predicate symbol of arbitrary arity

For the work I am doing on abduction inference, I need a second order many-sorted logic where the only predicate symbol $\psi$ of the first order formulas may have an arbitrary arity. I may assume ...
• 193
78 views

### Prove the Archimedean property from second-order Dedekind completeness OR prove the existence of the integers.

Context: I am taking an introductory real analysis class (because I need the credit), and the professor has provided me with their notes on the subject. In the notes, the professor defines the real ...
• 4,440
39 views

### Second-order arithmetic subsystems

I've been surfing the internet, and have found some subsystems or additional axioms of second-order arithmetic whose definitions I could not find. Does anyone know what the following axioms/subsystems ...
• 263
86 views

### Proving $\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax))) \vdash \forall x (Dx \to Ax)$

I'm trying to prove the following: $$\forall x (\exists Y ((Dx \to Yx) \land (Yx \to Ax))) \vdash \forall x (Dx \to Ax)$$ The following is my first attempt. However, I'm not sure if I can just drop ...
69 views

### Is there a "canonical" form of second order logic?

For the sake of comparison, the entirety of first-order logic can be summarized as follows: The well formed formulas of first order logic are those generate by the grammar: \begin{align} &\...
• 4,440
104 views

### How big a "scaffold" does second-order logic need to detect its own equivalence notion?

(Now asked at MO.) Let $\Sigma$ be the language consisting of a single binary relation symbol. Second-order logic can "detect" second-order-elementary-equivalence of $\Sigma$-structures in ...
• 228k
118 views

### Validity of theorems using natural numbers and irrational reals together

I read in other posts (like in this answer) that the natural numbers are not definable in the first-order theory of the real numbers- That is considering just the reals within the context of a real ...
• 679
47 views

### Satisfiability of Second-Order Logic: Is this Decision Problem Complete for Some Level of the Arithmetical Hierarchy?

Consider the following decision problem defined in terms of input/output: Input: a second order logic  theory $\mathcal{T}$ (i.e., $\mathcal{T}$ is a set of second order logic formulas) Output: ...
1 vote
117 views

### Is there a model of $\operatorname{Th}(\mathbb{R})$ which is not a complete ordered field?

As far as I understand completeness (every non-empty subset bounded from above has a supremum) is a second order property. Is there a model of $\operatorname{Th}(\mathbb{R})$, the first order theory ...
• 85
66 views

### Can second order ZFC have a set model

Second order ZFC cannot have a countable model. Can it have a set model (in full semantics) of size $\kappa$ for some cardinal ? What can be said about such a $\kappa$ ?
• 3,901
1 vote
93 views

### Definition of ZFC2 (second order logic)

ZFC with 1st order logic is known. My question may be formulated either way What is the definition of ZFC2 (ZFC+second order logic)? (I assume that formulas also have quantifications of two kind over ...
• 760
161 views

### Does the absolute fragment of second-order logic satisfy a strong Lowenheim-Skolem property?

Let $\mathsf{SOL_{abs}}$ be the "forcing-absolute" fragment of second-order logic - that is, the set of second-order formulas $\varphi$ such that for every (set) forcing $\mathbb{P}$ and ...
• 228k
33 views

### Which to use for this relational calculus query, the "for all" quantifier" or the "there exists" quantifier?

Let's say the following relations are given: Sailors(sid, sname, rating, age) Boats(bid, bname, color) Reserves(sid, bid, day) What will be the tuple relation calculus query to Find the sailor name, ...
• 328
183 views

### When to use the "there exists" quantifier in tuple relational calculus?

Let's say we're given the following relation: Sailors(sid, sname, rating) And we have to answer the following query: The names of all sailors with a rating above 7. What will be the tuple relational ...
• 328
It’s my understanding that Julius Büchi showed that $WS1S$, the weak monadic second-order theory of one successor is decidable by a finite-state automaton, and that this implies that Presburger ...