Questions tagged [second-order-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
0 answers
23 views

Hypotheses of the quadratic convergence of a real serie $x_k$

My book claims that a serie has a quadractic convergence if $\forall x_k$, $k = 1, 2, \dots$: \begin{equation} |x-x_{k+1}| \le C|x-x_k|^p \end{equation} such as $C \in \mathbb{R}$ and $p = \color{...
user avatar
1 vote
0 answers
36 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 ...
user avatar
  • 6,426
5 votes
1 answer
169 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 ...
user avatar
  • 6,426
0 votes
0 answers
26 views

Questions about smt-solvers.

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 ...
user avatar
1 vote
0 answers
17 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 ...
user avatar
  • 243
0 votes
0 answers
32 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 ...
user avatar
  • 193
0 votes
0 answers
38 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 ...
user avatar
  • 3,707
0 votes
0 answers
26 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 ...
user avatar
  • 243
-1 votes
1 answer
78 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 ...
user avatar
  • 1
0 votes
0 answers
60 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} &\...
user avatar
  • 3,707
6 votes
0 answers
100 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 ...
user avatar
0 votes
0 answers
30 views

Algorithm to decide if a first order formula is an instance of a second order formula

Is there an algorithm to detect if a first-order formula is an instance of a second order formula ? My goal is to detect if a specific first-order formula is an instance of an axiom schema. Context : ...
user avatar
  • 46
0 votes
1 answer
111 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 ...
user avatar
  • 639
0 votes
1 answer
39 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 [1] theory $\mathcal{T}$ (i.e., $\mathcal{T}$ is a set of second order logic formulas) Output: ...
user avatar
2 votes
3 answers
104 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 ...
user avatar
  • 67
0 votes
1 answer
61 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$ ?
user avatar
  • 3,578
0 votes
0 answers
56 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 ...
user avatar
  • 704
8 votes
1 answer
138 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 ...
user avatar
0 votes
1 answer
30 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, ...
user avatar
  • 327
0 votes
1 answer
34 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 ...
user avatar
  • 327
0 votes
0 answers
20 views

Sequent in a second-order arithmetic.

In one book I found a statement that "in a second-order arithmetic PA$_2$" one can prove such sequent (with a hint that it is needed to use the left introduction rule for second-order ...
user avatar
  • 180
-2 votes
1 answer
111 views

Is there a class of finite graphs that can be axiomatized by existential second-order formulas but it's complement couldn't? (edited) [closed]

I'm interested in the question above. I've just the add the "finite" requirement.
user avatar
0 votes
0 answers
36 views

What is the interpretation of Presburger Arithmetic in WS1S?

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 ...
user avatar
2 votes
2 answers
201 views

Incompleteness theorem: Peano arithmetic vs. standard model of arithmetic

Context (from https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic#From_the_incompleteness_theorems): The incompleteness theorems show that a particular sentence G, the Gödel sentence of ...
user avatar
  • 604
0 votes
0 answers
80 views

How does second-order arithmetic rule out non-standard numbers?

According to 1 there are axioms of second-order arithmetic which categorically characterize the natural numbers up to isomorphism. The axioms are: $$\forall x\,\neg(x+1=0)$$ $$\forall x\,\forall y(x+1=...
user avatar
  • 305
2 votes
1 answer
91 views

Can second-order logic with Henkin semantics be completely described by a structurally-inductive translation into many-sorted first-order logic?

From the little I've read about Henkin semantics for second-order logic, it seems like a fairly thin wrapper over the standard semantics for first-order logic. I'm wondering whether this impression is ...
user avatar
  • 6,426
4 votes
1 answer
174 views

Does intuitionist second-order logic prove the negations of some classical theorems?

On p.2(!) of his book The Boundary Stones of Thought, Ian Rumfitt asserts Intuitionistic second-order logic affirms the negations of some classical theorems. That surprised me. I'm probably just ...
user avatar
2 votes
1 answer
73 views

Are there logics that lack a Löwenheim number?

This answer contains the definition of the Löwenheim number. The question is about second-order logic. The Löwenheim number is the smallest cardinal $λ$ so that if a theory $T$ has a model then it ...
user avatar
  • 6,426
0 votes
0 answers
64 views

Converting a sentence to a formula in second order logic and typed first-order logic

I was given the following sentence: "There are sets X & Y, such that the function F from X to Y is injective but not surjective." I need to turn this sentence into a formula in: second ...
user avatar
1 vote
1 answer
56 views

Show that V is a strong limit in second-order terms

Let $X, Y$ be two proper classes. We say that the power of $X$ is equinumerous to $Y$ iff there is a relation $R$ with $domain(R) = Y$ and $range(R) = X$ such that (i) $\forall Z \subseteq X \exists y ...
user avatar
  • 379
0 votes
0 answers
33 views

Prove that the prime numbers set can be defined in a model

Given first order language, $L = <0, S, +, \cdot, = >$, $0$ is the number zero, $S$ is the successor function, and a model $M$ with the domain $\mathbb{N}$, I need to prove that the prime ...
user avatar
1 vote
0 answers
40 views

Can we get something equivalent to $\mathsf{ZFC2}$ by naively allowing the separation and replacement to range over second-order wffs? [duplicate]

I've seen $\mathsf{ZFC2}$ mentioned in a few questions such as this one and I'm curious about ways to axiomatize it that have the fewest differences from plain $\mathsf{ZFC}$ as possible. My question ...
user avatar
  • 6,426
3 votes
2 answers
95 views

Expressing "finitely many", "infinitely many", "most" and "more" in second-order logic

Famously it is impossible to express "finitely many" or "most" and so on in first-order logic, but we can apparently do so in second-order logic. Unfortunately, I cannot find ...
user avatar
1 vote
1 answer
43 views

Suggestions for learning natural deductions in simple and ramified second order logic

I am reading the book Natural Deductions: A proof-theoretic study by Dag Prawitz and stuck at the chapter V of this book, which is about natural deduction in second order logic. Before reading this ...
user avatar
3 votes
1 answer
57 views

Classical $\mathcal{A}$ quantifier: prove that $(\mathcal{A} \forall)_{1}$ relations and $\Sigma_1^1$ relations have the same expressive strength..

A quantifier on $\mathbb{N}$ is a set $Q$ such that $\emptyset \subsetneq Q \subsetneq P(\mathbb{N})$ and $Q$ is closed upwards, i.e. if $X \subseteq Y \subseteq \mathbb{N}$ and $X \in Q$, then $Y \in ...
user avatar
1 vote
0 answers
41 views

Does adding new sorts to propositional logic with quantification keep the logic second-order?

Suppose we add propositional quantifiers in the language of propositional logic. So, for example, we can write $\forall\!p\,(p\lor\neg p)$ to express the proposition that every proposition is either ...
user avatar
  • 571
0 votes
1 answer
31 views

Writing $\forall q\, (\forall p\,q)$ instead of the schematic $\forall p\,\phi$

Suppose we're working with the propositional logic enriched with propositional quantifiers. Is it, in general, all right to write $\forall q\, (\forall p\,q)$ instead of the schematic $\forall p\,\phi$...
user avatar
  • 571
0 votes
2 answers
173 views

Formal or informal definability of the standard model of natural numbers

I started a discussion in comments to this answer, but it grew beyond what fits comments, so I'm promoting it to this separate question. Here is a recap: $\Large\color{green}{\unicode{0x2BA9}}\,$ The ...
user avatar
6 votes
0 answers
79 views

Candidate "AEC-yielding" fragments of bad logics

Given a logic $\mathcal{L}$ and a signature $\Sigma$, let the $\Sigma$-system of $\mathcal{L}$ be the pair $Sys_\Sigma(\mathcal{L})=(Struc(\Sigma),\preccurlyeq_\mathcal{L})$ of structures partially ...
user avatar
3 votes
1 answer
71 views

What's the purpose of the word $w$ in the proof for $ L \in \mathsf{REG} \implies L(\varphi) \in \mathsf{MSO}$ with $L(\varphi) = L$?

I'm taking a lecture where we proved $ L \subseteq \mathsf{REG(\Sigma^*)} \iff \exists \phi \in \mathsf{MSO}$ with $L(\phi) = L$. For the first direction $L \subseteq \mathsf{REG(\Sigma^*)} \implies \...
user avatar
  • 473
10 votes
1 answer
215 views

A tame(ish) fragment of second-order logic

This question is about a tame(?) fragment of second-order logic with the standard semantics $\mathsf{SOL}$, motivated by the Tarski-Vaught test. The general setup is as follows. Given structures $\...
user avatar
2 votes
1 answer
69 views

What is the Turing degree of truth in the second-order theory of real numbers?

Let $X$ be the set of Godel numbers of sentences in the second-order language of ordered fields which are true in $\mathbb{R}$. Then my question is, what is the Turing degree of $X$? In particular, ...
user avatar
6 votes
1 answer
134 views

Are there nonstandard $\mathsf{PA}$ models without $\Delta^1_1$ cuts?

My question is the following: Is there a nonstandard model $\mathcal{M}\models\mathsf{PA}$ such that $\mathcal{M}$ has no $\Delta^1_1$-with-parameters-definable nonempty proper successor-closed ...
user avatar
6 votes
1 answer
128 views

"$\Sigma_1^1$-Peano arithmetic" - does it pin down $\mathbb{N}$?

Let $\mathsf{PA}_{\Sigma^1_1}$ be the theory in second-order logic gotten by extending the usual first-order Peano axioms to include arbitrary $\Sigma^1_1$ formulas in the induction scheme. My ...
user avatar
1 vote
1 answer
66 views

A problem with the Boolos/Burges/Jeffrey proof of incompleteness of second order logic

My question concerns the proof of the fact that the set of valid sentences of 2nd order logic (SOL) is not recursively enumerable, as presented in "Computability and Logic" 4th edition in ...
user avatar
2 votes
1 answer
371 views

How do you turn a proof of a mathematical statement into a zero-knowledge proof?

I recently watched a video on Numberphile2 in which Avi Wigderson describes how one can prove a graph has a 3-colouring in zero-knowledge and that as 3-colouring is NP-complete, all NP statements have ...
user avatar
  • 389
1 vote
0 answers
97 views

How can we trust second-order logic?

Let’s accept for the sake of argument the ontology of set theories without proper classes. Sets (improper classes) are the only things at all. This is perhaps silly, but it will hopefully illustrate a ...
user avatar
  • 1,569
5 votes
1 answer
104 views

Limitation of Henkin sematics in second order logic

I am reading Enderton's A Mathematical Introduction to Logic. The book explains that compactness fails in second order logic by a counter example $\Sigma = \{\neg \lambda_{\infty} , \lambda_2, \...
user avatar
2 votes
1 answer
72 views

Why second order logic is more expressive that the first order logic?

As far as I understand, the second order logic is more expressive than the first order logic because it can make statements about predicates. However, I do not understand why this problem (...
user avatar
  • 453
6 votes
1 answer
112 views

Does the logical system with the "there exist uncountably many"-quantifier satisfy a variant of upwards Löwenheim-Skolem

Let $\mathcal L_Q$ be the logical system that includes first order logic together with the quantifier $Q$ which is defined as follows: For an interpretation $\mathfrak I=(\mathfrak A, \beta)=((A,\...
user avatar
  • 139